有没有办法获得Isabelle各种运营商/构造商的完整列表？

如何解决有没有办法获得Isabelle各种运营商/构造商的完整列表？

例如，伊莎贝尔（Isabelle）可以将“ and”表示为“ ^”，“ or”表示为“ v” .....是否可以获取所有这些运算符/构造函数的完整列表？>

解决方法

有print_syntax命令，但其输出可能看起来有些吓人。但是，例如，以下行

logic(55) = logic(55) "∘" logic(56) ⇒ "\<^const>Fun.comp

告诉您符号∘是一个前缀运算符，其优先级55映射到常数Fun.comp。相应的声明是这样的：

definition comp :: "('b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c"  (infixl "∘" 55)
  where "f ∘ g = (λx. f (g x))"

发现这些符号的更常见的方式是

1. 尝试一种明显的表示法（在很多事情上，这正是人们所期望的，就像上面的函数组成一样）。

2. 找出常量的名称，然后在定义该常量的地方四处查看，以查看为该常量设置的符号。

,

我不知道。

一个很好的起点是all symbols in Main的列表。但是，它不包含所有符号，也没有提供从符号到定义的映射。

通常，查找事物的缩写不是那么有用：

• 如果有符号，则可以单击它以找到定义。
• 如果您有符号并且不知道如何键入，可以转到Isabelle / jEdit的符号面板以查看如何键入。
• 如果有定义，只需键入term "and a b"，输出将显示带有符号的版本。

因此，真正的问题是如何找到正确的定义，而不是如何找到正确的符号。但这要困难得多。