blob: f44cff13e15f97faf83125bed3953580ef66f72e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
signature evalLib =
sig
(* This module implements [eval_conv], which supersedes EVAL_CONV by
allowing to use custom unfolding theorems. This is particularly
useful for divDefLib, which returns rewriting theorems to the user
which are actually not definitional theorems.
*)
include Abbrev
(* The following functions allow to *persistently* register custom unfolding theorems *)
val add_unfold_thm : thm -> unit
val add_unfold_thms : thm list -> unit
(* Get the unfolding theorems *)
val get_unfold_thms : unit -> thm list
(* The custom "eval" conversion *)
val eval_conv : conv
(* The custom "eval" function *)
val eval : term -> term
end
|