isabelle - Isabelle 中的错误名称绑定(bind)

Question

输入以下定义时

datatype env = "nat => 'a option"

Isabelle/jedit 显示一个感叹号并说

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

有什么问题，我该如何解决这种类型的同义词？

更新:甚至

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

哪个更好，理论上的定义并没有解决问题。

Answer 1

在 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"