如何用ASCII编写isabelle迭代隐含

Question

在学习Isabelle (2020)时，我试图将文档中的一个示例复制到一个包含迭代含义的.thy文件中。由于文档是PDF格式的，我不知道它的正确ASCII应该是什么。我能得到的最接近的结果是：

lemma "[[ xs @ ys = ys @ xs ; length xs = length ys]]   ==> xs = ys"

但是Isabelle抱怨“内部语法错误”。我尝试使用"...;..."，但Isabelle似乎将其视为一个列表，并抱怨列表和bool之间的冲突。

如何在ASCII中键入公式？

一般来说，如何从PDF文档中找到表示法的ASCII？有什么地方有查询表吗？

Answer 1

这些符号的名称是\<lbrakk>和\<rbrakk>。对应的Unicode字符是⟦和⟧。如果你在Isabelle/jEdit中输入[|或|]，它会自动转换成它们。

从PDF中复制代码几乎永远不会起作用；PDF是一种非常糟糕的格式。

一个很好的查找符号的地方是Isabelle/jEdit中的‘symbols’选项卡。例如，你可以在“标点符号”部分找到这些括号。还有一个~~/etc/symbols文件，但我不认为它对这种情况有什么帮助，因为它只显示Unicode代码点，而不显示字符本身。