equal
deleted
inserted
replaced
7 ML {* val _ = recursive := false *} |
7 ML {* val _ = recursive := false *} |
8 |
8 |
9 atom_decl var |
9 atom_decl var |
10 atom_decl tvar |
10 atom_decl tvar |
11 |
11 |
12 (* there are types, coercion types and regular types *) |
12 (* there are types, coercion types and regular types list-data-structure *) |
13 (* list-data-structure |
|
14 nominal_datatype tkind = |
13 nominal_datatype tkind = |
15 KStar |
14 KStar |
16 | KFun "tkind" "tkind" |
15 | KFun "tkind" "tkind" |
17 and ckind = |
16 and ckind = |
18 CKEq "ty" "ty" |
17 CKEq "ty" "ty" |
19 and ty = |
18 and ty = |
20 TVar "tvar" |
19 TVar "tvar" |
21 | TC "string" |
20 | TC "string" |
22 | TApp "ty" "ty" |
21 | TApp "ty" "ty" |
23 | TFun "string" "ty list" |
22 | TFun "string" "ty_lst" |
24 | TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
23 | TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
25 | TEq "ty" "ty" "ty" |
24 | TEq "ty" "ty" "ty" |
|
25 and ty_lst = |
|
26 TsNil |
|
27 | TsCons "ty" "ty_lst" |
26 and co = |
28 and co = |
27 CC "string" |
29 CC "string" |
28 | CApp "co" "co" |
30 | CApp "co" "co" |
29 | CFun "string" "co list" |
31 | CFun "string" "co_lst" |
30 | CAll tv::"tvar" "ckind" C::"co" bind tv in C |
32 | CAll tv::"tvar" "ckind" C::"co" bind tv in C |
31 | CEq "co" "co" "co" |
33 | CEq "co" "co" "co" |
32 | CSym "co" |
34 | CSym "co" |
33 | CCir "co" "co" |
35 | CCir "co" "co" |
34 | CLeft "co" |
36 | CLeft "co" |
35 | CRight "co" |
37 | CRight "co" |
36 | CSim "co" |
38 | CSim "co" |
37 | CRightc "co" |
39 | CRightc "co" |
38 | CLeftc "co" |
40 | CLeftc "co" |
39 | CCoe "co" "co" |
41 | CCoe "co" "co" |
|
42 and co_lst = |
|
43 CsNil |
|
44 | CsCons "co" "co_lst" |
40 |
45 |
|
46 (* |
41 abbreviation |
47 abbreviation |
42 "atoms A \<equiv> atom ` A" |
48 "atoms A \<equiv> atom ` A" |
43 |
49 |
44 nominal_datatype trm = |
50 nominal_datatype trm = |
45 Var "var" |
51 Var "var" |