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



Dear BNF user,

> 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
> [...]
> 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.


Thanks for the report. This is now fixed in the repository (d71c2737ee21).

Cheers,

Jasmin





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