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



Dear Andreas,

> 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?

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





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