1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
_require "basis.smi"
_require "terms.smi"
structure Rules =
struct
datatype term =
Prop of {name : string, props : (term * term) list ref} * term list
| Var of int
datatype binding = Bind of int * term
type head = {name : string, props : (term * term) list ref}
val get : string -> head
val headname : head -> string
val add_lemma : term -> unit
val apply_subst : binding list -> term -> term
val rewrite : term -> term
datatype cterm = CProp of string * cterm list | CVar of int
val cterm_to_term : cterm -> term
val add : cterm -> unit
end
|
