Quoting Florian Haftmann <[email protected]>:
The following datatype specification succeeds as expected
datatype ('a, 'b) foo = Nihil | Bar "('a, 'b) bar"
and ('a, 'b) bar = Foo "('a, 'b) foo"
whereas the following logically equivalent, but differently written
specification fails with a low-level exception in size.ML:
datatype ('a, 'b) foo = Nihil | Bar "('b, 'a) bar"
and ('b, 'a) bar = Foo "('a, 'b) foo"
Hi Florian,
this is a perfectly legal datatype and therefore should be handled by
the datatype package without prior "consolidation" or whatever, but
I think this case has just been overlooked when reimplementing the
definition of the size functions using the new infrastructure for
datatype interpretations. I'll try to find out what exactly goes wrong.
Greetings,
Stefan
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
