coq - 避免在 Coq 中使用 Proof General 打印符号

Question

在 DeepSpec 2018 的第 6 讲中，讲师检查了

string_dec

获得：

string_dec
     : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}

然后他继续查看 + 的定义，但在此之前，他在 CoqIde 中禁用了符号的打印。这样 sumbool 就被打印出来了。可以检查最后一个符号。

我怎样才能用 Proof General 做同样的事情？

Answer 1

您可以使用菜单，Coq > OPTIONS > Set Printing All。

您也可以直接发出命令，Set Printing All.在运行 Check 命令之前在缓冲区中键入和评估它。这也使您可以访问Unset Printing Notations仅禁用打印符号（您可以使用 CoqIDE 中的菜单执行此操作）。完成后，您可以删除此命令，这将撤消其效果。

最后，你也可以直接使用Coq > OTHER QUERIES > Check (show all)on string_dec。