Email Gateway (Aug 18 2022 at 10:19): Email Gateway (Aug 18 2022 at 10:19):From: Nicole Rauch <rauch@informatik.uni-kl.de>
Hello all,
I defined a function called typeof, which I would like to use with the
syntax "\<tau>" .
So I defined the syntax
syntax
"_tau" :: "Value \<Rightarrow> Javatype" ("\<tau> _" 1000)
translations
"\<tau> v" == "typeof v"
But whatever priority I give above, I have to put parentheses around
all occurrences of "\<tau> x" in order to avoid getting ambiguous
syntax, although I can write "typeof x" without the parentheses.
Is this some kind of Isabelle function application precedence magic?
How can I define the syntax to behave in the same way as the original
function?
Thanks a lot in advance
Nicole
Email Gateway (Aug 18 2022 at 10:19):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Hi Nicole,
On Tuesday 13 March 2007, Nicole Rauch wrote:
syntax
"_tau" :: "Value \<Rightarrow> Javatype" ("\<tau> _" 1000)translations
"\<tau> v" == "typeof v"
[..]
How can I define the syntax to behave in the same way as the original
function?
The easiest way to do that is:
syntax
"_tau" :: "Value \<Rightarrow> Javatype" ("\<tau>")
Cheers,
Gerwin
Last updated: May 03 2024 at 04:19 UTC