Hi! We're working on incorporating Custom Entry notations into the next version of Software Foundations and have been running into an issue with Reserved Notation and Custom Entries.
It looks like there isn't a way to use
Reserved Notation while using
Custom Entries, as far as we can tell.
Declare Custom Entry example. Reserved Notation " x '==' 1 " (in custom example at level 0, x constr). Fail Fixpoint stupid (x : nat) : nat := 1 where " x '==' 1" := (stupid x).
There is no way to specify the modifier for custom entries for the definition of
stupid, because the Coq syntax accepts notation interpretation scopes but not
modifiers on the where clause. It would make things cleaner if we could use reserved notation for the custom entries grammar here. Is the observation that Coq currently doesn't support this correct?
For reference, this is on
8.12.dev, and previous versions of Coq (>=
8.9.0) also demonstrate this behavior.
This bug has been filed as an issue and has been addressed by the developers. :-) Sorry for posting a bug report here!
Last updated: Oct 04 2023 at 23:01 UTC