Stream: Coq users

Topic: Disable specific notation (Coq 8.13.2)


view this post on Zulip spaceloop (Jul 28 2023 at 14:29):

Hi, I would like coq to stop printing specific notation in my goal. The notation lives in a certain scope. I would have expected that Close Scope does this, but it behaves differently:

Close Scope nat_scope.
Goal ge 1 0.

Now it still prints

1 subgoal

========================= (1 / 1)
(1 >= 0)%nat

(I would like it to print just ge 1 0, but keep other notation, so not use Unset Printing Notations).

I'm on Coq 8.13.2, so unfortunately I don't have the Disable Notation command yet. Is there another way to do this?

view this post on Zulip Li-yao (Jul 28 2023 at 14:40):

Try making a new notation to override the existing one Notation ge := ge.

view this post on Zulip Pierre Courtieu (Jul 31 2023 at 10:08):

To me this looks like a bug, but it is an old one, so there must be an explanation.
Meanwhile this works: Disable Notation "_ >= _": nat_scope.

view this post on Zulip Paolo Giarrusso (Jul 31 2023 at 11:06):

After Close Scope, (1 >= 0)%nat still parses, as intended, and you can also use closed scopes via at least Bind Scope, Arguments, and notations wrapping uses of %key. The "bug" is just to use the notations during pretty-printing as well.

view this post on Zulip Paolo Giarrusso (Jul 31 2023 at 11:08):

Maybe you'd like pretty-printing to never use %, but using % seems a crucial feature when proving theory relating Nat, N and Z.

view this post on Zulip Pierre Courtieu (Jul 31 2023 at 11:19):

Yes the printing of ˋgeˋ with <= is surprising.

Le lun. 31 juil. 2023 à 13:10, Zulip notifications <noreply@zulip.com> a
écrit :

view this post on Zulip Jason Gross (Aug 04 2023 at 03:38):

Try Close Scope nat_scope. Undelimit Scope nat_scope. (Note that if you Unbind Scope nat_scope. or w/e, you'll lose the notation for numerals in your goal.)


Last updated: Oct 13 2024 at 01:02 UTC