scottnarmstrong/leanautoformalizationskills/lean-naming-style

Lean Naming Style

Use this skill when creating or renaming declarations, organizing modules, or cleaning Lean code for review. The goal is not just “pretty code”; it is a library-shaped API that feels native to Mathlib.

Naming Rules

• Use snake_case for theorem names and terms of type Prop.
• Use UpperCamelCase for structures, classes, inductive types, and other declarations returning Type or Sort.
• Use lowerCamelCase for ordinary terms returning data.
• Prefer descriptive theorem names whose conclusion drives the name.
• add hypotheses with _of_...
• use systematic fragments like nonneg, inj, ext, iff
• Put the declaration in the most specific namespace that supports natural dot notation.

File and API Rules

• Use UpperCamelCase.lean file names.
• In projects using the module system, follow this header order:
• copyright comment;
• module;
• imports: public import only for what statements need, plain import

otherwise;

• /-! module docstring -/;
• public section.

See the lean-project-architecture skill's references/module-system.md.

• Keep one focused topic per file and follow the repository's file-size limit.
• Import as little as possible.
• After adding a public definition, add the obvious API immediately.
• constructor or evaluation lemmas
• @[simp] lemmas only when they genuinely improve simplification
• extensionality lemmas where equality is structural
• Add module docstrings and public-definition docstrings where they help later readers.

Style Rules

• Prefer readable proofs over clever ones.
• Keep checked-in proofs explicit and lint-clean.
• Do not commit unmanifested sorry, exact?, apply?, or exploratory

simp. The sole sorry exception is the exact by sorry body of an author-approved, manifest-bound frozen keystone theorem in state DRAFT_SORRY; it is statement ABI, not finished code.

• In projects with a zero-warning policy, do not commit while linter warnings remain.

Review Checklist

• Does the name match Mathlib conventions?
• Is the namespace the right one?
• Is the file the canonical home?
• Are imports minimal?
• Are there missing simp, ext, or accessor lemmas?
• Is the code docstring- and linter-clean?

References

• Read references/naming-and-style.md for naming patterns, symbol-to-name translations, structural lemma conventions, file organization, and lint/style expectations.