Struct move_model::ast::Spec

pub struct Spec {
    pub loc: Option<Loc>,
    pub conditions: Vec<Condition>,
    pub properties: PropertyBag,
    pub on_impl: BTreeMap<CodeOffset, Spec>,
}

Specification and properties associated with a language item.

Fields

loc: Option<Loc>

conditions: Vec<Condition>

properties: PropertyBag

on_impl: BTreeMap<CodeOffset, Spec>

Implementations

impl Spec

pub fn has_conditions(&self) -> bool

pub fn filter<P>(&self, pred: P) -> impl Iterator<Item = &Condition>where P: FnMut(&&Condition) -> bool,

pub fn filter_kind( &self, kind: ConditionKind ) -> impl Iterator<Item = &Condition>

pub fn filter_kind_axiom(&self) -> impl Iterator<Item = &Condition>

pub fn any<P>(&self, pred: P) -> boolwhere P: FnMut(&Condition) -> bool,

pub fn any_kind(&self, kind: ConditionKind) -> bool

Trait Implementations

impl Clone for Spec

fn clone(&self) -> Spec

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Spec

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

Formats the value using the given formatter.

impl Default for Spec

fn default() -> Spec

Returns the “default value” for a type.