1.11 Comments and Documentation

Lean files serve two readers at once: the compiler and the human maintainer. Comments and documentation strings give structure to a file without changing the mathematical content. Good comments explain intent, constraints, and design choices. They do not restate every line of code.

Problem

You want to document Lean code so that examples, definitions, and theorems remain understandable after the file grows.

Solution

Use ordinary comments for local notes and documentation comments for public declarations.

-- A single-line comment.

def double (n : Nat) : Nat :=
  n + n

For longer notes, use block comments:

/-
This comment may span several lines.

It is useful for explaining a group of related declarations,
a design choice, or a temporary development note.
-/

For declarations that should appear in generated documentation, use documentation comments:

/-- `double n` returns `n + n`. -/
def double (n : Nat) : Nat :=
  n + n

Single-Line Comments

A single-line comment starts with -- and continues to the end of the line.

def inc (n : Nat) : Nat :=
  n + 1 -- add one to the input

Use these comments for short clarifications. Avoid comments that merely repeat the syntax.

Poor:

-- Define inc.
def inc (n : Nat) : Nat :=
  n + 1

Better:

-- Used in examples where we want computation by `rfl`.
def inc (n : Nat) : Nat :=
  n + 1

The better comment records why the definition has this shape.

Block Comments

A block comment starts with /- and ends with -/.

/-
The next few declarations use `Nat` rather than an arbitrary type
because we want the examples to evaluate with `#eval`.
-/
def square (n : Nat) : Nat :=
  n * n

Block comments are useful near groups of declarations, especially when explaining a section boundary or a temporary simplification.

Documentation Comments

A documentation comment starts with /-- and ends with -/. It attaches to the declaration that follows it.

/-- `square n` is the product of `n` with itself. -/
def square (n : Nat) : Nat :=
  n * n

Use documentation comments for declarations that are part of the public interface of a file or library.

A good documentation comment states the meaning of the declaration, not the proof strategy.

/-- The identity function returns its argument unchanged. -/
def identity {α : Type} (x : α) : α :=
  x

Documenting Theorems

For theorems, document the statement in ordinary mathematical language.

/-- Implication is transitive. -/
theorem imp_trans (P Q R : Prop)
    (hpq : P -> Q) (hqr : Q -> R) : P -> R := by
  intro hp
  exact hqr (hpq hp)

Avoid documentation that depends on the current proof script.

Poor:

/-- Proved by introducing `hp` and applying `hqr`. -/
theorem imp_trans_bad (P Q R : Prop)
    (hpq : P -> Q) (hqr : Q -> R) : P -> R := by
  intro hp
  exact hqr (hpq hp)

The proof may change later. The theorem meaning should remain stable.

Section-Level Notes

Use ordinary comments to mark file regions.

namespace Cookbook

/-
Basic examples used by later recipes.
The declarations are intentionally concrete so that `#eval` works.
-/

def triple (n : Nat) : Nat :=
  n + n + n

theorem triple_zero : triple 0 = 0 := by
  rfl

end Cookbook

This makes the file easier to scan without adding unnecessary namespace layers.

Commenting Proofs

Proof comments should explain the proof move when the tactic script hides an important idea.

theorem and_swap (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  intro h
  constructor
  · exact h.right
  · exact h.left

This proof needs no comments. The tactic script is already readable.

A comment is useful when the proof depends on a non-obvious reduction.

def double (n : Nat) : Nat :=
  n + n

theorem double_zero : double 0 = 0 := by
  -- `double 0` unfolds to `0 + 0`, which reduces definitionally.
  rfl

Use comments to explain hidden computation, library dependencies, or why a lemma is shaped in a particular way.

Stable Documentation Style

Prefer stable descriptions:

/-- Appending the empty list on the right leaves a list unchanged. -/

Avoid unstable descriptions:

/-- This theorem is easy and solved by `simp`. -/

The first remains useful even if the proof changes. The second records an implementation detail.

Literate Examples

Cookbook-style Lean files often mix prose comments and executable code.

/-
This example shows that a theorem can be used as a function.
A proof of `P -> Q` consumes a proof of `P` and returns a proof of `Q`.
-/
theorem use_implication (P Q : Prop) (hp : P) (hpq : P -> Q) : Q :=
  hpq hp

This style is useful for teaching and for regression examples. The code still compiles, so the explanation remains tied to checked artifacts.

Temporary Comments

During development, it is common to leave notes near incomplete work.

-- TODO: generalize this from `Nat` to an arbitrary additive monoid.
def addSelf (n : Nat) : Nat :=
  n + n

Use temporary comments sparingly. They should name a concrete follow-up action.

Common Pitfalls

If a comment explains what every token does, the code probably needs better names.

If a documentation comment describes the proof script, it may become stale after refactoring.

If public declarations lack documentation, later users must infer intent from names alone.

If examples are written only in comments, Lean cannot check them. Prefer executable examples when possible.

Takeaway

Comments should explain intent, constraints, and non-obvious choices. Documentation comments describe the meaning of public declarations. Ordinary comments support local reading and development. The best Lean documentation stays close to checked code while avoiding dependence on fragile proof-script details.