From a446af49be66752ad048c4edfddcf55c41f1dda1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 16 Aug 2022 21:58:00 -0400 Subject: [PATCH] doc --- src/simplify/sidekick_simplify.mli | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/simplify/sidekick_simplify.mli b/src/simplify/sidekick_simplify.mli index 1c3abf1a..43ee9e54 100644 --- a/src/simplify/sidekick_simplify.mli +++ b/src/simplify/sidekick_simplify.mli @@ -18,13 +18,13 @@ val proof : t -> Proof_trace.t type hook = t -> Term.t -> (Term.t * Proof_step.id Iter.t) option (** Given a Term.t, try to simplify it. Return [None] if it didn't change. - A simple example could be a hook that takes a Term.t [t], - and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number, - returns [Some (const (x+y))], and [None] otherwise. + A simple example could be a hook that takes a Term.t [t], + and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number, + returns [Some (const (x+y))], and [None] otherwise. - The simplifier will take care of simplifying the resulting Term.t further, - caching (so that work is not duplicated in subterms), etc. - *) + The simplifier will take care of simplifying the resulting Term.t further, + caching (so that work is not duplicated in subterms), etc. +*) val add_hook : t -> hook -> unit