equal
deleted
inserted
replaced
8 |
8 |
9 Type = Maybe + |
9 Type = Maybe + |
10 |
10 |
11 (* new class for structures containing type variables *) |
11 (* new class for structures containing type variables *) |
12 classes |
12 classes |
13 type_struct < term |
13 type_struct < type |
14 |
14 |
15 (* type expressions *) |
15 (* type expressions *) |
16 datatype |
16 datatype |
17 typ = TVar nat | "->" typ typ (infixr 70) |
17 typ = TVar nat | "->" typ typ (infixr 70) |
18 |
18 |
21 subst = nat => typ |
21 subst = nat => typ |
22 |
22 |
23 arities |
23 arities |
24 typ::type_struct |
24 typ::type_struct |
25 list::(type_struct)type_struct |
25 list::(type_struct)type_struct |
26 fun::(term,type_struct)type_struct |
26 fun::(type,type_struct)type_struct |
27 |
27 |
28 (* substitutions *) |
28 (* substitutions *) |
29 |
29 |
30 (* identity *) |
30 (* identity *) |
31 constdefs |
31 constdefs |