问题描述
在 Isabelle (2020) 理论文件中输入证明陈述,例如
from ‹prime p › have p: "1 < p "
当我输入引号时,jEdit 界面应用程序会弹出一个工具提示,提供插入一个打开的 cartouche 命令 \<open>
。正如您在上面的行中看到的,我一直允许这样做,而且似乎是允许的。 Isabelle 文档似乎将内部语法视为嵌入的类别,这似乎允许用引号或涡旋外壳 \<open ... \<close>.
这样做有不利的一面吗? imports
语句需要引用对具有 module.theory 格式的理论文件“HOL-computational_Algebra.Primes”的引用,并且不会在那里接受旋转图案,但在理论上它似乎是等效的。
解决方法
Cartouches 与引号目前是样式问题,但导入、语法定义和某些命令参数(如 nitpick[eval=".."]
)除外。
请注意,某些键盘布局可以直接输入它们(例如,mac US international)。
我相信 Makarius 最终会弃用引号。这将允许用户为字符串编写 "a"
而不是 ''a''
)。但不要指望这会很快发生。
所以:写下你最喜欢的!