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

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.并在缓冲区中对其求值。这也使您可以访问仅禁用打印符号的Unset Printing Notations (这是您可以使用CoqIDE中的菜单执行的操作)。完成后，您可以删除此命令，这将撤消其效果。

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