[isabelle-dev] Type arguments in datatype declarations
florian.haftmann at informatik.tu-muenchen.de
Mon Sep 27 15:20:32 CEST 2010
> why can't we repair interpret_construction so that it handles this case
well, we can extend interpret_construction in such a way but also have
to do so for the tools which use it. This is perhaps not even that
difficult, but it adds considerable complexity to already complicated
tools, only to keep codified comments (the only effect of different
names of type variables in datatype branches is in the theory source
text and some quasi-internal tables).
> Nevertheless, it would be interesting to see what goes wrong,
> since your example used to work in older releases of Isabelle without
> further ado.
This surely is worth the effort.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev