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