Email Gateway (Aug 18 2022 at 12:53): Email Gateway (Aug 18 2022 at 12:53):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hello all,
according to the Isabelle reference manual, identifiers may consist not
only of characters and numbers, but also of letters of the form "\<...>"
where ... is one letter or two letters. This works well for e.g. \<f>
and \<ff>, but if the two letters are different, say \<fh>, then I get
an inner lexical syntax error, e.g. in:
term "%\<fh>. 0"
term "%\<f>. 0" and term "%\<ff>. 0" however work perfectly.
How can I use e.g. \<fh> as an identifier in a lambda abstraction?
Thanks in advance,
Andreas
Email Gateway (Aug 18 2022 at 12:53):From: Makarius <makarius@sketis.net>
You can't. The two letters in the name of the symbol need to be equal.
Makarius
Email Gateway (Aug 18 2022 at 12:54):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Makarius wrote:
If that seems arbitrary: the syntax for identifiers and therefore bound names
says that it must consist of letters (and numbers, underscore etc). \<ff> is a
letter, so is \<alpha>, \<fh> is not.
There is a table in Pure/General/symbol.ML that says which symbols are letters.
Cheers,
Gerwin
Last updated: May 03 2024 at 08:18 UTC