Declare `Hint Mode` for `Reflexive`, `Symmetric`, `Equivalence`, ...
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 2/5
- Tempo stimato
- 1-3 ore
- Idoneità per principianti
- 38/100
- Tipo di issue
- Bug
- Chiarezza
- Abbastanza chiara
- Stato di attività
- Ferma
- Ambito
- compilers
Direzione di ricerca
Individua le dichiarazioni di Reflexive, Symmetric, Transitive, Equivalence e PreOrder, quindi esamina i relativi suggerimenti per l’inferenza delle typeclass. Verifica come setoid rewrite cerca queste istanze e assicurati che gli Hint Modes richiesti impediscano le ricerche di relazioni non vincolate senza compromettere un’inferenza valida.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
I noticed that as part of the type class inference performed by setoid rewrite, Coq's often performing a wild goose chase on trying to find instances like:
Reflexive A ?R
i.e. Coq is trying to find an arbitrary reflexive relation on a given type.
I think this should be avoided, since:
- It leads to enormous amounts of backtracking, hence poor performance.
- It's possible to get loops by adding instances like
Reflexive A R → Reflexive A (foo R).
The obvious choice to avoid this is to set Hint Modes like:
Hint Mode Symmetric ! ! : typeclass_instances.
Hint Mode Transitive ! ! : typeclass_instances.
Hint Mode Equivalence ! ! : typeclass_instances.
Hint Mode PreOrder ! ! : typeclass_instances.
- Lingua principale
- Rocq Prover
- Stelle
- 42
- Fork
- 40
- Merge medio
- 20h 23m
- PR unite (30g)
- 2
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: 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 ·
-
`QArith`: Add more rounding modes to complement `Qfloor` and `Qceiling`Forse già presa @RyanGlScott l’ha presa 87 giorni fa. Aperta
Difficoltà 3/5 1-2 giorni Idoneità per principianti 52/100
rocq-prover/stdlib#283 · 2 commenti ·
-
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
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
I maintainer di solito rispondono entro 1 giorno
-
Default-import note suggests `import * as process` for velt:process, which does not name the builtinAperta
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
I maintainer di solito rispondono entro 1 giorno
-
diagnostics good first issue
Difficoltà 2/5 1-3 ore Idoneità per principianti 82/100
I maintainer di solito rispondono entro 1 giorno
-
category:runtime
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
I maintainer di solito rispondono entro 1 giorno
-
Re-enable -fno-lto testApertatests
Difficoltà 2/5 1-3 ore Idoneità per principianti 62/100
rust-lang/rustc_codegen_gcc#993 ·
I maintainer di solito rispondono entro 1 giorno