coq - 如何在 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 设为 ∀ 并展开我的符号。

我按照 Coq Reference Manual 中的指示尝试了 Set Printing Notations 但这没有做任何事情，也没有启用

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

Answer 1

Printing Notations 的有趣之处在于您实际上必须对其进行 Unset。

Unset Printing Notations.

Here's where the manual hints at it :

Printing Notations:
Controls whether to use notations for printing terms wherever possible. Default is on.