diff options
Diffstat (limited to 'plugins/cc/ccproof.mli')
| -rw-r--r-- | plugins/cc/ccproof.mli | 38 |
1 files changed, 34 insertions, 4 deletions
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index d55d3ef7..0e0eb6d2 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,14 +16,44 @@ type rule= | Refl of term | Trans of proof*proof | Congr of proof*proof - | Inject of proof*constructor*int*int + | Inject of proof*pconstructor*int*int 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 - - |