[isabelle-dev] Forgotten feature of the datatype package
makarius at sketis.net
Thu May 28 22:45:18 CEST 2009
On Fri, 22 May 2009, Brian Huffman wrote:
> I came across an old feature of the datatype package that doesn't work
> theory Scratch
> imports Main
> datatype (bar) foo = Foo
> *** Unknown constant: "Scratch.foo.Foo"
> *** At command "datatype".
> I suppose this feature might be useful if for some reason you wanted to
> define a datatype with a non-alphanumeric name. But obviously it is not
> *that* useful, since the feature has been broken since Isabelle2008 at
> least, and apparently nobody has noticed.
This still needs some further investigation. As a general rule of thumb
there is no need to imitate obscure features of old packages, if there is
no clear indicating that there will be actual uses.
On the other hand, original 'datatype' as one of the very first Isabelle
packages probably still depends on this feature internally. IIRC, it was
introduced to accomodate old-style type names such as "*" which will still
be with us for some time. In newer developments, those that are less than
10 years old, plain identifiers are used uniformly of course.
More information about the isabelle-dev