Module 1 · Lesson 4

Local Scope

Use let bindings to create intermediate values and structure your computations clearly.

Let Bindings

The let keyword introduces local variables. These are scoped to the expression that follows:

lean

1def circleArea (radius : Float) : Float :=
2  let pi := 3.14159
3  let radiusSquared := radius * radius
4  pi * radiusSquared
5
6#eval circleArea 5.0  -- 78.539750

Each letbinding creates a name that's available in all subsequent code within the same scope.

Let with Type Annotations

You can add type annotations to let bindings for clarity:

lean

1def example1 : Nat :=
2  let x : Nat := 10
3  let y : Nat := 20
4  x + y
5
6-- Type annotations are optional when inferable
7def example2 : Nat :=
8  let x := 10  -- Inferred as Nat
9  x * 2

Nested Let Bindings

Let bindings can be nested, and each inner binding can use outer ones:

lean

1def compute : Nat :=
2  let a := 5
3  let b := a * 2      -- Uses 'a'
4  let c := a + b      -- Uses both 'a' and 'b'
5  c * 2               -- Result: 30
6
7#eval compute  -- 30

Variable Shadowing

You can reuse names in inner scopes. The inner definition "shadows" the outer one:

lean

1def shadowExample : Nat :=
2  let x := 10
3  let x := x + 5   -- This 'x' shadows the previous one
4  let x := x * 2   -- And this shadows again
5  x                -- Final value: 30
6
7#eval shadowExample  -- 30

ℹ

Shadowing is useful for transforming values step-by-step while keeping names meaningful. The original value is not modified—a new binding is created.

Let in Expressions

let can be used inline within expressions:

lean

1-- Inline let
2#eval let x := 5; x * x  -- 25
3
4-- Multiple inline lets
5#eval let a := 2; let b := 3; a + b  -- 5
6
7-- Let in function arguments
8#eval List.map (fun n => let doubled := n * 2; doubled + 1) [1, 2, 3]
9-- [3, 5, 7]

Let with Pattern Matching

You can destructure values directly in a let binding.

lean

1def swap (p : Nat × Nat) : Nat × Nat :=
2  let (a, b) := p
3  (b, a)
4
5#eval swap (3, 7)  -- (7, 3)
6
7-- Nested patterns work too
8def sum3 (p : Nat × Nat × Nat) : Nat :=
9  let (a, b, c) := p
10  a + b + c
11
12#eval sum3 (1, 2, 3)  -- 6

⚠

Pattern-matching let only accepts patterns that cannot fail — a single constructor, like a pair or a one-constructor structure. Writing let some x := o for an Option makes Lean ask what should happen in the none case. Use if let or match for those.

if let

if letcombines a pattern match with a fallback in one line. It is the idiomatic way to handle "try this pattern, otherwise do something else".

lean

1def firstEven (xs : List Nat) : String :=
2  if let some x := xs.find? (· % 2 == 0) then
3    s!"found {x}"
4  else
5    "none"
6
7#eval firstEven [1, 3, 4]  -- "found 4"
8#eval firstEven [1, 3, 5]  -- "none"

let rec: Recursive Local Definitions

A plain let cannot refer to itself. Add rec when you need a local loop and do not want to expose a top-level helper.

lean

1def sumTo (n : Nat) : Nat :=
2  let rec go : Nat → Nat
3    | 0     => 0
4    | k + 1 => (k + 1) + go k
5  go n
6
7#eval sumTo 4  -- 10

ℹ

let rec and where both give you a recursive local helper. where is usually preferred: it keeps the main expression at the top, and it produces a named auxiliary declaration (sumTo.go) that you can refer to in proofs.

Let vs Where

Both let and where create local bindings, but they have different use cases:

lean

1-- 'let' bindings come BEFORE the main expression
2def withLet (x : Nat) : Nat :=
3  let doubled := x * 2
4  let tripled := x * 3
5  doubled + tripled
6
7-- 'where' bindings come AFTER the main expression
8def withWhere (x : Nat) : Nat :=
9  doubled + tripled
10where
11  doubled := x * 2
12  tripled := x * 3
13
14-- Both produce the same result
15#eval withLet 5    -- 25
16#eval withWhere 5  -- 25

Key Takeaway

Use let for step-by-step computation (top to bottom). Use where when you want the main logic first with supporting definitions below.

Exercise: Refactor with let

Rewrite the following function to use let bindings for clarity.

lean

1def bmi (weightKg heightM : Float) : Float :=
2  weightKg / (heightM * heightM)
3
4-- Refactor into named steps
5def bmi' (weightKg heightM : Float) : Float :=
6  let heightSq := heightM * heightM
7  let ratio := weightKg / heightSq
8  ratio

Scope Isolation

Variables defined in one scope don't leak into others:

lean

1def outer : Nat :=
2  let x := 10
3  let inner := 
4    let y := 20  -- 'y' is only visible here
5    x + y        -- Can access 'x' from outer scope
6  -- 'y' is not accessible here
7  inner + x      -- Can use 'inner' and 'x'
8
9#eval outer  -- 40

Deep Dive: Let is Not Mutation

Coming from imperative languages, let might look like variable assignment. But Lean is purely functional—there is no mutation.

Each let creates a new, immutable binding. Shadowing creates a new binding with the same name, not a modification of the original.

lean

1-- This is NOT mutation:
2def notMutation : Nat :=
3  let x := 5
4  let x := 10  -- New binding, old 'x' is gone
5  x            -- 10

let vs have

Lean has a second local-binding keyword, have. It looks interchangeable with let, and for values it very nearly is — but the difference matters as soon as you start proving things.

lean

1-- let REMEMBERS the definition: later code can see that x is literally 5
2example : True :=
3  let x := 5
4  -- here Lean knows x = 5 by definition, so this typechecks:
5  have : x = 5 := rfl
6  trivial
7
8-- have FORGETS the definition: it keeps only the type
9example : True :=
10  have y := 5
11  -- have : y = 5 := rfl   -- fails! Lean only knows y : Nat, not y = 5
12  trivial

💡

The rule: use let for data you will compute with, and have for proofs, where the statement is all that matters and the proof term is irrelevant. Using have for proofs also keeps goal displays readable — the proof term never gets inlined into your goal.

Practical Example

Here's a more realistic example showing local scope in action:

lean

1def formatPrice (cents : Nat) : String :=
2  let dollars := cents / 100
3  let remaining := cents % 100
4  let dollarStr := toString dollars
5  let centStr := if remaining < 10 
6                 then "0" ++ toString remaining 
7                 else toString remaining
8  "$" ++ dollarStr ++ "." ++ centStr
9
10#eval formatPrice 1234   -- "$12.34"
11#eval formatPrice 50     -- "$0.50"
12#eval formatPrice 1005   -- "$10.05"

Functions & Definitions Next: Syntax & Notation