[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)
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
That's indeed the striking point. Thanks for explaining.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev