Theory.Init
The initial theory.
val var : 'a var -> 'a pure
var v is the value of the variable v.
var v
v
val unk : 'a Value.sort -> 'a pure
unk s an unknown value of sort s.
unk s
s
This term explicitly denotes a term with undefined or unknown value.
val let_ : 'a var -> 'a pure -> 'b pure -> 'b pure
let_ v exp body bind the value of exp to v body.
let_ v exp body
exp
body
val ite : bool -> 'a pure -> 'a pure -> 'a pure
ite c x y is x if c evaluates to b1 else y.
ite c x y
x
c
b1
y