Conflicting use of "~=" in Coq.Program.Equality and Coq.Structures.Equalities
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 3/5
- Tempo stimato
- 1-2 giorni
- Idoneità per principianti
- 35/100
- Tipo di issue
- Bug
- Chiarezza
- Abbastanza chiara
- Stato di attività
- Ferma
- Ambito
- tooling
Direzione di ricerca
Esamina le dichiarazioni di ~= in Coq.Structures.Equalities e Coq.Program.Equality, quindi cerca nella libreria standard gli usi della notazione. Decidi quale dichiarazione o ambito dovrebbe essere modificato affinché l'importazione di entrambe le librerie non produca più un avviso di ridefinizione, quindi verifica le importazioni delle librerie interessate e tutti gli usi individuati.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
Description of the problem
The Coq.Structures.Equalities library file declares the ~= notation (in the empty scope) to mean inequivalence according to some equivalence relation:
Module Type EqNotation (Import E:Eq).
Infix "==" := eq (at level 70, no associativity).
Notation "x ~= y" := (~eq x y) (at level 70, no associativity).
End EqNotation.
The Coq.Program.Equality library file, however, declares it to mean heterogeneous-type equality:
Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
This is not exactly a bug but leads to annoying redefinition warnings when including EqNotation in a module where the Equality library is imported.
Since most projects importing Coq.Program.Equality are probably doing so for access to its tactics, and not making use of the declared ~= notation, it is probably unnecessary to export that notation at all. I cannot find any actual uses of it within the standard library, so simply deleting the notation from Coq.Program.Equality is probably an acceptable solution. If in fact it is being used, another solution would be to declare it in type_scope or program_scope rather than the empty scope. However, it is in any case probably bad practice to use the same notation for equality in one setting and inequality in another, so probably some change should be made to one or the other of these declarations.
Coq Version
The Coq Proof Assistant, version 8.15.2
compiled with OCaml 4.13.1
- Lingua principale
- Rocq Prover
- Stelle
- 45
- Fork
- 39
- Merge medio
- 1g 13h
- PR unite (30g)
- 3
Preparare l'ambiente
- Nessun Dockerfile né file Docker Compose
- Ha un modello di pull request
- Leggi la guida per i contributori
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di rocq-prover/stdlib
-
incl_dec and NoDup_dec should be Defined and not QedForse di nuovo libera Una pull request per questa issue è stata chiusa senza essere unita. Aperta
Difficoltà 1/5 1-3 ore Idoneità per principianti 65/100
rocq-prover/stdlib#25 ·
-
Reals: a constructive pi for the constructive Cauchy reals with a strong irrationality separation theorem (Leibniz series)Forse già presa @hy7pc8gfmf-dotcom l’ha presa 21 giorni fa. Aperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 6/100
rocq-prover/stdlib#315 ·
-
Reals: escape-window separation engine for the constructive Cauchy reals (abstract irrationality criterion)Forse già presa Una pull request collegata a questa issue è aperta o già unita. Aperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100
rocq-prover/stdlib#312 ·
-
Maintaining NaryFunctionsAperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100
rocq-prover/stdlib#293 ·
-
Inconsistent OPAM packaging of rocq-stdlibForse già presa Una pull request collegata a questa issue è aperta o già unita. Aperta
Difficoltà 4/5 3-5 giorni Idoneità per principianti 42/100
rocq-prover/stdlib#256 · 4 commenti · 3 reazioni ·
Tutte le issue di rocq-prover/stdlib
Issue simili
-
Variadic arguments that aren't objects are passed as objects (stringWithFormat_ with %d / %f)Aperta
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
I maintainer di solito rispondono entro 1 giorno
-
bug triage
Difficoltà 2/5 1-3 ore Idoneità per principianti 74/100
I maintainer di solito rispondono entro 1 giorno
-
bug
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
-
bug p2 qa:ui triaged
Difficoltà 2/5 1-3 ore Idoneità per principianti 85/100
saketh-kowtha/lazyhub#464 ·
I maintainer di solito rispondono entro 1 giorno
-
developer-experience documentation good first issue priority: low testing
Difficoltà 2/5 1-3 ore Idoneità per principianti 85/100
Gautam-aman/CODOVYN#22 ·