时间戳

首页 > 解决方案 > Isabelle/ZF 中缀定义问题

isabelle - Isabelle/ZF 中缀定义问题

问题描述

我试图定义这样的定义：

theory intext
imports ZF.Int
begin

definition zmod :: "[i,i] ⇒ i" (infixl "$//" 69)
where 
  "a $// b == 0"

但是，它在“$//”和“a $// b == 0”中显示错误：

Inner syntax error⌂
Failed to parse prop

我试图查看 ZF.Int 中是否有中缀定义，我确实找到了，但 Isabelle 一开始就在理论中显示错误：

Cannot update finished theory "ZF.Int"

我可以知道有没有人在 Isabelle/ZF 中使用中缀运算符定义定义的经验可以给我一些建议？

标签： isabelle

解决方案

该字符/是 mixfix 注释中的特殊字符，因此您需要使用'以下方法对其进行转义：

definition zmod :: "[i,i] ⇒ i" (infixl "$'/'/" 69)
where 
  "a $// b == 0"

有关 mixfix 注释的更多信息，请参阅Isabelle/Isar 参考手册，第 8.2 节。

关于错误消息Cannot update finished theory "ZF.Int"，这意味着它Int是 ZF 的一部分，无法编辑。

推荐阅读