[[Style is consistent constraint]]. Having a consistent style collapses hundreds of future decisions into one, and gives me focus. - Steph Ango - CEO of Obsidian # Lean Notes style emphasizes terse but effective comments sand labeling guidelines, ...and more The Lean Notes code guidelines is intended to help beginners as they learn Lean. It is also helpful for others who tend to error on the side of emphasizing exposition over terseness and who appreciate consistent naming protocols. Interestingly, the Lean Notes code guidelines are inspired by the coding explanations generated by Gemini. Here are the general principles that define the Lean Notes code guidelines: - The coding style emphasizes explanations over terseness... in moderation. - Comments are mandated when the Lean syntax is opaque in its meaning. - Coding phrases that are self-explanatory are mandated, such as using: - exact show *Goal* from *Hypothesis* instead of - exact *Hypotheses*. - Comments are intended to minimize the need to refer back to other parts of the code. The idea here is that reading the code should have a forward direction, minimal back and forth pivoting, thereby reducing "reading friction". Please help us refine and improve the Lean Notes code guidelines Your suggestions and observations will be considered carefully if you provide comments by way of the LeanNotes GitHub repository. --- The remaining sections in this article offer specific recommendations for comment and identifier naming conventions. # Hypotheses Names **Guidelines** - Hypothesis have an h prefix followed by the simplest abbreviations possible. - Implication is mapped to adjacency: P → Q maps to **hPQ** - Simple boolean hypothesis map symbols to their word counterparts: P ∧ Q maps to **hPandQ** - Parentheses are mapped to pairs of underbars: (P → Q) → R maps to **\_PQ_R** - A single complex hypothesis is named h, or h{description suffix} - A series of complex hypotheses is enumerated with a numbering suffix: *h1, h2, ... hn* **Examples** | term | maps to | hypothesis | Comment | | -------------------------- | ------- | --------------- | ---------------------------------------------------------------------- | | P | | hP | Try to use P, Q, R, S, T as Prop constant terms | | ¬P | | hnotP | Negation is mapped to a not prefix. | | P ∧ Q | | hPandQ | | | P ∨ Q | | hPorQ | | | P → Q | | hPQ | The implication arrow maps to juxtaposition. | | P → Q → R | | hPQR | The implication arrow maps to juxtaposition. | | P ↔ Q | | hPiffQ | | | P ↔ Q ↔ R | | hPiffQiffR | | | | | | | | P ∨ (Q ∧ R) | | hPor\_QandR\_ | Parentheses are mapped to underbars. | | (P ∨ Q) ∧ R | | h_PorQ_andR | Parentheses are mapped to underbars. | | | | | | | lengthly premise | | h, hFcontinuous | A complex hypothesis maps to h or to h and a terse descriptive suffix. | | multiple lengthly premises | | h1, h2, ... hn | Multiple complex terms are numbered. | **Rationale**: We want to encode as much information as possible in the names of hypothesis in as few letters as possible. # Shadowed identifiers have single quote suffixes **Definition and examples**: When an identifier is shadowed, use one or more single quotes, ', to designate the shadow identifiers These shadow identifiers are not used in subsequent portions within the current context; only the first (non-shadow) identifier is used. **Examples**: - if the term *hP* has one shadow, then the shadow is named *\_hp* - If the term hP has more than one shadow, then the shadows are enumerated by quote suffixes as in: *\_hp', \_hp'', \_hp'''*. - The shadowed versions of the original constant, \_hp', and \_hp'' , are not used in subsequent portions within the current scope. That is, the original identifier, hP, is the only one used in subsequent occurrences within the current scope. **Rationale**: The Lean syntax allows shadowed constants to be referred to implicitly with no name in the code and only as a reference in the infoview. An underbar placeholder and also be used for shadowed constants. Both of these syntax conventions can require backwards code scanning to remember which variable is being shadowed. This backward scanning can be avoided by using this style guideline. Example: ```lean theorem pPPPP : P → P → P → P := by intros hP hP' hP'' -- ⊢ P sorry ``` ![[Shadowed term example.png]] # Unused constants have an underbar prefix **Definition**: Use an underbar prefix followed by an identifier to designate an unused identifier. **Rationale**: This guideline explicitly exposes which identifiers are actually unused, serving as a reminder that the proof may need editing to remove superfluous assertions. Using an underbar alone to denote an unused identifier often requires that the reader scan the code backwards to remember which identifier is unused. This backwards scanning can be eliminated by denoting unused identifiers with an underbar prefix to the identifier. **Notes**: - The Lean parser recognizes both _ and \_{identifier} as an unused identifier. - The `set_option linter.unusedVariables false` directive can be used to turn off linter warnings of unused identifiers. --- **Author**: [[dducoff]] **Creation Date:** 2026-01-19