Struct move_ir_types::spec_language_ast::Invariant_
source · pub struct Invariant_ {
pub modifier: Option<Symbol>,
pub target: Option<Symbol>,
pub exp: SpecExp,
}
Expand description
An invariant over a resource.
Fields§
§modifier: Option<Symbol>
A free string (for now) which specifies the function of this invariant.
target: Option<Symbol>
An optional synthetic variable to which the below expression is assigned to.
exp: SpecExp
A specification expression.
Trait Implementations§
source§impl Clone for Invariant_
impl Clone for Invariant_
source§fn clone(&self) -> Invariant_
fn clone(&self) -> Invariant_
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 moresource§impl Debug for Invariant_
impl Debug for Invariant_
source§impl PartialEq<Invariant_> for Invariant_
impl PartialEq<Invariant_> for Invariant_
source§fn eq(&self, other: &Invariant_) -> bool
fn eq(&self, other: &Invariant_) -> bool
This method tests for
self
and other
values to be equal, and is used
by ==
.