区域设置定义生成两个解析树

Question

以下是我在Isabelle:中的简单区域设置定义

locale sig =
fixes le:: "'a ⇒ 'a ⇒ bool" (infixl "≤" 50)
assumes refl: "x ≤ x"

现在，我收到一条错误消息：

Ambiguous input⌂ produces 2 parse trees:
("<^const>HOL.Trueprop"
("<^const>Orderings.ord_class.less_eq" ("_position" x) ("_position" x)))
("<^const>HOL.Trueprop" ("<^fixed>le" ("_position" x) ("_position" x)))
Ambiguous input
2 terms are type correct:
(x ≤ x)
(x ≤ x)
Failed to parse prop

我与内置的less或equal运算符有冲突吗？

我该怎么解决这个问题？

Answer 1

≤运算符是在ord类型类中定义的，所以您可以扩展这个类：

class sig = ord +
assumes refl: "x ≤ x"

其他替代方案：

• 不导入ord的定义
• 使用no_notation Orderings.ord_class.less_eq ("(_/ ≤ _)" [51, 51] 50)隐藏现有的表示法(请参阅隐藏运算符以避免AST中的歧义(
• 使用其他名称或符号