## Stream: Coq users

### Topic: Parsing levels

#### Clément Pit-Claudel (May 19 2020 at 21:18):

Hi all. Can someone explain why the following makes sense? Print Grammar Constr says level 9 is LEFTA, but then complains that it's right associative:

Print Grammar constr. (* | "9" LEFTA *)
Notation "'Ob'" := 0 (at level 9, left associativity). (* Works *)
Notation "'A' x" := (x + x) (at level 9, left associativity). (* Fails *)
(* The command has indeed failed with message: *)
(* Level 9 is already declared right associative while it is now expected to be left associative. *)

#### Kenji Maillard (May 19 2020 at 21:33):

I don't have a clue why it happens but It's probably related to the content of level 9, if you try with the (empty in my case) level 8:

Notation "'A' x 'A'" := (x + x) (at level 8, left associativity). (* Works *)
Notation "'B' x" := (x + x) (at level 8, left associativity). (* Fails  but works if you remove the previous line *)

and in the level 9 there seem to be a notation along the lines of "'..' something '..'".

#### Clément Pit-Claudel (May 20 2020 at 01:27):

Huh, I didn't realize the second one would fail either

#### Clément Pit-Claudel (May 20 2020 at 01:34):

https://github.com/coq/coq/issues/12373

#### Paolo Giarrusso (May 20 2020 at 11:48):

For these sort of questions I often end up browsing the camlp5 manual

#### Paolo Giarrusso (May 20 2020 at 11:49):

actually, I’d first read carefully the chapter on notations of the Coq reference manual, and then if that fails go to camlp5.

#### Paolo Giarrusso (May 20 2020 at 11:51):

If you want to define notations which partially overlap, you also need to read about left-factoring and understand how LL(1) parsing works...

#### Paolo Giarrusso (May 20 2020 at 11:52):

(it sounds like this specific issue is an actual bug, but that’s the advice that I wish I got an year ago, so hope it helps somebody)

#### Clément Pit-Claudel (May 20 2020 at 14:00):

Paolo G. Giarrusso said:

actually, I’d first read carefully the chapter on notations of the Coq reference manual, and then if that fails go to camlp5.

Yup, I've done that many times :)

Last updated: Jun 24 2024 at 12:02 UTC