Functions

Functions are the heart of Lean. This level takes you from a one-line def to the pipeline style used throughout real Lean codebases.

Learning Goals

• Define functions with def, with and without explicit types.
• Write anonymous functions three different ways and know when each reads best.
• Explain what Nat → Nat → Nat really means (it is not what most people assume).
• Use map, filter, and foldl instead of writing loops.
• Structure larger definitions with let and where.

Definitions with def

The full form names each argument with its type, then the return type, then the body. When several arguments share a type you can group them.

1def add (x : Nat) (y : Nat) : Nat := x + y
2#eval add 3 5          -- 8
3
4-- Same thing, grouped arguments
5def add' (x y : Nat) : Nat := x + y
6#eval add' 3 5         -- 8
7
8def greet (name : String) : String := "Hello, " ++ name
9#eval greet "Lean"     -- "Hello, Lean"

Letting Lean infer the types

Lean can often work out the types itself. This is convenient for scratch work, but in code you intend to keep, writing the type is worth it: it documents your intent and it makes error messages point at the real mistake instead of somewhere three functions downstream.

1def double x := x * 2
2
3#check double          -- double (x : Nat) : Nat
4#eval double 21        -- 42

Anonymous Functions

Not every function deserves a name. Lean gives you three ways to write one inline, in decreasing order of verbosity.

1-- 1. Full lambda syntax
2#eval (fun x => x * 2) 21           -- 42
3#eval (fun x y => x + y) 3 4        -- 7
4
5-- 2. With an explicit type when Lean needs help
6#check fun (x : Nat) => x * 2       -- fun x => x * 2 : Nat → Nat
7
8-- 3. Centred-dot shorthand: · becomes the argument
9#eval (· * 2) 21                    -- 42
10#eval [1, 2, 3].map (· * 2)         -- [2, 4, 6]

Currying: Every Function Takes One Argument

This is the idea that unlocks a lot of Lean code. When you write add (x y : Nat) : Nat, you have not defined a function of two arguments. You have defined a function of one argument that returns another function. Ask Lean and it will tell you so.

1def addC (x : Nat) (y : Nat) : Nat := x + y
2
3#check addC      -- addC (x y : Nat) : Nat
4#check addC 3    -- addC 3 : Nat → Nat     ← still a function!
5
6-- So you can supply arguments one at a time
7def addFive : Nat → Nat := addC 5
8#eval addFive 10   -- 15

Supplying fewer arguments than the full count is called partial application, and it is how you build small specialised functions out of general ones without writing a lambda.

Pattern Matching in Definitions

Instead of a single body, a function can branch on the shape of its input. Both forms below define the same function; the second drops the match boilerplate by listing the cases directly after the type.

1def isZero (n : Nat) : Bool :=
2  match n with
3  | 0 => true
4  | _ => false
5
6-- Equation style: same function, less ceremony
7def isZero' : Nat → Bool
8  | 0 => true
9  | _ => false
10
11#eval isZero 0    -- true
12#eval isZero 4    -- false

Level 6 covers pattern matching properly. For now just note that the equation style is extremely common in Lean source, so it is worth recognising.

Structuring Bigger Definitions

Use let to name an intermediate value inside a body, and where to attach helper definitions after it. where reads well when the helper is a detail you want out of the way of the main idea.

1def sumOfSquares (a b : Nat) : Nat :=
2  let sq := a * a + b * b
3  sq + 1
4
5#eval sumOfSquares 3 4    -- 26
6
7def area (w h : Nat) : String :=
8  s!"area is {a}"
9where
10  a : Nat := w * h
11
12#eval area 3 4            -- "area is 12"

Higher-Order Functions

A function that takes another function as an argument is called higher-order. Lean has no forloop in the imperative sense — the three functions below do most of the work loops do in other languages.

1def applyTwice (f : Nat → Nat) (x : Nat) : Nat := f (f x)
2#eval applyTwice (· + 3) 10         -- 16
3
4-- map: transform every element
5#eval [1, 2, 3].map (· * 2)         -- [2, 4, 6]
6
7-- filter: keep the elements that pass a test
8#eval [1, 2, 3, 4, 5].filter (· % 2 == 0)   -- [2, 4]
9
10-- foldl: collapse a list to a single value
11#eval [1, 2, 3, 4, 5].foldl (· + ·) 0       -- 15

Reading foldl

foldl f init xs starts with init and folds each element in, left to right. With (· + ·) and 0 it computes ((((0+1)+2)+3)+4)+5. Swap in (· * ·) and 1and you have a product instead. Most “loop over a list and accumulate” tasks are a fold in disguise.

Pipelines

Chaining operations with nested parentheses gets unreadable fast. The |> operator feeds the value on the left into the call on the right, letting you read a transformation in the order it happens.

1-- Nested: read inside-out
2#eval ([1, 2, 3, 4, 5].filter (· % 2 == 0)).map (· * 10)
3
4-- Pipeline: read left-to-right
5#eval [1, 2, 3, 4, 5] |>.filter (· % 2 == 0) |>.map (· * 10)
6
7-- Both print [20, 40]

There is also function composition with ∘, which builds a new function rather than immediately applying one. Order matters: the right-hand function runs first.

1def inc (n : Nat) : Nat := n + 1
2def dbl (n : Nat) : Nat := n * 2
3
4#eval (inc ∘ dbl) 5    -- 11   doubles first, then increments
5#eval (dbl ∘ inc) 5    -- 12   increments first, then doubles

Implicit Arguments

Braces instead of parentheses mark an argument Lean should figure out on its own. The identity function works at any type, but you never have to say which type you are using — Lean reads it off the value you pass.

1def myId {α : Type} (x : α) : α := x
2
3#eval myId 5       -- 5      α inferred as Nat
4#eval myId "hi"    -- "hi"   α inferred as String
5
6-- The @ prefix shows the function with implicits made visible
7#check @myId       -- @myId : {α : Type} → α → α

Practice

1def getOrZero (value : Option Nat) : Nat :=
2  match value with
3  | some n => n
4  | none => 0
5
6#eval getOrZero (some 7)   -- 7
7#eval getOrZero none       -- 0

1def applyN (f : Nat → Nat) : Nat → Nat → Nat
2  | 0, x => x
3  | n + 1, x => applyN f n (f x)
4
5#eval applyN (· + 3) 4 0    -- 12

1def sumEvens (xs : List Nat) : Nat :=
2  xs.filter (· % 2 == 0) |>.foldl (· + ·) 0
3
4#eval sumEvens [1, 2, 3, 4, 5, 6]   -- 12

Common Mistakes

• Using a period instead of the centred dot. (. * 2) is not (· * 2).
• Expecting an arity error from partial application.Passing too few arguments is legal and gives you a function back — the error usually surfaces later, somewhere confusing.
• Reaching for a loop. If you catch yourself wanting for, the answer is almost always map, filter, foldl, or recursion.
• Getting composition backwards. f ∘ g runs g first.

Check Yourself

• What is the type of add 3 if add : Nat → Nat → Nat?
• Rewrite fun x => x + 1 using the dot shorthand.
• What does [1,2,3].foldl (· * ·) 1 evaluate to?
• Which runs first in (inc ∘ dbl) 5?