Dep_elim database not used?
I maintainer di solito rispondono entro 2 giorni
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 4/5
- Tempo stimato
- 3-5 giorni
- Idoneità per principianti
- 35/100
- Tipo di issue
- Funzionalità
- Chiarezza
- Abbastanza chiara
- Stato di attività
- Ferma
- Ambito
- tooling
Direzione di ricerca
Inizia da theories/Program/Equality.v alle righe collegate ed esamina simplify_dep_elim, insieme alle tattiche correlate simpl_eqs e simplify_eqs. Determina se il database di unfolding di dep_elim può essere incluso senza costi inaccettabili, quindi verifica che i casi di base che coinvolgono eq_rect_r funzionino senza un passaggio separato di autounfold with dep_elim.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
Was this unfolding database meant to be used in simplify_dep_elim? Because it doesn't seem to be used anywhere in this file, which is a shame. I keep having to call autounfold with dep_elim; simpl_eqs (or simplify_eqs/simplify_dep_elim) in order to get any mileage out of these tactics (eq_rect_r comes up in even the simplest of instances). Would there be a cost to including it in the tactics?
- Lingua principale
- Rocq Prover
- Stelle
- 43
- Fork
- 39
- Merge medio
- 4g 13h
- PR unite (30g)
- 6
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 ·
I maintainer di solito rispondono entro 2 giorni
-
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 16 giorni fa. Aperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 6/100
rocq-prover/stdlib#315 ·
I maintainer di solito rispondono entro 2 giorni
-
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 ·
I maintainer di solito rispondono entro 2 giorni
-
Maintaining NaryFunctionsAperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100
rocq-prover/stdlib#293 ·
I maintainer di solito rispondono entro 2 giorni
-
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 ·
I maintainer di solito rispondono entro 2 giorni
Tutte le issue di rocq-prover/stdlib
Issue simili
-
bug easy good first issue
Difficoltà 2/5 1-3 ore Idoneità per principianti 85/100
lacs-project/sysknife#659 ·
I maintainer di solito rispondono entro 2 giorni
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 85/100
mochan-tk/agentic-dev-kit-for-codex#64 ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 75/100
I maintainer di solito rispondono entro 1 giorno
-
good first issue help wanted
Difficoltà 2/5 1-3 ore Idoneità per principianti 85/100
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
ChromeDevTools/chrome-devtools-mcp#3340 ·
I maintainer di solito rispondono entro 1 giorno