我正在尝试伊莎贝尔官方教程中的列表示例。我更换了# with :和@ with ++具有与 Haskell 相同的语法。现在我收到有关 AST 中含糊之处的警告。我知道我可以隐藏功能hide_const但这对于中缀表示法的运算符不起作用。如何在伊莎贝尔中隐藏操作员？
确切的警告消息是：
Ambiguous input⌂ produces 2 parse trees:
("\<^const>HOL.Trueprop"
("\<^const>HOL.eq" ("\<^const>Map.map_add" ("/<^const>toylist.list.Nil") ("_position" ys))
("_position" ys)))
("\<^const>HOL.Trueprop"
("\<^const>HOL.eq" ("\<^fixed>app" ("\<^const>toylist.list.Nil") ("_position" ys)) ("_position" ys)))
Fortunately, only one parse tree is well-formed and type-correct,
but you may still want to disambiguate your grammar or your input.
隐藏运算符不会删除其符号。有一个单独的命令no_notation删除现有的注释。在伊莎贝尔/HOL，++一定会map_add从歧义警告可以看出。您可以按如下方式删除它。
no_notation map_add (infixl "++" 100)
Note that you must repeat the exact precedence parameters with which the notation to be deleted has been declared. There is no easy way to find the notation declaration for a constant, but it is good style to declare notation close to the declaration of the constant; Ctrl-clicking on a constant takes you to its declaration.
关于:，默认情况下绑定到Set.member。您可以使用以下命令删除它no_notation Set.member ("(_/ : _)" [51, 51] 50).
除非出于演示或探索目的，否则我建议不要过多更改 Isabelle 的默认语法。否则，其他 Isabelle 用户会发现很难阅读您的代码，并且您的理论将与其他人不兼容。原因是当导入不同的理论时，符号会相加地合并。因此，如果删除该符号++ for map_add理论上A和理论B导入理论A以及其他一些理论源自Main但不是A，那么模糊度为++回到理论上B.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
