Определение локали создает два дерева синтаксического анализа

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-or- оператор равенства?

Как это исправить?

Answer 1

Оператор ≤ определен в классе типов ord, поэтому вы можете просто расширить этот класс:

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

Другие альтернативы:

• Не импортируйте определение ord
• Скрыть существующую нотацию с помощью no_notation Orderings.ord_class.less_eq ("(_/ ≤ _)" [51, 51] 50) (см. операторы скрытия, чтобы избежать двусмысленности в AST )
• Используйте другое имя или символ