Re: [isabelle] \<fh> as identifier



Makarius wrote:
On Tue, 20 Jan 2009, Andreas Lochbihler wrote:

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?

You can't.  The two letters in the name of the symbol need to be equal.

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.