Re: [isabelle] Overloading in locales

Hi John,

> Thanks for the pointer to overloading. Can the class declaring the
> class operation or the instantiation of the class be constructed
> within a locale? 

> Can all or part of the overloading happen inside a locale rather than
> at the top level, e.g., can the instantiation of plus be created
> inside a locale?

Class instantiations are always global, since there is no concept of
»local sort algebra« or such in Isabelle.

> Also, if I were to overload a function 'foo' that returns true if the
> input is of type A and false if it's of type B, then is the following
> correct?

Rule of thumb: Try out and report if you get into problems ;-)




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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