Isabelle：mixfix 注释中的优先级太多

问题描述

我正在 Isabelle 教程 (2020) pp6 中试验以下示例 classes.pdf。 我已尽力将 PDF 内容翻译成校对文本，例如将 PDF 中的 α 更改为 'a、添加引号等。

class group = monoidl +
  fixes inverse :: "'a ⇒ 'a" ("(-÷)" [1000] 999)
  assumes invl : "x ÷ ⊗ x = ?"

然而，上面的定义仍然没有解析，出现错误：

Too many precedences in mixfix annotation

我不确定应该如何声明逆符号。到目前为止，我只遇到过中缀表示法。

有人可以帮助解释如何修复示例中的“mixfix”注释？

解决方法

根据 Isabelle sources of the document，它是下划线，而不是连字符：

class group = monoidl +
  fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>"    ("(_\<div>)" [1000] 999)
  assumes invl: "x\<div> \<otimes> x = \<one>"

用连字符替换下划线是文档生成的一个特性。连字符看起来比下划线更好看（至少在模式中）。