Struct State 

pub struct State {
    pub name: Ident,
    pub ty: ModelType,
    pub default: SpecExpr,
    pub pos: Pos,
}

Declare an element of global state accessible by verification specs.

Fields

name: Ident

Name of the state element.

ty: ModelType

Type of the state element.

default: SpecExpr

Default specification, applied if the state is not modified.

pos: Pos

Trait Implementations

impl Clone for State

fn clone(&self) -> State

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for State

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

Formats the value using the given formatter.

impl Eq for State

impl PartialEq for State

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for State

impl ToSExpr for State

fn to_sexpr(&self) -> SExpr

Convert the given value to an S-expression.