Qed.Engine
Generic Engine Signature
type link =
| F_call of string
n-ary function
*)| F_subst of string * string
n-ary function with substitution first value is the link name, second is the substitution (e.g. "foo(%1,%2)")
*)| F_left of string
2-ary function left-to-right +
*)| F_right of string
2-ary function right-to-left +
*)| F_list of string * string
n-ary function with (cons,nil) constructors
*)| F_assoc of string
associative infix operator
*)| F_bool_prop of string * string
Has a bool and prop version
*)type mode =
| Mpositive
Current scope is Prop
in positive position.
| Mnegative
Current scope is Prop
in negative position.
| Mterm
Current scope is Term
.
| Mterm_int
Int
is required but actual scope is Term
.
| Mterm_real
Real
is required but actual scope is Term
.
| Mint
Current scope is Int
.
| Mreal
Current scope is Real
.
module type Env = sig ... end
Generic Engine Signature
class type virtual ['z, 'adt, 'field, 'logic, 'tau, 'var, 'term, 'env] engine = object ... end