Struct SpecFunc

pub struct SpecFunc {
    pub name: Ident,
    pub sort_vars: Vec<Ident>,
    pub params: RefineParams,
    pub output: Sort,
    pub body: Option<Expr>,
    pub hide: bool,
}

A global function definition. It can be either an uninterpreted function or a syntactic abstraction, i.e., a function with a body.

Fields

name: Ident

sort_vars: Vec<Ident>

params: RefineParams

output: Sort

body: Option<Expr>

Body of the function. If not present this definition corresponds to an uninterpreted function.

hide: bool

Is this function “hidden” i.e. to be considered as uninterpreted by default (only makes sense if body is_some …) as otherwise it is always uninterpreted.

Trait Implementations

impl Debug for SpecFunc

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

Formats the value using the given formatter.