伊莎贝尔的名字装订不好

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"