Re: [isabelle] should this use of the datatype package produce an error?
On Thu, 15 Apr 2010, Brian Huffman wrote:
The following datatype definition is accepted without any warning
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).
This known problem shows up once a year or so. By using the proper local
theory layer for the package, it will just dissappear, because there are
sanity checks built in. Numerous other problems will be solved by
localizing old-style packages.
Just today Alex has pointed out another yearly accident: sort constraints
within type definitions (this time for record). The basic packages can
(typedecl, typedef, record) now handle that. The more complex ones
(datatype family, domain) still have their own partial ways of coping with
Maybe now is a good time for some spring cleaning, before we get too close
to the next Isabelle release. (It is already > 4 months after
This archive was generated by a fusion of
Pipermail (Mailman edition) and