[isabelle-dev] Type arguments in datatype declarations
berghofe at in.tum.de
Mon Sep 27 14:50:46 CEST 2010
Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
> 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"
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.
More information about the isabelle-dev