Irene Yoon (Jun 15 2020 at 03:19): Irene Yoon (Jun 15 2020 at 03:19):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.
For instance,
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?
Irene Yoon (Jun 15 2020 at 03:25):For reference, this is on 8.12.dev, and previous versions of Coq (>= 8.9.0) also demonstrate this behavior.
Irene Yoon (Jun 19 2020 at 15:04):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 13 2024 at 01:02 UTC