equal
deleted
inserted
replaced
8 |
8 |
9 signature TYPE_EXT0 = |
9 signature TYPE_EXT0 = |
10 sig |
10 sig |
11 val raw_term_sorts: term -> (indexname * sort) list |
11 val raw_term_sorts: term -> (indexname * sort) list |
12 val typ_of_term: (indexname -> sort) -> term -> typ |
12 val typ_of_term: (indexname -> sort) -> term -> typ |
|
13 val term_of_typ: bool -> typ -> term |
13 end; |
14 end; |
14 |
15 |
15 signature TYPE_EXT = |
16 signature TYPE_EXT = |
16 sig |
17 sig |
17 include TYPE_EXT0 |
18 include TYPE_EXT0 |
18 val term_of_sort: sort -> term |
19 val term_of_sort: sort -> term |
19 val term_of_typ: bool -> typ -> term |
|
20 val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast |
20 val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast |
21 val type_ext: SynExt.syn_ext |
21 val type_ext: SynExt.syn_ext |
22 end; |
22 end; |
23 |
23 |
24 structure TypeExt : TYPE_EXT = |
24 structure TypeExt : TYPE_EXT = |