equal
deleted
inserted
replaced
|
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 |