问伊莎贝尔中的恶名绑定
EN

Stack Overflow用户

提问于 2014-01-23 16:02:51

回答 1查看 536关注 0票数 4

输入以下定义时

datatype env = "nat => 'a option"

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

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

有什么问题，我如何修复这种类型的同义词？

更新:偶数

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

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

回答已采纳

发布于 2014-01-23 17:09:17

在datatype定义的右侧，通常会列出数据类型的构造函数。在您的示例中，您没有编写任何构造函数，因此datatype认为要将其命名为nat => 'a option，它不是构造函数或任何其他伊莎贝尔常量的合法名称。

如果您只想将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"

票数 5

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/21313331

复制

相似问题

问伊莎贝尔中的恶名绑定EN