如何解决我们可以在 jEdit Isabelle/HOL 会话中使用旋转图标而不是引号来描述内部语法吗
在 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''）。但不要指望这会很快发生。
所以：写下你最喜欢的！
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
