▶ Open this chapter in JupyterLite

Chapter 4 — Lists

List is Lean's bread-and-butter linked-list type. It's the default sequential collection — pattern-match-friendly, recursion-friendly, and how most standard-library APIs return multi-valued results.

(For random-access workloads, jump ahead to Chapter 5 (`Array`). For frequent contains-tests, Chapter 7 (`HashMap` / `HashSet`).)

4.1 Literals and basic construction

#eval [1, 2, 3]

[1, 2, 3]

#check ([1, 2, 3] : List Nat)

[1, 2, 3] : List Nat

The empty list is []. It's polymorphic, so the type usually comes from context:

#check ([] : List Nat)

[] : List Nat

The cons operator is :::

#eval 0 :: [1, 2, 3]

[0, 1, 2, 3]

:: is right-associative, so 1 :: 2 :: 3 :: [] is the same as 1 :: (2 :: (3 :: [])), which is the same as [1, 2, 3].

4.2 Concatenation, length, reverse

#eval [1, 2] ++ [3, 4]
#eval [1, 2, 3, 4].length
#eval [1, 2, 3, 4].reverse

[1, 2, 3, 4]
4
[4, 3, 2, 1]

++ is O(n) on the left operand (just like Haskell's ++): walks the left list, then re-uses the right one. For repeated appends, build the list in reverse and reverse once at the end.

4.3 The functor/foldable toolbox

#eval [1, 2, 3, 4].map (· * 10)
#eval [1, 2, 3, 4].filter (· > 2)
#eval [1, 2, 3, 4].foldl (· + ·) 0
#eval [1, 2, 3, 4].sum
#eval [1, 2, 3, 4].any (· > 3)
#eval [1, 2, 3, 4].all (· > 0)

[10, 20, 30, 40]
[3, 4]
10
10
true
true

The (· ▢ ·) syntax (two anonymous-argument placeholders) is a shorthand for fun a b => a ▢ b.

foldl is left-fold; foldr exists too but be aware it forces the entire list:

-- right-fold flips the arrow:
#eval [1, 2, 3, 4].foldr (· :: ·) ([] : List Nat)

[1, 2, 3, 4]

4.4 Zipping and unzipping

#eval List.zip [1, 2, 3] ["a", "b", "c"]

[(1, "a"), (2, "b"), (3, "c")]

zip stops at the shorter list. zipWith zips with a function:

#eval List.zipWith (· + ·) [1, 2, 3] [10, 20, 30]

[11, 22, 33]

4.5 Range and friends

List.range n produces [0, 1, …, n-1]. There's no range a b / range a b step in core, but the building blocks are easy to combine:

#eval List.range 5
#eval (List.range 6).map (· + 1)
#eval (List.range 10).filter (· % 2 == 0)

[0, 1, 2, 3, 4]
[1, 2, 3, 4, 5, 6]
[0, 2, 4, 6, 8]

4.6 for ... in ... do over lists

In do notation, for x in xs do ... iterates monadically. This is the easiest way to combine an IO action with a list:

#eval show IO Unit from do
  for i in [1, 2, 3] do
    IO.println s!"item {i}"

item 1
item 2
item 3

show IO Unit from do ... is an ascription that tells the elaborator which monad the do runs in — needed because in a bare #eval do ... the elaborator can't infer the monad from just for ... do IO.println alone. With IO.println involved, IO is the natural pick.

4.7 Pattern-matching on lists

def headOrZero : List Nat → Nat
  | []     => 0
  | x :: _ => x

#eval headOrZero []
#eval headOrZero [42, 7, 13]

0
42

Multiple cells of pattern-matching at once:

def takePairs : List α → List (α × α)
  | a :: b :: rest => (a, b) :: takePairs rest
  | _              => []

#eval takePairs [1, 2, 3, 4, 5, 6]
#eval takePairs [1, 2, 3]

[(1, 2), (3, 4), (5, 6)]
[(1, 2)]

4.8 List.foldl vs explicit recursion

For most things, the prelude already has what you want. Need a sum / product / max / min / count? Reach for the combinator first:

#eval [3, 1, 4, 1, 5, 9, 2, 6].foldl Nat.max 0
#eval [3, 1, 4, 1, 5, 9, 2, 6].length

9
8

Explicit recursion is good for new shapes that don't fit a standard fold. Lean's compiler still unrolls them efficiently when the recursion is structural.

4.9 List.toArray when you outgrow lists

Lists are great for sequential / pattern-matching workloads but indexing xs[100] is O(100). When you need random access, ship the list to an Array:

#eval [10, 20, 30].toArray
#eval [10, 20, 30].toArray[1]!

#[10, 20, 30]
20

[i]! is the panicking-on-OOB indexing operator; safer alternatives are xs[i]? (returns Option) and xs[i] plus a proof of i < xs.size (chapter 5 covers this).

4.10 Recap

You can now:

zipWith, range

Next: Chapter 5 (`Array`), Lean's primary random-access container.