leanprover-community/physlib

Remove `erw`s

Ouverte

#385 ouverte le 10 mars 2025

Voir sur GitHubGuide contributeur
 (1 commentaire) (0 réaction) (0 personne assignée)Lean (139 forks)auto 404
good first issuehelp-wanted

Métriques du dépôt

Stars
 (642 étoiles)
Métriques de merge PR
 (Métriques PR en attente)

Description

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.

Guide contributeur

Direction de recherche
Recherchez dans la base de code les motifs `erw`. Pour chacun, identifiez le lemme utilisé et considérez s'il peut être rendu `simp` normal. Remplacez ensuite `erw` par `simp` ou `rw` selon le cas. Assurez vous que les modifications passent la suite de tests.
Stack technique
Aucun
Domaine
performance
Type d'issue
Refactorisation
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
2
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
Une demi journée
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Active
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Claire
Prérequis
Lean
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
70