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.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
