isabelle - 有没有办法获得 Isabelle 的各种运算符/构造函数的完整列表？

Question

例如，Isabelle 可以将“and”表示为“^”，“or”表示为“v”……有没有办法获得所有这些类型的运算符/构造函数的完整列表？

Answer 1

有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))"

发现这些符号的更常用方法是

尝试明显的符号(对于很多事情，这正是人们所期望的，就像上面的函数组合的情况一样)。

找出常量的名称，然后环顾定义它的地方，看看为它设置了什么符号。