试图了解在伊莎贝尔“语法”关键字/ HOL

Question

我想了解实施伊莎贝尔/ HOL线性逻辑：https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/ILL.html对于不syntax关键字代表什么，什么是代码的意思是：

syntax 
    "_Trueprop" :: "single_seqe" ("((_)/ ⊢ (_))" [6,6] 5) 
    "_Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5) 
    "_PromAux" :: "three_seqe" ("promaux {_||_||_}") 

我在哪里可以找到syntax关键字的文档？关于infixr以及计算机科学讲义第828卷中的翻译规则，我找到了详尽的文档。但是我找不到关于syntax的类似文档。

Answer 1

这在参考手册的8.5.2节（截至2016年1月1日）中描述：“原始语法和翻译”。

这里的第一行表示添加语法规则，表示P ⊢ Q解析为_Trueprop P Q。​​的下一行给出parse_translation，稍后在参考手册的相同章节中进行描述。该翻译告诉Isabelle将_Trueprop翻译为K (single_tr Trueprop)，并将Trueprop声明为文件顶部的未解释常量。你会看到还有一个print_translation，它控制漂亮的打印机。