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