Re: [isabelle] Type classes vs. locales?

On 14-08-26 08:24, Holden Lee wrote:
In Isabelle, (A) what can be done using locales that can't be done using
typeclasses, and (B) what can be done using locales that would be
inconvenient with typeclasses?

I don't know all the details about how to overload notation, but it appears that overloading notation through type classes is generally superior to doing it other ways, and notation can be of huge importance.

If you use type classes, you obtain other magic by default, in particular with the code generator, which at a minimum comes into play with the "value" command. It's very useful to always be able to do some experimental computations with "value", and very annoying when "value" won't work for my functions, even though my logic is good.


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