equal
deleted
inserted
replaced
13 datatype |
13 datatype |
14 "list(A)" = Nil | Cons ("a \<in> A", "l \<in> list(A)") |
14 "list(A)" = Nil | Cons ("a \<in> A", "l \<in> list(A)") |
15 |
15 |
16 notation Nil (\<open>[]\<close>) |
16 notation Nil (\<open>[]\<close>) |
17 |
17 |
|
18 nonterminal list_args |
18 syntax |
19 syntax |
19 "_List" :: "is \<Rightarrow> i" (\<open>[(_)]\<close>) |
20 "" :: "i \<Rightarrow> list_args" (\<open>_\<close>) |
20 syntax_consts "_List" \<rightleftharpoons> Cons |
21 "_List_args" :: "[i, list_args] \<Rightarrow> list_args" (\<open>_,/ _\<close>) |
|
22 "_List" :: "list_args \<Rightarrow> i" (\<open>[(_)]\<close>) |
|
23 syntax_consts |
|
24 "_List_args" "_List" \<rightleftharpoons> Cons |
21 translations |
25 translations |
22 "[x, xs]" == "CONST Cons(x, [xs])" |
26 "[x, xs]" == "CONST Cons(x, [xs])" |
23 "[x]" == "CONST Cons(x, [])" |
27 "[x]" == "CONST Cons(x, [])" |
24 |
28 |
25 consts |
29 consts |