避免使用Proof General在Coq中打印注释

Question

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

string_dec

获取：

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

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

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

Answer 1

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

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

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