|
2112
|
1 |
signature Thry_sig =
|
|
|
2 |
sig
|
|
|
3 |
type Type
|
|
|
4 |
type Preterm
|
|
|
5 |
type Term
|
|
|
6 |
type Thm
|
|
|
7 |
type Thry
|
|
|
8 |
type 'a binding
|
|
|
9 |
|
|
|
10 |
structure USyntax : USyntax_sig
|
|
|
11 |
val match_term : Thry -> Preterm -> Preterm
|
|
|
12 |
-> Preterm binding list * Type binding list
|
|
|
13 |
|
|
|
14 |
val match_type : Thry -> Type -> Type -> Type binding list
|
|
|
15 |
|
|
|
16 |
val typecheck : Thry -> Preterm -> Term
|
|
|
17 |
|
|
|
18 |
val make_definition: Thry -> string -> Preterm -> Thm * Thry
|
|
|
19 |
|
|
|
20 |
(* Datatype facts of various flavours *)
|
|
|
21 |
val match_info: Thry -> string -> {constructors:Preterm list,
|
|
|
22 |
case_const:Preterm} USyntax.Utils.option
|
|
|
23 |
|
|
|
24 |
val induct_info: Thry -> string -> {constructors:Preterm list,
|
|
|
25 |
nchotomy:Thm} USyntax.Utils.option
|
|
|
26 |
|
|
|
27 |
val extract_info: Thry -> {case_congs:Thm list, case_rewrites:Thm list}
|
|
|
28 |
|
|
|
29 |
end;
|
|
|
30 |
|
|
|
31 |
|