leanprover-community/physlib

Remove `erw`s

Offen

#385 geöffnet am 10.03.2025

Auf GitHub ansehenContributor Guide
 (1 Kommentar) (0 Reaktionen) (0 zugewiesene Personen)Lean (139 Forks)auto 404
good first issuehelp-wanted

Repository-Metriken

Stars
 (642 Sterne)
PR-Merge-Metriken
 (PR-Metriken ausstehend)

Beschreibung

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.

Contributor Guide

Research-Richtung
Durchsuchen Sie die Codebasis nach `erw` Mustern. Identifizieren Sie für jedes Muster das verwendete Lemma und überlegen Sie, ob es in die `simp` Normalform gebracht werden kann. Ersetzen Sie dann `erw` durch `simp` oder `rw` je nach Bedarf. Stellen Sie sicher, dass die Änderungen die Testsuite bestehen.
Tech Stack
Keine
Domain
performance
Issue Type
Refactoring
SchwierigkeitGeschätzte Implementierungsschwierigkeit für neue Contributors, von 1 für sehr kleine Änderungen bis 5 für Expertenarbeit.
2
Geschätzte ZeitEin grober Zeitrahmen, um zu recherchieren, zu implementieren, zu testen und einen Pull Request vorzubereiten.
Halber Tag
AktivitätsstatusWie verfügbar das Issue gerade wirkt: frisch, aktiv, stale, blockiert oder wartet auf Maintainer-Input.
Aktiv
KlarheitWie klar das Issue die erwartete Änderung, Akzeptanzkriterien und den nächsten Schritt erklärt.
Klar
Voraussetzungen
Lean
EinsteigerfreundlichkeitEin Score von 1 bis 100, der schätzt, wie zugänglich dieses Issue für First-Time Contributors ist.
70