theory Scratch
  imports Main
begin

typedecl syntax_click_list_args

datatype 'a click_list = CLNil ("\<lbrakk>\<rbrakk>") | CLCons 'a "'a click_list"
consts "syntax_click_list" :: "syntax_click_list_args \<Rightarrow> 'a" ("\<lbrakk>_\<rbrakk>")

syntax "" :: "args \<Rightarrow> syntax_click_list_args" ("_")

translations
  "\<lbrakk>x, xs\<rbrakk>" == "CONST CLCons x \<lbrakk>xs\<rbrakk>"
  "\<lbrakk>x\<rbrakk>" == "CONST CLCons x \<lbrakk>\<rbrakk>"

term "\<lbrakk>\<rbrakk>"
term "\<lbrakk>x\<rbrakk>"
term "\<lbrakk>x,y\<rbrakk>"

end