Re: [isabelle] Overloaded datatype constructors

On 04/14/2012 09:52 PM, Makarius wrote:
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.

Now that I've thought about this, I no longer see how this could work: Suppose I want to define the type "'a re" of regular expressions, and overload just 0: I cannot write

  instantiation re :: (type) zero

before the type re is defined. So defining re inside this instantiation target won't work, unfortunately. To make this work, the package and the target would need to interact in a non-standard way, which seems far beyond the current architecture. Bad luck.

Anyway, for this application the advantage would just be syntactic, so it is no big deal.


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