simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

doc

Browse source
This commit is contained in:
Simon Cruanes 2022-08-16 21:58:00 -04:00
parent b23a031519
commit a446af49be
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/simplify/sidekick_simplify.mli
View file

@ -18,13 +18,13 @@ val proof : t -> Proof_trace.t
type hook = t -> Term.t -> (Term.t * Proof_step.id Iter.t) option 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. (** 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], 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, and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number,
returns [Some (const (x+y))], and [None] otherwise. returns [Some (const (x+y))], and [None] otherwise.
The simplifier will take care of simplifying the resulting Term.t further, The simplifier will take care of simplifying the resulting Term.t further,
caching (so that work is not duplicated in subterms), etc. caching (so that work is not duplicated in subterms), etc.
*) *)
val add_hook : t -> hook -> unit val add_hook : t -> hook -> unit