[isabelle] should this use of the datatype package produce an error?



Hello all,

Peter Gammie recently brought this issue to my attention (with
"domain" instead of "datatype", but the behavior is the same for
both).

The following datatype definition is accepted without any warning messages:

datatype tree = "tree list"

Can anyone guess what this type definition actually means?

That's right, it defines a datatype with a single nullary constructor,
which is called "tree list". Never mind that the constructor's name
contains a space, and is therefore impossible to parse.

Clearly, no one would ever write such a datatype definition on purpose.

A feature request: If the name of a constant contains a space or other
illegal character, the datatype package should issue an error (or at
the very least, a warning message).

- Brian





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