equal
deleted
inserted
replaced
21 subsection \<open>Finite lazy lists\<close> |
21 subsection \<open>Finite lazy lists\<close> |
22 |
22 |
23 code_lazy_type llist |
23 code_lazy_type llist |
24 |
24 |
25 no_notation lazy_llist (\<open>_\<close>) |
25 no_notation lazy_llist (\<open>_\<close>) |
26 nonterminal llist_args |
|
27 syntax |
26 syntax |
28 "" :: "'a \<Rightarrow> llist_args" (\<open>_\<close>) |
27 "_llist" :: "args => 'a list" (\<open>\<^bold>[(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>]\<close>) |
29 "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args" (\<open>_,/ _\<close>) |
|
30 "_llist" :: "llist_args => 'a list" (\<open>\<^bold>[(_)\<^bold>]\<close>) |
|
31 syntax_consts |
28 syntax_consts |
32 "_llist_args" "_llist" == lazy_llist |
29 lazy_llist |
33 translations |
30 translations |
34 "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]" |
31 "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]" |
35 "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]" |
32 "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]" |
36 "\<^bold>[x\<^bold>]" == "CONST lazy_llist x" |
33 "\<^bold>[x\<^bold>]" == "CONST lazy_llist x" |
37 |
34 |