[isabelle-dev] Type arguments in datatype declarations

Stefan Berghofer 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"

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.


More information about the isabelle-dev mailing list