Struct move_model::ast::GlobalInvariant
source · pub struct GlobalInvariant {
pub id: GlobalId,
pub loc: Loc,
pub kind: ConditionKind,
pub mem_usage: BTreeSet<QualifiedInstId<StructId>>,
pub spec_var_usage: BTreeSet<QualifiedInstId<SpecVarId>>,
pub declaring_module: ModuleId,
pub properties: PropertyBag,
pub cond: Exp,
}
Expand description
Describes a global invariant.
Fields§
§id: GlobalId
§loc: Loc
§kind: ConditionKind
§mem_usage: BTreeSet<QualifiedInstId<StructId>>
§spec_var_usage: BTreeSet<QualifiedInstId<SpecVarId>>
§declaring_module: ModuleId
§properties: PropertyBag
§cond: Exp
Trait Implementations§
source§impl Clone for GlobalInvariant
impl Clone for GlobalInvariant
source§fn clone(&self) -> GlobalInvariant
fn clone(&self) -> GlobalInvariant
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 more