隐藏运算符以避免AST中的歧义

Question

我正在尝试官方Isabelle教程中的列表示例.我将#with :和@with 替换为与++Haskell具有相同的语法.现在我收到有关AST中含糊不清的警告.我知道我可以隐藏函数,hide_const但这对于中缀表示法的运算符不起作用.我怎样才能隐藏Isabelle的操作员？

确切的警告信息是:

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.

Answer 1

隐藏运营商不会删除其表示法.有一个单独的命令no_notation可以删除现有的表示法.在伊莎贝尔/ HOL,++势必map_add如可以从模糊度警告中看到.您可以按如下方式删除它.

no_notation map_add (infixl "++" 100)

请注意,必须重复已声明要删除的表示法的确切优先级参数.没有简单的方法可以找到常量的符号声明,但是声明符号接近常量声明是很好的方式; Ctrl - 点击一个常量会转到它的声明.

关于:,这是默认绑定的Set.member.您可以删除它no_notation Set.member ("(_/ : _)" [51, 51] 50).

除非出于演示或探索目的,我建议不要过多地更改Isabelle的默认语法.否则,其他Isabelle用户会发现很难阅读您的代码,而您的理论也不会与其他人相容.原因在于,在导入不同理论时,符号会相加合并.因此,如果你删除符号++的map_add理论A与理论B进口理论A和来自其他一些理论Main,但没有A,那么不确定性的++是早在理论上B.