leanprover-community/physlib

Remove `erw`s

Aperta

#385 aperta il 10 mar 2025

Vedi su GitHubGuida contributor
 (1 commento) (0 reazioni) (0 assegnatari)Lean (139 fork)auto 404
good first issuehelp-wanted

Metriche repository

Star
 (642 stelle)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

There are lots of erw [...] in PhysLean. These are slow, and thus it is beneficial for them to be removed.

To remove an erw [...] usually means changing the corresponding lemma to simp-normal form.

Guida contributor

Direzione di ricerca
Cerca nel codice i pattern `erw`. Per ognuno, identifica il lemma utilizzato e considera se può essere reso `simp` normale. Quindi sostituisci `erw` con `simp` o `rw` a seconda dei casi. Assicurati che le modifiche passino la suite di test.
Tech stack
Nessuno
Dominio
performance
Tipo issue
Refactoring
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
2
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
Mezza giornata
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
Lean
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
70