有没有办法获得 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))"

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

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

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