The Coq mailing list

[Jakob Botsch Nielsen <jakob.botsch.nielsen AT gmail.com>]

Hi,

In experimenting with notations I have come up with an example I am having

trouble understanding. See the following Coq program:

Close Scope core_scope.

Close Scope function_scope.

Close Scope type_scope.

Close Scope nat_scope.

Print Visibility.

(* Empty: no other notations to conflict with *)

Notation "[ x ]" := x.

(* "Setting notation at level 0." *)

(* A: *)

Notation "x [ proj := v ]" := O (at level 12, left associativity).

(* B: *)

(*Notation "x [ proj := v ]" := O (at level 10, left associativity).*)

Print Visibility.

(*

Lonely notations

"[ x ]" := x

"x [ proj := v ]" := O

*)

Definition example := O [ _ := _ ].

Here is the behavior with Coq 8.9.0:

* If the "[ x ]" notation is not defined, then the example works with either of

  A or B (so level 10 or level 12 does not matter).

* If the "[ x ]" notation is defined, then the definition of A (at level 12) is

  fine, but parsing of the example fails.

* If the "[ x ]" notation is defined, then the definition of B (at level 10) is

  fine, and the example parses fine.

Why does the definition of "[ x ]" (which is a notation at level 0) affect the

other notation in this way?

Best,

Jakob