Best Practices

Writing idiomatic Lean 4 code requires more than just knowing syntax. Follow these guidelines to write code that is readable, maintainable, and aligned with the community.

Naming Conventions

Lean follows specific casing rules. Sticking to these makes your code look native.

• CamelCase for types, structures, classes, and modules.
  Example: MyType, List.map, HashMap
• camelCase for functions, definitions, local variables, and theorems.
  Example: myFunction, calculateSum, isPrime
• snake_case is rarely used in core Lean 4, though you might see it in legacy mathlib code.

Explicit vs Implicit Types

Lean's type inference is powerful, but readability is king.

Do Type:

• Top-level function signatures (always!)
• Structure fields
• Ambiguous literals (e.g., (5 : Float))

1-- Good: explicit types for top-level
2def add (x : Nat) (y : Nat) : Nat := x + y
3
4-- Bad: relying on inference for public API
5def add x y := x + y

Don't Type:

• Local variables where type is obvious
• Match arms where patterns imply types

Do Notation Usage

Use do notation for monadic code (IO, Option, etc.). Avoid raw bind (>>=) operators unless the pipeline is very short (1-2 steps).

1-- Good: readable, imperative style
2def safeCompute (x : Nat) : Option Nat := do
3  let y ← safeSubtract x 10
4  let z ← safeDivide y 2
5  return z
6
7-- Avoid: confusing operator chains for complex logic
8def hardToRead (x : Nat) : Option Nat :=
9  safeSubtract x 10 >>= fun y => safeDivide y 2 >>= fun z => pure z

Termination

Avoid partial unless absolutely necessary.partial functions cannot be used in proofs and can hide infinite loops. Try to use structural recursion or termination_by first.

Structure vs Class

Pattern Matching

Prefer the dot syntax match x with or the function match shorthand when possible.

1-- Good: shorthand for simple cases
2def isZero : Nat → Bool
3  | 0 => true
4  | _ => false
5
6-- Good: dot notation for structures
7def getX (p : Point) : Int :=
8  match p with
9  | { x, .. } => x

Use the Standard Library

Before writing a helper function, check List, Array, and String namespaces. Functions like filterMap,find?, any, and all are often built-in.