diff options
Diffstat (limited to 'plugins/cc/ccproof.mli')
| -rw-r--r-- | plugins/cc/ccproof.mli | 34 |
1 files changed, 32 insertions, 2 deletions
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 50e3624d0a..ba95ebb59e 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -20,10 +20,40 @@ type rule= and proof = private {p_lhs:term;p_rhs:term;p_rule:rule} +(** Proof smart constructors *) + +val prefl:term -> proof + +val pcongr: proof -> proof -> proof + +val ptrans: proof -> proof -> proof + +val psym: proof -> proof + +val pax : (Ccalgo.term * Ccalgo.term) Ccalgo.Constrhash.t -> + Ccalgo.Constrhash.key -> proof + +val psymax : (Ccalgo.term * Ccalgo.term) Ccalgo.Constrhash.t -> + Ccalgo.Constrhash.key -> proof + +val pinject : proof -> pconstructor -> int -> int -> proof + +(** Proof building functions *) + +val equal_proof : forest -> int -> int -> proof + +val edge_proof : forest -> (int*int)*equality -> proof + +val path_proof : forest -> int -> ((int*int)*equality) list -> proof + +val congr_proof : forest -> int -> int -> proof + +val ind_proof : forest -> int -> pa_constructor -> int -> pa_constructor -> proof + +(** Main proof building function *) + val build_proof : forest -> [ `Discr of int * pa_constructor * int * pa_constructor | `Prove of int * int ] -> proof - - |