Enum move_lang::expansion::ast::SpecConditionKind_

pub enum SpecConditionKind_ {
    Assert,
    Assume,
    Decreases,
    AbortsIf,
    AbortsWith,
    SucceedsIf,
    Modifies,
    Emits,
    Ensures,
    Requires,
    Invariant(Vec<(Name, AbilitySet)>),
    InvariantUpdate(Vec<(Name, AbilitySet)>),
    Axiom(Vec<(Name, AbilitySet)>),
}

Variants

Assert

Assume

Decreases

AbortsIf

AbortsWith

SucceedsIf

Modifies

Emits

Ensures

Requires

Invariant(Vec<(Name, AbilitySet)>)

InvariantUpdate(Vec<(Name, AbilitySet)>)

Axiom(Vec<(Name, AbilitySet)>)

Trait Implementations

impl AstDebug for SpecConditionKind_

fn ast_debug(&self, w: &mut AstWriter)

impl Clone for SpecConditionKind_

fn clone(&self) -> SpecConditionKind_

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for SpecConditionKind_

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

Formats the value using the given formatter.

impl PartialEq<SpecConditionKind_> for SpecConditionKind_

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

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

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

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for SpecConditionKind_