Email Gateway (Aug 19 2022 at 12:36): Email Gateway (Aug 19 2022 at 12:36):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 19 2022 at 12:37):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Dear BNF user,
Thanks for the report. This is now fixed in the repository (d71c2737ee21).
Cheers,
Jasmin
Last updated: Apr 23 2024 at 16:19 UTC