Clément Pit-Claudel (May 19 2020 at 21:18): 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. *)
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: Apr 18 2024 at 04:02 UTC