输入以下定义
datatype env = "nat => 'a option"
isabelle/jedit显示了感叹号，并说
Legacy feature! Bad name binding: "nat => 'a option"
问题是什么，我该如何修复此类型的同义词？
更新：甚至
datatype 'a env = "nat => 'a option"
这是理论上更好的定义不能解决问题。
在datatype定义的右侧，通常列出数据类型的构造函数。在您的示例中，您尚未写任何构造函数，因此datatype认为您要称其为nat => 'a option，这不是构造函数或任何其他Isabelle常数的合法名称。
如果您只想引入env作为nat => 'a option的类型缩写，则type_synonym是您要寻找的。
type_synonym 'a env = "nat => 'a option"
请注意，您必须在左侧重复所有类型变量。然后，'a env和nat => 'a option可以互换使用。如果要引入env的新类型构造函数，则必须提供一个构造函数，例如Env：
datatype 'a env = Env "nat => 'a option"