coq-community/coq-ext-lib

Functor and Monad notations conflict

Closed this issue · 3 comments

jbaum98 commented

Both Functor and Monad notations are declares at level 51, but Functor notation is left associative while Monad notation is right associative. I've solved this locally by changing the Functor notations to level 52, so if that's the right approach I'm happy to submit the tiny PR.

gmalecha commented

That is probably the right way to go. There is a convention in Coq to use even and odd numbers for left and right associative entries, but I don't recall which is which. Can you confirm in the standard library and make a PR?

jbaum98 commented

Based on https://coq.inria.fr/library/Coq.Init.Notations.html, I guess it would be that even is left and odd is right, but this is not such a strict convention (see ^)

Reserved Notation "x + y" (at level 50, left associativity).
Reserved Notation "x - y" (at level 50, left associativity).
Reserved Notation "x * y" (at level 40, left associativity).
Reserved Notation "x / y" (at level 40, left associativity).
Reserved Notation "- x" (at level 35, right associativity).
Reserved Notation "/ x" (at level 35, right associativity).
Reserved Notation "x ^ y" (at level 30, right associativity).

Another example of even right at https://coq.inria.fr/library/Coq.Init.Datatypes.html

Infix "::" := cons (at level 60, right associativity) : list_scope.
gmalecha commented

Alright, let's do that even left, odd right. Can you make a PR?

  • 👍1