Stream: Coq users

Topic: How to replace one notation with another project-wide


view this post on Zulip walker (Apr 26 2023 at 07:36):

So in mathcomp:

From mathcomp Require Import all_ssreflect.
Locate "\o".
(*Notation "f1 \o f2" := (comp f1 f2) : fun_scope (default interpretation)*)

But in a file called utils.v I have :

Notation " g ∘ f " := (comp g f) (at level 40, left associativity).

Now I want t force coq to disable that other notation from mathcomp so it does not appear in interactive proofs, how can i do that?

Ideally I would want to do it so that it is reflected on every file that imports mathcomp.

view this post on Zulip Pierre Roux (Apr 26 2023 at 08:07):

You should probably look for Disable Notation in the manual (available since Coq 8.17).

view this post on Zulip walker (Apr 26 2023 at 08:22):

thanks, unfortunately today is not the day I move to 8.17 because I am using mathcomp 2.0 and it didn't compile on 8.17, but thanks, I wll bookmark this for when I upgrade

view this post on Zulip Pierre Roux (Apr 26 2023 at 08:24):

Just use the hierarchy-builder branch instead of the alpha mathcomp-2 tag, this currently supports Coq 8.16, 8.17 and master.


Last updated: Jun 20 2024 at 13:02 UTC