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