agentsclimarketplace
Sign in

Mathlib review

Skill leanprover/skills/skills/mathlib-review

Review guidelines for Mathlib PRs. Use when reviewing pull requests, checking code quality, or assessing whether a PR is ready to merge.From its SKILL.md

Install
npx -y skills add leanprover/skills --skill mathlib-review

Assembled from the repository path, not quoted from the project. Check it against their README if it does not work.

SKILL.md

1.5 KB, as published. Nobody here has run it

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:

Keep looking

Skills are one crate of 617,483. Ordering is by how many stacks a row turns up in, so the top of any crate is what has actually been picked rather than what has the most stars.