Stream: Coq users

Topic: Overriding stdlib pairs

James Wood (Oct 31 2022 at 10:44):

In my project, I'm using some parts of the standard library, but I want to replace its products by my own definition which obeys η-rules. What is the best way to do this? At the moment, I have the following, but wherever I import the definition, I get an annoying warning Warning: Notation "_ * _" was already used in scope type_scope. [notation-overridden,parsing]. I provide the code only to illustrate what I'm doing, not to ask for a minimal change to it that will make the specific warning go away.

#[global] Set Primitive Projections.

Record prod {A B : Type} : Type := pair {
  prl : A;
  prr : B;
}.
Arguments prod A B : clear implicits.
Arguments pair {A B} & prl prr.

Notation "A * B" := (prod A B) : type_scope.
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.

Karl Palmskog (Oct 31 2022 at 10:47):

Set Warnings "-warning-to-suppress-temporarily".
<code with warning goes here>
Set Warnings "warning-to-suppress-temporarily".

James Wood (Oct 31 2022 at 10:52):

This seems to still leave warnings at every Require where these notations were defined (unless I wrap each Require in the same pattern, which I don't really want to do).

Karl Palmskog (Oct 31 2022 at 10:53):

you can suppress warnings at "project level" by putting the following in _CoqProject (there is similar for Dune):

-arg -w -arg -notation-overridden

James Wood (Oct 31 2022 at 10:54):

Is this really the best solution? It throws the baby out with the bath water.

Karl Palmskog (Oct 31 2022 at 10:55):

you can of course do your own build where you send specific flags to coqc for specific files

James Wood (Oct 31 2022 at 10:59):

That wouldn't help because I want to override prod everywhere. But thanks for the suggestions. If turning the entire warning off is the best I can do, I guess that's what I'll do.

Gaëtan Gilbert (Oct 31 2022 at 11:05):

James Wood said:

This seems to still leave warnings at every Require where these notations were defined (unless I wrap each Require in the same pattern, which I don't really want to do).

if you use Export Set Warnings around the Notation it might work
(it's Require Import causing warnings not just Require right?)

James Wood (Oct 31 2022 at 13:04):

Aha, yes, Export Set seems to do the right thing with respect to warnings. Thanks!

Last updated: Apr 20 2024 at 04:02 UTC