The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

[Print Grammar constr] informs me that QArith defined [p ~ 0] and [p ~ 1] at level 7.  So your notation must be at level 7 or lower to override this; putting your notation at level 7 makes the code go through.

The issue is that Coq uses OCaml's parser to parse things, and it is not very robust.

-Jason

On Sat, Jun 7, 2014 at 4:25 PM, Chris Dams <chris.dams.nl AT gmail.com> wrote:

Hello all,

Here is a simplified example of what I am trying to do.

Require Import QArith.

Parameter bla: nat -> nat -> Prop.

Notation "A ~ B" := (bla A B) (at level 70).

Parameter bla_equal:
   forall c: nat,
   c ~ c.

Coq (version 8.3pl2) reacts to the last line by saying "Syntax error: '0' or '1' expected after '~' (in [constr:operconstr])".

Apparently this is due to the fact that because of the QArith import a notation that involves "~" is defined. I tried various ways of getting around this. E.g., trying "Close Scope positive", trying to put my notation in a scope and opening that and so forth. None of this seems to help. Any ideas?

All the best,
Chris