坏名伊莎贝尔

Question

结合当进入以下定义

datatype env = "nat => 'a option" 

伊莎贝尔/ 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"