From 99dc9743a3291d664a70e4b78a7252d0ffb5b627 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 16 Aug 2022 21:29:12 -0400 Subject: [PATCH] doc --- src/cc/expl.mli | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/cc/expl.mli b/src/cc/expl.mli index 24618076..efa26063 100644 --- a/src/cc/expl.mli +++ b/src/cc/expl.mli @@ -28,20 +28,20 @@ val mk_congruence : E_node.t -> E_node.t -> t val mk_theory : Term.t -> Term.t -> (Term.t * Term.t * t list) list -> Proof_term.step_id -> t (** [mk_theory t u expl_sets pr] builds a theory explanation for - why [|- t=u]. It depends on sub-explanations [expl_sets] which - are tuples [ (t_i, u_i, expls_i) ] where [expls_i] are - explanations that justify [t_i = u_i] in the current congruence closure. + why [|- t=u]. It depends on sub-explanations [expl_sets] which + are tuples [ (t_i, u_i, expls_i) ] where [expls_i] are + explanations that justify [t_i = u_i] in the current congruence closure. - The proof [pr] is the theory lemma, of the form - [ (t_i = u_i)_i |- t=u ]. - It is resolved against each [expls_i |- t_i=u_i] obtained from - [expl_sets], on pivot [t_i=u_i], to obtain a proof of [Gamma |- t=u] - where [Gamma] is a subset of the literals asserted into the congruence - closure. + The proof [pr] is the theory lemma, of the form + [ (t_i = u_i)_i |- t=u ]. + It is resolved against each [expls_i |- t_i=u_i] obtained from + [expl_sets], on pivot [t_i=u_i], to obtain a proof of [Gamma |- t=u] + where [Gamma] is a subset of the literals asserted into the congruence + closure. - For example for the lemma [a=b] deduced by injectivity - from [Some a=Some b] in the theory of datatypes, - the arguments would be - [a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr] - where [pr] is the injectivity lemma [Some a=Some b |- a=b]. - *) + For example for the lemma [a=b] deduced by injectivity + from [Some a=Some b] in the theory of datatypes, + the arguments would be + [a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr] + where [pr] is the injectivity lemma [Some a=Some b |- a=b]. +*)