mathlib-review
Review guidelines for Mathlib PRs. Use when reviewing pull requests, checking code quality, or assessing whether a PR is ready to merge.
소스 정보
- 저장소
- leanprover/skills
- 최근 소스 활동
- 2026년 2월 20일 12:34
- 감지된 SKILL.md 언어
- 영어
- 스타
- 74
- 포크
- 2
설치 방법
기본적으로 소스를 먼저 확인하는 Prompt가 선택됩니다. 직접 명령으로 전환하거나 로컬 사본을 다운로드할 수도 있습니다.
소스 파일 검토
설치 여부를 결정하기 전에 SKILL.md와 SkillsMP에 표시된 보조 파일을 읽어 보세요.
SKILL.md 표시 중
SKILL.md
소스 지침 · 읽기 전용 미리보기- name
- mathlib-review
- description
- Review guidelines for Mathlib PRs. Use when reviewing pull requests, checking code quality, or assessing whether a PR is ready to merge.
# Mathlib PR Review
## Attributes and API
- New definitions should come with associated lemmas and appropriate attributes (`@[simp]`, `@[ext]`, etc.).
- Watch for instance diamonds.
- Prefer bundled morphisms, `FunLike` API for morphism classes, `SetLike` API for subobject classes.
## Style Points Specific to Mathlib
- **Simp squeezing:** Terminal `simp` calls should NOT be squeezed (replaced with `simp only [...]`) unless there's a measured performance problem. Unsqueezed `simp` is more maintainable and doesn't break when lemmas are renamed.
- **Normal forms:** Prefer `s.Nonempty` over alternatives. Use `hne : x ≠ ⊥` in hypotheses (easier to check), `hlt : ⊥ < x` in conclusions (more powerful).
- **Transparency:** Needing `erw`, or `rfl` after `simp`/`rw` usually means the API is missing lemmas.
- **File size:** Consider splitting files that exceed ~1000 lines or cover multiple topics.
## Reference Guides
The full review guide and style references:
- **Review guide:** https://leanprover-community.github.io/contribute/pr-review.html
- **Naming conventions:** https://leanprover-community.github.io/contribute/naming.html
- **Code style:** https://leanprover-community.github.io/contribute/style.html
- **Documentation style:** https://leanprover-community.github.io/contribute/doc.html
GitHub에서 보기