Enum move_model::ast::ConditionKind
source · pub enum ConditionKind {
Show 19 variants
LetPost(Symbol),
LetPre(Symbol),
Assert,
Assume,
Decreases,
AbortsIf,
AbortsWith,
SucceedsIf,
Modifies,
Emits,
Ensures,
Requires,
StructInvariant,
FunctionInvariant,
LoopInvariant,
GlobalInvariant(Vec<Symbol>),
GlobalInvariantUpdate(Vec<Symbol>),
SchemaInvariant,
Axiom(Vec<Symbol>),
}
Expand description
Variants§
LetPost(Symbol)
LetPre(Symbol)
Assert
Assume
Decreases
AbortsIf
AbortsWith
SucceedsIf
Modifies
Emits
Ensures
Requires
StructInvariant
FunctionInvariant
LoopInvariant
GlobalInvariant(Vec<Symbol>)
GlobalInvariantUpdate(Vec<Symbol>)
SchemaInvariant
Axiom(Vec<Symbol>)
Implementations§
source§impl ConditionKind
impl ConditionKind
sourcepub fn allows_old(&self) -> bool
pub fn allows_old(&self) -> bool
Returns true of this condition allows the old(..)
expression.
sourcepub fn allowed_on_fun_decl(&self, _visibility: FunctionVisibility) -> bool
pub fn allowed_on_fun_decl(&self, _visibility: FunctionVisibility) -> bool
Returns true if this condition is allowed on a function declaration.
sourcepub fn allowed_on_fun_impl(&self) -> bool
pub fn allowed_on_fun_impl(&self) -> bool
Returns true if this condition is allowed in a function body.
sourcepub fn allowed_on_struct(&self) -> bool
pub fn allowed_on_struct(&self) -> bool
Returns true if this condition is allowed on a struct.
sourcepub fn allowed_on_module(&self) -> bool
pub fn allowed_on_module(&self) -> bool
Returns true if this condition is allowed on a module.
Trait Implementations§
source§impl Clone for ConditionKind
impl Clone for ConditionKind
source§fn clone(&self) -> ConditionKind
fn clone(&self) -> ConditionKind
Returns a copy of the value. Read more
1.0.0 · source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source
. Read moresource§impl Debug for ConditionKind
impl Debug for ConditionKind
source§impl Display for ConditionKind
impl Display for ConditionKind
source§impl PartialEq<ConditionKind> for ConditionKind
impl PartialEq<ConditionKind> for ConditionKind
source§fn eq(&self, other: &ConditionKind) -> bool
fn eq(&self, other: &ConditionKind) -> bool
This method tests for
self
and other
values to be equal, and is used
by ==
.impl Eq for ConditionKind
impl StructuralEq for ConditionKind
impl StructuralPartialEq for ConditionKind
Auto Trait Implementations§
impl RefUnwindSafe for ConditionKind
impl Send for ConditionKind
impl Sync for ConditionKind
impl Unpin for ConditionKind
impl UnwindSafe for ConditionKind
Blanket Implementations§
source§impl<Q, K> Equivalent<K> for Qwhere
Q: Eq + ?Sized,
K: Borrow<Q> + ?Sized,
impl<Q, K> Equivalent<K> for Qwhere Q: Eq + ?Sized, K: Borrow<Q> + ?Sized,
source§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
Compare self to
key
and return true
if they are equal.