--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Wed Aug 28 22:54:45 2024 +0200
@@ -23,8 +23,13 @@
code_lazy_type llist
no_notation lazy_llist ("_")
-syntax "_llist" :: "args => 'a list" ("\<^bold>[(_)\<^bold>]")
-syntax_consts "_llist" == lazy_llist
+nonterminal llist_args
+syntax
+ "" :: "'a \<Rightarrow> llist_args" ("_")
+ "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args" ("_,/ _")
+ "_llist" :: "llist_args => 'a list" ("\<^bold>[(_)\<^bold>]")
+syntax_consts
+ "_llist_args" "_llist" == lazy_llist
translations
"\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]"
"\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"