Jonas Oberhauser (Oct 28 2021 at 13:54): Jonas Oberhauser (Oct 28 2021 at 13:54):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?
Paolo Giarrusso (Oct 28 2021 at 23:55):if you understand LL parsing and left factoring well enough, you might be able to make your notation and Setoid’s one coexist.
Paolo Giarrusso (Oct 28 2021 at 23:56):or you can post your grammar (at least your Reserved Notation) and some people here can help.
Paolo Giarrusso (Oct 28 2021 at 23:58):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.
Paolo Giarrusso (Oct 28 2021 at 23:59):this is the key section: https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simple-factorization-rules
Paolo Giarrusso (Oct 29 2021 at 00:02):oh, there’s a simpler alternative: using Require Setoid does not enable Setoid’s notations!
Paolo Giarrusso (Oct 29 2021 at 00:03):then you can use Setoid…. (when that works), or import Setoid locally (inside Section). Not ideal but might be enough sometimes.
Paolo Giarrusso (Oct 29 2021 at 00:06):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.
Jonas Oberhauser (Oct 29 2021 at 10:23):Thanks a lot, that's very helpful!
Last updated: Oct 13 2024 at 01:02 UTC