Menu
Notations are convenient when you're familiar with a project but can be confusing when you're just starting with a code base. I know you can turn off all notations with the vernacular Set Printing All. However, I want to keep some printing off, such as implicit arguments. Printing all as follows:
Require Import Utf8_core.
Set Printing All.
Theorem contradiction_implies_anything : forall P Q : Prop,
(P /\ ~P) -> Q.
Proof.
gives the following proof state:
1 subgoal (ID 120)
============================
forall (P Q : Prop) (_ : and P (not P)), Q
Which is almost there, but I would like the _ to be removed and the forall to be ∀ and just unfold my notations.
I tried Set Printing Notations as indicated in the Coq Reference Manual but that didn't do anything, nor did enabling
Set Printing Implicit.
Set Printing Coercions.
Set Printing Synth.
Set Printing Projections.
348
These are the notations whose level and associativity is imposed by Coq Reserved Notation "x <-> y" (at level 95, no associativity). Reserved Notation "x /\ y" (at level 80, right associativity). Reserved Notation "x \/ y" (at level 85, right associativity).
To deal with the ambiguity of notations, Coq uses precedence levels ranging from 0 to 100 (plus one extra level numbered 200) and associativity rules. Consider for example the new notation Notation "A \/ B" := (or A B). Clearly, an expression such as forall A:Prop, True /\ A \/ A \/ False is ambiguous.
It is sometimes expected that the same symbolic notation has different meanings in different contexts; to achieve this form of overloading, Coq offers a notion of notation scopes . The main command to provide custom notations for tactics is Tactic Notation.
In Unicode, one can use combining characters like ⃗that combine with a regular character and puts the arrow on top. Since Coq notations ignore whitespace, it is possible to define the following notation: Notation "x ⃗" := x (x global). This then allows you to parse notations like x⃗ y⃗and z⃗as Coq variables x yand z.
The funny thing about Printing Notations is that you actually have to Unset it.
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.
136
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
