Re: [isabelle] name of locale predicate



I have a type class that is essentially the same as Haskell's Show class. Hence I wanted to name it show, but then I can not define a function named 'show' (for showing a string) inside the class. Currently I'm using to_string instead of show, but I thought it would be nice to have the same naming as in Haskell :)

cheers

chris

On 05/10/2010 09:06 AM, Florian Haftmann wrote:
Hi Christian,

if I understood correctly, for every locale of name "L" we get a
predicate of name "L" taking the fixes of the locale as argument. Is it
possible to influence the name of this predicate?

on the ML level this is possible;  however there is no Isar syntax for
this.  What is your scenario?  The illusion of a differently named
locale predicate can be created using an abbreviation.

Hope this helps,
	Florian







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