Re: [isabelle] Overloaded datatype constructors

On Fri, 13 Apr 2012, Alexander Krauss wrote:

I wonder if it is possible (possibly via some tricks) to make datatype constructors coincide with overloaded constants.

Is it conceivable that a fully localized datatype package could do this directly, when used in an instantiation target???

Yes, a properly datatype package would be able to do this. Constructor definitions are just definitions.

It should now also work with sophisticated syntax translations attached to them, because I've recently changed the "locale_const" scheme to use plain name space aliases for the special case where a locally defined term does not depend on context parameters. This means the syntax layer would see the global foundation constant in any case, not a funny abbreviation.

So it is now merely a matter to go through all the primitive and derived ML proofs of the package, and do the right thing wrt. "Free" variables.


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