Mathlib Review
Review guidelines for Mathlib PRs. Use when reviewing pull requests, checking code quality, or assessing whether a PR is ready to merge.
MCP get_skill({ skillId: "mathlib-review-a8b0e8cf" })Use this skill with your agent
Create a free account and connect via MCP
# 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
Related Skills
More skills in Software Engineering
Accessibility Standards
Comprehensive web accessibility standards based on WCAG 2.2 AA, with 38+ anti-patterns, legal enforcement context (EAA, ADA Title II), WAI-ARIA patterns, and framework-specific fixes for modern web frameworks and libraries.
Accord
Authoring unified specification packages across Business/Development/Design teams via staged elaboration (L0 Vision → L1 Requirements → L2 Team Detail → L3 Acceptance Criteria). No code. Use when authoring cross-team specs, building L0-L3 packages, or aligning Biz/Dev/Design on a single source of truth.
Acquire Codebase Knowledge
Use this skill when the user explicitly asks to map, document, or onboard into an existing codebase. Trigger for prompts like "map this codebase", "document this architecture", "onboard me to this repo", or "create codebase docs". Do not trigger for routine feature implementation, bug fixes, or narrow code edits unless the user asks for repository-level discovery.
Acreadiness Assess
Run the AgentRC readiness assessment on the current repository and produce a static HTML dashboard at reports/index.html. Wraps `npx github:microsoft/agentrc readiness` and hands off rendering to the @ai-readiness-reporter custom agent. Supports policies (--policy) for org-specific scoring. Use when asked to assess, audit, or score the AI readiness of a repo.
Acreadiness Generate Instructions
Generate tailored AI agent instruction files via AgentRC instructions command. Produces .github/copilot-instructions.md (default, recommended for Copilot in VS Code) plus optional per-area .instructions.md files with applyTo globs for monorepos. Use after running /acreadiness-assess to close gaps in the AI Tooling pillar.
Acreadiness Policy
Help the user pick, write, or apply an AgentRC policy. Policies customise readiness scoring by disabling irrelevant checks, overriding impact/level, setting pass-rate thresholds, or chaining org baselines with team overrides. Use when the user asks about strict mode, AI-only scoring, custom weights, CI gating, or wants org-wide standardisation.
Explore Other Categories
Skills from other categories with shared topics
Lean PR
PR conventions for the leanprover/lean4 repository. Use when creating pull requests, writing commit messages, or following project conventions for Lean contributions.
Lean Proof
Use when asked to prove something in Lean. Covers one-step-at-a-time proving, error priority, working on the hardest case first, proof cleanup, and handling dependent type rewriting issues.
Lean4 Setup
Set up a lean4 repository clone with proper elan toolchains.