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 :)
On 05/10/2010 09:06 AM, Florian Haftmann wrote:
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and