Qed.Logic
type 'a operator = {
invertible : bool;
associative : bool;
commutative : bool;
idempotent : bool;
neutral : 'a element;
absorbant : 'a element;
}
Algebraic properties for user operators.
type 'a category =
| Function
logic function
*)| Constructor
f xs = g ys
iff f=g && xi=yi
| Injection
f xs = f ys
iff xi=yi
| Operator of 'a operator
Algebraic properties for functions.
module type Symbol = sig ... end
Ordered, hash-able and pretty-printable symbols
module type Data = sig ... end
module type Field = sig ... end
module type Function = sig ... end
module type Variable = sig ... end
type ('f, 'a, 'd, 'x, 'b, 'e) term_repr =
| True
| False
| Kint of Z.t
| Kreal of Q.t
| Times of Z.t * 'e
mult: k1 * e2
*)| Add of 'e list
add: e11 + ... + e1n
*)| Mul of 'e list
mult: e11 * ... * e1n
*)| Div of 'e * 'e
| Mod of 'e * 'e
| Eq of 'e * 'e
| Neq of 'e * 'e
| Leq of 'e * 'e
| Lt of 'e * 'e
| Aget of 'e * 'e
access: array1idx2
| Aset of 'e * 'e * 'e
update: array1idx2 -> elem3
| Acst of ('f, 'a) datatype * 'e
constant array type -> value
| Rget of 'e * 'f
| Rdef of ('f * 'e) list
| And of 'e list
and: e11 && ... && e1n
*)| Or of 'e list
or: e11 || ... || e1n
*)| Not of 'e
| Imply of 'e list * 'e
imply: (e11 && ... && e1n) ==> e2
*)| If of 'e * 'e * 'e
ite: if c1 then e2 else e3
*)| Fun of 'd * 'e list
Complete call (no partial app.)
*)| Fvar of 'x
| Bvar of int * ('f, 'a) datatype
| Apply of 'e * 'e list
High-Order application (Cf. binder)
*)| Bind of binder * ('f, 'a) datatype * 'b
representation of terms. type arguments are the following:
module type Term = sig ... end