Stream: Coq users

Topic: Setoid notation clash?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 00:02):

oh, there’s a simpler alternative: using Require Setoid does not enable Setoid’s notations!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jonas Oberhauser (Oct 29 2021 at 10:23):

Thanks a lot, that's very helpful!


Last updated: Jan 31 2023 at 13:02 UTC