Enum move_model::ast::ConditionKind

pub enum ConditionKind {
    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>),
    Update,
}

Conditions

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>)

Update

Implementations

impl ConditionKind

pub fn allows_old(&self) -> bool

Returns true of this condition allows the old(..) expression.

pub fn allowed_on_fun_decl(&self, _visibility: FunctionVisibility) -> bool

Returns true if this condition is allowed on a function declaration.

pub fn allowed_on_fun_impl(&self) -> bool

Returns true if this condition is allowed in a function body.

pub fn allowed_on_struct(&self) -> bool

Returns true if this condition is allowed on a struct.

pub fn allowed_on_module(&self) -> bool

Returns true if this condition is allowed on a module.

Trait Implementations

impl Clone for ConditionKind

fn clone(&self) -> ConditionKind

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ConditionKind

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for ConditionKind

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq<ConditionKind> for ConditionKind

fn eq(&self, other: &ConditionKind) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &ConditionKind) -> bool

This method tests for !=.

impl StructuralPartialEq for ConditionKind