[isabelle] Datatype selectors cannot have the same name as the datatype



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




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