leanprover-community/physlib

Remove `erw`s

开放

#385 创建于 2025年3月10日

在 GitHub 查看贡献者指南
 (1 条评论) (0 个反应) (0 位负责人)Lean (139 个派生)auto 404
good first issuehelp-wanted

仓库指标

星标
 (642 个星标)
PR 合并指标
 (PR 指标待抓取)

描述

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
议题类型
重构
难度面向新贡献者的预计实现难度，1 表示很小改动，5 表示专家级工作。
2
预计时间有经验贡献者完成调查、实现、测试并准备 pull request 的粗略时间范围。
半天
活动状态议题当前的可参与程度：新鲜、活跃、陈旧、阻塞或等待维护者输入。
活跃
清晰度议题是否清楚说明期望改动、验收标准和下一步。
清晰
前置要求
Lean
新手友好度1-100 的估计分数，表示该议题对首次贡献者的友好程度。
70