[isabelle-dev] Type arguments in datatype declarations
makarius at sketis.net
Mon Sep 27 16:43:41 CEST 2010
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
More information about the isabelle-dev