Hello,

I am fairly new to this and sorry if it has some obvious solution I did not find. Is there a way to know if a binary infix notation is left or right associative ?

I only know of `Locate "+".`

for instance, but it does not display this information (priority is also hidden).

I also don't know. As a workaround, you can temporarily `Set Printing Parentheses.`

to find out.

Try using `Print Grammar constr.`

(see here for details https://coq.inria.fr/refman/user-extensions/syntax-extensions.html)

I

My hack for finding the priority is to (try to) redefine the notation at some random level. For example:

```
Notation "a + b" := (a - b) (at level 0).
```

Since "+" is not actually defined at level 0, Coq complains with a very informative message:

```
Error: Notation "_ + _" is already defined at level 50 with arguments constr
at level 50, constr at next level while it is now required to be at level 0
with arguments constr at next level, constr at next level.
```

you should see something like this:

```
| "95" RIGHTA
[ SELF; "<->"; NEXT ]
```

where the number (`95`

here) is the precedence (lower will be parsed first), then `RIGHTA`

tells you it's rigth associative and then you see the notation (in this case `<-->`

).

Actually we could do much better, unless I'm missing something, we could add some kind of `Print Notation`

command; that kind of functionality is exposed in serapi, so users can do:

```
(Query () (Unparsing "_ + _"))
(Answer 0 Ack)
(Answer 0
(ObjList
((CoqUnparsing
(((UnpBox (PpHOVB 0)
((() (UnpMetaVar (LevelLe 50) (Left))) (() (UnpTerminal " +"))
(() (UnpCut (PpBrk 1 0))) (() (UnpMetaVar (LevelLt 50) (Right))))))
50)
()
(((notgram_level (InConstrEntry 50 ((LevelLe 50) (LevelLt 50))))
(notgram_assoc (LeftA)) (notgram_notation (InConstrEntry "_ + _"))
(notgram_prods
(((GramConstrNonTerminal
(ETProdConstr InConstrEntry
((NumLevel 50) (BorderProd Left (LeftA))))
((Id x)))
(GramConstrTerminal (PKEYWORD +))
(GramConstrNonTerminal
(ETProdConstr InConstrEntry
((NumLevel 50) (BorderProd Right (LeftA))))
((Id y))))))
(notgram_typs
((ETConstr InConstrEntry () ((NumLevel 50) (BorderProd Left (LeftA))))
(ETConstr InConstrEntry ()
((NumLevel 50) (BorderProd Right (LeftA))))))))))))
```

you can see the full info in the several records. So maybe indeed worth opening a bug to put this code into Coq.

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

Thanks @Ana de Almeida Borges

There is `Print Grammar constr.`

which prints the current grammar of Gallina terms.

See https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.Print-Grammar.

@Pierre Rousselin we ended up implementing `Print Notation`

, so from Coq 8.16 on you can just use it to find these things out!

Great ! Thanks a lot !

Last updated: Jun 20 2024 at 12:02 UTC