I have a development on labeled transitions which declares a notation "x -- L --> y". Now I find I need to `Require Import Setoid.`

, but then my --> notations no longer work. (`Syntax error: '-->' expected after [term level 200] (in [term]).`

).

Is there a way out other than changing my notation to something else?

if you understand LL parsing and left factoring well enough, you might be able to make your notation and Setoid’s one coexist.

or you can post your grammar (at least your `Reserved Notation`

) and some people here can help.

and sorry for the poor phrasing: what I meant is that Coq notations are harder to use than they should, and in particular they are not very modular. The needed tricks _are_ documented, but they’re not easy to apply.

this is the key section: https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simple-factorization-rules

oh, there’s a simpler alternative: using `Require Setoid`

does not enable `Setoid`

’s notations!

then you can use `Setoid….`

(when that works), or import `Setoid`

locally (inside `Section`

). Not ideal but might be enough sometimes.

for the “tweaking grammars” part, looking at https://github.com/coq/coq/blob/dc405d2cfabd794939e505a77890e4acbf229f0f/theories/Classes/Morphisms.v#L103-L104 does not explain the failure alone… one would need an example to investigate further. Declaring your notation with `Reserved Notation … (<all the notation properties>).`

should be enough to reproduce the conflict.

Thanks a lot, that's very helpful!

Last updated: Jun 18 2024 at 21:01 UTC