如何在 Coq 中暂时禁用符号

Question

当您熟悉一个项目时，符号很方便，但当您刚开始使用代码库时可能会感到困惑。我知道你可以用白话关闭所有符号Set Printing All。但是，我想保留一些打印功能，例如隐式参数。全部打印如下：

Require Import Utf8_core. 
Set Printing All.
Theorem contradiction_implies_anything : forall P Q : Prop,
  (P /\ ~P) -> Q.
Proof.

给出以下证明状态：

1 subgoal (ID 120)

  ============================
  forall (P Q : Prop) (_ : and P (not P)), Q

这几乎是没有，但我想的_要被删除，forall是?和刚刚展开我的符号。

我Set Printing Notations按照Coq 参考手册中的说明进行了尝试，但没有做任何事情，也没有启用

Set Printing Implicit.
Set Printing Coercions.
Set Printing Synth.
Set Printing Projections.

Answer 1

有趣的Printing Notations是，您实际上必须这样Unset做。

Unset Printing Notations.

这是手册提示的地方：

Printing Notations：
控制是否尽可能使用符号来打印术语。默认开启。