[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sun Aug 4 20:55:06 CEST 2013

> There is also a more technical reason why we want to perform the "nested
> to mutual" reduction: It gives us a very cheap compatibility layer for
> the old package. I.e. everything that is defined by the new package and
> falls into the fragment of the old package can be registered as an old
> datatype benefiting from all the infrastructure built around it (e.g.
> size function, Quickcheck, and other "datatype interpretations"). We
> expect this actually to save much work, compared to reimplementing that
> functionality now before moving to Main (instead we can do it in a lazy
> fashion).

That's indeed the striking point.  Thanks for explaining.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130804/8e879a04/attachment.sig>

More information about the isabelle-dev mailing list