[isabelle] BNF: Dead type variables confuse custom names for set functions



Dear BNF developers,

In Isabelle2013-1, dead type variables in datatype_new definitions require confusing specifications for custom names of the set functions. Here's an example where 'a is dead:

datatype_new ('a, foo_B: 'b, foo_C: 'c, foo_D: 'd) foo = Foo "'a => 'b" 'c 'd

I would expect to get the following 3 set functions

foo_B :: ('a, 'b, 'c, 'd) foo => 'b set
foo_C :: ('a, 'b, 'c, 'd) foo => 'c set
foo_D :: ('a, 'b, 'c, 'd) foo => 'd set

Unfortunately, datatype_new defines the following functions.

foo_set1 :: ('a, 'b, 'c, 'd) foo => 'b set
foo_B :: ('a, 'b, 'c, 'd) foo => 'c set
foo_C :: ('a, 'b, 'c, 'd) foo => 'd set

Apparently, dead type variables shift the positions of the custom names. In order to get what I want, I have to write the following specification (which I consider at least confusing):

datatype_new (foo_B: 'a, foo_C: 'b, foo_D: 'c, 'd) foo = Foo "'a => 'b" 'c 'd

Best,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.