Struct move_model::ast::SpecFunDecl
source · 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§
source§impl Clone for SpecFunDecl
impl Clone for SpecFunDecl
source§fn clone(&self) -> SpecFunDecl
fn clone(&self) -> SpecFunDecl
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