Email Gateway (Aug 22 2022 at 11:38): Email Gateway (Aug 22 2022 at 11:38):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear BNF experts,
I would like to define a selector for a datatype whose name is the same as the name of the
datatype. For example,
datatype 'v foo = Foo (foo: 'v)
For some reason, this raises a type error claiming that "foo" was of type 'v foo rather
than "'v foo => 'v". As both before and after the datatype declaration, the name foo is
not bound, I guess that the name foo is used somewhere internally in the BNF package. Is
that right?
So I'd like to request the feature that selectors in datatypes may have the same name as
the type.
Best,
Andreas
Email Gateway (Aug 22 2022 at 11:51):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Andreas,
That's correct. The name "foo" was used for values of that type, without checking whether the name clashed with discriminators or selectors. I have just pushed a change to testboard.
Incidentally, this gave me the idea of testing this:
datatype f = f
This currently gives a failure, because "f" is used internally as well (but at another place than the selectors/discriminators). Hm, and I thought I'd go home early tonight!
Cheers,
Jasmin
Last updated: Apr 23 2024 at 16:19 UTC