leanprover-community/physlib

Remove `erw`s

オープン

#385 opened on 2025/03/10

GitHub で見るコントリビューターガイド
 (1 件のコメント) (0 件のリアクション) (0 人の担当者)Lean (139 件のフォーク)auto 404
good first issuehelp-wanted

Repository metrics

Stars
 (642 個のスター)
PR merge metrics
 (PR metrics pending)

説明

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.

コントリビューターガイド

調査方針
コードベースで`erw`パターンを検索します。それぞれについて、使用されている補題を特定し、それを`simp`ノーマル形式にできるか検討します。その後、`erw`を`simp`または`rw`に置き換えます。変更がテストスイートを通過することを確認してください。
技術スタック
なし
領域
performance
Issue 種別
リファクタリング
難度新しい貢献者にとっての実装難度です。1 は非常に小さな変更、5 は専門的な作業です。
2
推定時間経験ある貢献者が調査、実装、テスト、pull request 準備にかけるおおよその時間範囲です。
半日
活動状況Issue が今どれだけ取り組みやすいかを示します。新しい、活発、古い、ブロック中、またはメンテナー入力待ちなどです。
アクティブ
明確さ期待される変更、受け入れ条件、次の手順がどれだけ明確かを示します。
明確
前提条件
Lean
初心者向け度初回貢献者にどれだけ取り組みやすいかを 1-100 で推定したスコアです。
70