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

post-rebase fix

Browse source
This commit is contained in:
Simon Cruanes 2021-06-11 21:55:44 -04:00
parent 6a9dbb8440
commit 899ea67188
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/core/Sidekick_core.ml
View file

@ -630,7 +630,7 @@ module type SOLVER_INTERNAL = sig
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. *)
val normalize : t -> term -> term val normalize : t -> term -> (term * P.t) option
(** Normalize a term using all the hooks. This performs (** Normalize a term using all the hooks. This performs
a fixpoint, i.e. it only stops when no hook applies anywhere inside a fixpoint, i.e. it only stops when no hook applies anywhere inside
the term. *) the term. *)