Stream: Coq users

Topic: (Bug?) Reserved Notation and Custom Entries


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

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

view this post on Zulip 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: Jan 27 2023 at 00:03 UTC