Struct move_model::ast::SpecFunDecl

pub struct SpecFunDecl {
    pub loc: Loc,
    pub name: Symbol,
    pub type_params: Vec<(Symbol, Type)>,
    pub params: Vec<(Symbol, Type)>,
    pub context_params: Option<Vec<(Symbol, bool)>>,
    pub result_type: Type,
    pub used_spec_vars: BTreeSet<QualifiedInstId<SpecVarId>>,
    pub used_memory: BTreeSet<QualifiedInstId<StructId>>,
    pub uninterpreted: bool,
    pub is_move_fun: bool,
    pub is_native: bool,
    pub body: Option<Exp>,
}

Fields

loc: Loc

name: Symbol

type_params: Vec<(Symbol, Type)>

params: Vec<(Symbol, Type)>

context_params: Option<Vec<(Symbol, bool)>>

result_type: Type

used_spec_vars: BTreeSet<QualifiedInstId<SpecVarId>>

used_memory: BTreeSet<QualifiedInstId<StructId>>

uninterpreted: bool

is_move_fun: bool

is_native: bool

body: Option<Exp>

Trait Implementations

impl Clone for SpecFunDecl

fn clone(&self) -> SpecFunDecl

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for SpecFunDecl

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

Formats the value using the given formatter.