20 datatype "typ" = |
20 datatype "typ" = |
21 Type ml_string "typ list" (infix "{\<struct>}" 120) |
21 Type ml_string "typ list" (infix "{\<struct>}" 120) |
22 | TFix vname sort (infix "\<Colon>\<epsilon>" 117) |
22 | TFix vname sort (infix "\<Colon>\<epsilon>" 117) |
23 |
23 |
24 abbreviation |
24 abbreviation |
25 Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115) |
25 Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115) where |
26 "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]" |
26 "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]" |
27 Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115) |
27 abbreviation |
|
28 Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115) where |
28 "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty" |
29 "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty" |
29 |
30 |
30 datatype "term" = |
31 datatype "term" = |
31 Const ml_string "typ" (infix "\<Colon>\<subseteq>" 112) |
32 Const ml_string "typ" (infix "\<Colon>\<subseteq>" 112) |
32 | Fix vname "typ" (infix ":\<epsilon>" 112) |
33 | Fix vname "typ" (infix ":\<epsilon>" 112) |
33 | App "term" "term" (infixl "\<bullet>" 110) |
34 | App "term" "term" (infixl "\<bullet>" 110) |
34 |
35 |
35 abbreviation |
36 abbreviation |
36 Apps :: "term \<Rightarrow> term list \<Rightarrow> term" (infixl "{\<bullet>}" 110) |
37 Apps :: "term \<Rightarrow> term list \<Rightarrow> term" (infixl "{\<bullet>}" 110) where |
37 "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts" |
38 "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts" |
38 |
39 |
39 |
40 |
40 subsection {* ML interface *} |
41 subsection {* ML interface *} |
41 |
42 |