避免在带有普通证明的Coq中打印符号

Question

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

string_dec
获取：

string_dec
     : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}
然后，他继续查看+的定义，但在此之前，他在CoqIde中禁用了符号的打印。这样就可以打印摘要了。可以检查最后一个符号。

如何使用普通证明做同样的事情？

在DeepSpec 2018的第6讲中，讲师检查string_dec的定义，以获得：string_dec：forall s1 s2：string，{s1 = s2} + {s1 <> s2}然后他继续观察...] >

Answer 1

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

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