Re: [isabelle] \<fh> as identifier
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and