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