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?
Try making a new notation to override the existing one Notation ge := ge.
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.
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.
Maybe you'd like pretty-printing to never use %, but using % seems a crucial feature when proving theory relating Nat, N and Z.
Yes the printing of ˋgeˋ with <=
is surprising.
Le lun. 31 juil. 2023 à 13:10, Zulip notifications <noreply@zulip.com> a
écrit :
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