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.53975

Each let binding 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 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.

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

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: Structures