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 ;-)

Regards,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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