如何解决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>"
用连字符替换下划线是文档生成的一个特性。连字符看起来比下划线更好看(至少在模式中)。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。