On Mon, 27 Sep 2010, Florian Haftmann wrote:
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?
My impression is that 'datatype' always had this tendency to require
the LHS type arguments to agree exactly, but Stefan should know what he
had in mind originally.
I've made a quick test with Isabelle2008, Isabelle2009, Isabelle2009-1,
Isabelle2009-2: all fail on the example above, but with different
low-level exceptions.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
