79 |
79 |
80 (*<*) |
80 (*<*) |
81 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close> |
81 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close> |
82 nonterminal mtuple_args |
82 nonterminal mtuple_args |
83 syntax |
83 syntax |
84 "" :: "'a \<Rightarrow> mtuple_args" ("_") |
84 "" :: "'a \<Rightarrow> mtuple_args" (\<open>_\<close>) |
85 "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" ("_,/ _") |
85 "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" (\<open>_,/ _\<close>) |
86 "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") |
86 "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" (\<open>(2\<lbrace>_,/ _\<rbrace>)\<close>) |
87 syntax_consts |
87 syntax_consts |
88 "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair |
88 "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair |
89 translations |
89 translations |
90 "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
90 "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
91 "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y" |
91 "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y" |