Enum move_compiler::expansion::ast::SpecBlockMember_

pub enum SpecBlockMember_ {
    Condition {
        kind: SpecConditionKind,
        properties: Vec<PragmaProperty>,
        exp: Exp,
        additional_exps: Vec<Exp>,
    },
    Function {
        uninterpreted: bool,
        name: FunctionName,
        signature: FunctionSignature,
        body: FunctionBody,
    },
    Variable {
        is_global: bool,
        name: Name,
        type_parameters: Vec<(Name, AbilitySet)>,
        type_: Type,
        init: Option<Exp>,
    },
    Update {
        lhs: Exp,
        rhs: Exp,
    },
    Let {
        name: Name,
        post_state: bool,
        def: Exp,
    },
    Include {
        properties: Vec<PragmaProperty>,
        exp: Exp,
    },
    Apply {
        exp: Exp,
        patterns: Vec<SpecApplyPattern>,
        exclusion_patterns: Vec<SpecApplyPattern>,
    },
    Pragma {
        properties: Vec<PragmaProperty>,
    },
}

Variants

Condition

Fields

kind: SpecConditionKind

properties: Vec<PragmaProperty>

exp: Exp

additional_exps: Vec<Exp>

Function

Fields

uninterpreted: bool

name: FunctionName

signature: FunctionSignature

body: FunctionBody

Variable

Fields

is_global: bool

name: Name

type_parameters: Vec<(Name, AbilitySet)>

type_: Type

init: Option<Exp>

Update

Fields

lhs: Exp

rhs: Exp

Let

Fields

name: Name

post_state: bool

def: Exp

Include

Fields

properties: Vec<PragmaProperty>

exp: Exp

Apply

Fields

exp: Exp

patterns: Vec<SpecApplyPattern>

exclusion_patterns: Vec<SpecApplyPattern>

Pragma

Fields

properties: Vec<PragmaProperty>

Trait Implementations

impl AstDebug for SpecBlockMember_

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

impl Clone for SpecBlockMember_

fn clone(&self) -> SpecBlockMember_

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for SpecBlockMember_

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

Formats the value using the given formatter.

impl PartialEq<SpecBlockMember_> for SpecBlockMember_

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

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

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

This method tests for !=.

impl StructuralPartialEq for SpecBlockMember_