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.


	Makarius





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