Bad name binding in Isabelle

Question

When entering the following definition

datatype env = "nat => 'a option"

Isabelle/jedit shows an exclamation mark and says

Legacy feature! Bad name binding: "nat => 'a option" 

What is the problem and how can I fix this type synonym?

Update: even

datatype 'a env = "nat => 'a option"

which is better a definition in theory did not solve the problem.

Answer 1

On the right-hand side of a datatype definition, you normally list the constructors of the datatype. In your example, you have not written any constructor, so datatype thinks that you want to call it nat => 'a option, which is not a legal name for a constructor or any other Isabelle constant.

If you just want to introduce env as a type abbreviation for nat => 'a option, type_synonym is what you are looking for.

type_synonym 'a env = "nat => 'a option"

Note that you have to repeat all type variables on the left-hand side. Then, 'a env and nat => 'a option can be used interchangeably. If you want to introduce a new type constructor for env, then you must provide a constructor name such as Env:

datatype 'a env = Env "nat => 'a option"