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 | (*
|
| Injection | (*
|
| 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: array1 |
| Aset of 'e * 'e * 'e | (* update: array1 |
| Acst of ( 'f, 'a ) datatype * 'e | (* constant array |
| 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