[isabelle-dev] Type arguments in datatype declarations
florian.haftmann at informatik.tu-muenchen.de
Mon Sep 27 13:37:36 CEST 2010
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"
I have always assumed gracefully that for mutual datatype specifications
the names of arguments must be strictly the same, and many recent
extensions to the datatype package also do. Have specifications like
the second ever been intended to succeed? If yes, the issue could be
solved by consolidating specifications silently before processing. If
no, a user-level error message should be reported.
My personal preference is the second, but there might be different opinions.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev