Enum z3tracer::syntax::Term [−][src]
pub enum Term {
App {
name: String,
args: Vec<Ident>,
meaning: Option<Meaning>,
},
Var {
index: u64,
},
Quant {
name: String,
params: usize,
triggers: Vec<Ident>,
body: Ident,
var_names: Option<Vec<VarName>>,
},
Lambda {
name: String,
params: u64,
triggers: Vec<Ident>,
body: Ident,
},
Proof {
name: String,
args: Vec<Ident>,
property: Ident,
},
Builtin {
name: Option<String>,
},
}
Expand description
Concrete representation of a term.
Variants
Application of a symbol on top of other term(s).
Bound variable, used in the body a quantified expression or a lambda.
Fields of Var
index: u64
Quantified expression (either universal or existential).
Fields of Quant
Lambda.
Proof term.
Builtin (typically used to refer to a theory or for true/false literals).
Implementations
Trait Implementations
Auto Trait Implementations
impl RefUnwindSafe for Term
impl UnwindSafe for Term
Blanket Implementations
Mutably borrows from an owned value. Read more