[isabelle-dev] New (Co)datatypes: Status & Plan 2
florian.haftmann at informatik.tu-muenchen.de
Mon Nov 18 23:05:14 CET 2013
> First, LFP needs these five theories from "Library":
> GFP also needs one more theory from "Library":
> Then LFP and GFP need the following cardinals theories (all by Popescu &
> For completeness, these are the theories that are genuinely part of LFP:
> And part of GFP:
a huge bunch indeed, but I am sure you will find ways to work this out.
From a theoretic point of view it is a little bit – irritating that so
much stuff is needed to issue something so fundamental as datatypes, but
similar opinions have been held about blast in its beginning.
Have you already thought about bootstrap order? If the datatype
construction demands already lists, there is a problem ;-)…
All the best,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 263 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev