如何临时禁用Coq中的符号 [英] How to temporarily disable notations in Coq

问题描述

当您熟悉项目时，表示法很方便，但当您刚开始使用代码库时，可能会感到困惑。我知道您可以关闭所有带有白话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 Reference Manual所示，但这没有任何作用，也没有启用

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

推荐答案

Printing Notations有趣的是，您实际上必须Unset它。

Unset Printing Notations.

Here's where the manual hints at it：

Printing Notations：
控制是否尽可能使用表示法打印术语。默认为启用。

这篇关于如何临时禁用Coq中的符号的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！