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

[Florian Haftmann]

> 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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>