Module 1 · Lesson 3

Functions & Definitions

Functions are the heart of Lean programming. Learn to define them with explicit types, type inference, named arguments, and default values.

Basic Function Definitions

Use the def keyword to define functions. The syntax is clean and expressive:

lean

1-- A function with explicit types
2def add (x : Nat) (y : Nat) : Nat := x + y
3
4-- Using the function
5#eval add 3 5  -- 8
6
7-- A function that takes a String
8def greet (name : String) : String := "Hello, " ++ name ++ "!"
9
10#eval greet "Lean"  -- "Hello, Lean!"

The pattern is: def name (params) : ReturnType := body. Each parameter has its own parentheses and type annotation.

Type Inference

Lean's type inference is powerful. You can often omit types and let the compiler figure them out:

lean

1-- Type inferred for simple values
2def x := 42          -- Inferred: Nat
3def name := "Alice"  -- Inferred: String
4
5-- The RETURN type can be inferred from the body
6def double (x : Nat) := x + x   -- : Nat, inferred from x + x
7
8-- But a bare parameter cannot be inferred:
9-- def double' x := x + x
10-- error: typeclass instance problem is stuck, HAdd ?m ?m ?m
11--
12-- Lean has nothing to go on: x + x works for Nat, Int, Float, ...
13-- so it cannot pick one. Unlike Hindley-Milner languages, Lean does NOT
14-- generalise over unknown types here, because + is resolved by type class
15-- lookup and the class needs a concrete type first.
16
17-- Fix: annotate the parameter
18def double'' (x : Nat) : Nat := x + x

💡

Rule of thumb: annotate parameters always, and the return typewhenever the function is more than one line. Parameter types are usually required anyway; return types are optional but they turn a confusing error deep inside the body into a clear error at the signature.

Common Pitfalls

Beginners often run into small syntax gotchas. Keep these in mind as you practice.

Each parameter usually gets its own parentheses unless you group same-typed parameters.
Lean is expression-based—every branch must return the same type.
Use := for definitions and = for equations.

Multiple Parameters

Functions can take multiple parameters. Each parameter is in its own parentheses, or you can group parameters of the same type:

lean

1-- Each parameter separate
2def add1 (x : Nat) (y : Nat) : Nat := x + y
3
4-- Grouped parameters of same type  
5def add2 (x y : Nat) : Nat := x + y
6
7-- Mixed types
8def describe (name : String) (age : Nat) : String :=
9  s!"{name} is {age} years old"
10
11#eval describe "Alice" 30  -- "Alice is 30 years old"

Named Arguments

You can call functions with named arguments for clarity:

lean

1def greet (name : String) (formal : Bool) : String :=
2  if formal then s!"Good day, {name}." else s!"Hey {name}!"
3
4-- Positional arguments
5#eval greet "Alice" true   -- "Good day, Alice."
6
7-- Named arguments (order doesn't matter)
8#eval greet (name := "Bob") (formal := false)  -- "Hey Bob!"
9#eval greet (formal := true) (name := "Carol") -- "Good day, Carol."

Default Values

Parameters can have default values, making them optional:

lean

1def greet (name : String) (formal : Bool := false) : String :=
2  if formal then s!"Good day, {name}." else s!"Hey {name}!"
3
4-- Using default
5#eval greet "Alice"        -- "Hey Alice!" (formal defaults to false)
6
7-- Override default
8#eval greet "Bob" true     -- "Good day, Bob."
9
10-- Named argument to override
11#eval greet "Carol" (formal := true)  -- "Good day, Carol."

Key Takeaway

Parameters with := value are optional. This pattern is common for configuration options and flags.

Anonymous Functions (Lambdas)

Create inline functions with fun (or the Unicode λ):

lean

1-- Lambda syntax
2#eval (fun x => x + 1) 5     -- 6
3#eval (fun x y => x * y) 3 4 -- 12
4
5-- With type annotations
6#eval (fun (x : Nat) => x * 2) 5  -- 10
7
8-- Unicode lambda (optional but pretty)
9#eval (λ x => x + 1) 5  -- 6
10
11-- Lambdas are often used with higher-order functions
12#eval [1, 2, 3].map (fun x => x * 2)  -- [2, 4, 6]
13
14-- A lambda can pattern match directly, with no "match" keyword
15#eval [0, 1, 5].map (fun | 0 => "zero" | _ => "nonzero")
16-- ["zero", "nonzero", "nonzero"]

Equation-Style Definitions

When a function is defined entirely by cases on its argument, you can skip the match and write the equations directly after the type. This is the style you will see throughout the standard library.

lean

1-- Give the TYPE, then the equations — no parameter names, no :=
2def isZero : Nat → Bool
3  | 0 => true
4  | _ => false
5
6#eval isZero 0   -- true
7#eval isZero 3   -- false
8
9-- Equivalent long form
10def isZero' (n : Nat) : Bool :=
11  match n with
12  | 0 => true
13  | _ => false
14
15-- Multiple arguments: one pattern per argument, separated by commas
16def bothZero : Nat → Nat → Bool
17  | 0, 0 => true
18  | _, _ => false
19
20-- You can mix: name some parameters, match on the rest
21def replicate (n : Nat) : α → List α
22  | a => List.replicate n a

💡

The equation style is not just shorter. Lean generates equation lemmasfrom these cases (isZero.eq_1, isZero.eq_2, …) which simp and rw can use when you later prove things about the function. You get the same lemmas from a match, but the equation form makes the case split visible in the signature.

def, abbrev, example, and theorem

def is one of a family of declaration keywords. They differ in how eagerly Lean unfolds them and in what they are for:

lean

1-- def: the normal case. Semi-reducible — unfolds when asked (simp [f], unfold f)
2def Celsius := Float
3
4-- abbrev: fully reducible. Behaves as a transparent alias everywhere,
5-- including for type class search and definitional equality
6abbrev Name := String
7def hi (n : Name) : String := "hi " ++ n
8#eval hi "Ada"        -- works: Name IS String as far as Lean is concerned
9
10-- example: an anonymous declaration, checked and then discarded.
11-- Perfect for the code samples on this page.
12example : 1 + 1 = 2 := rfl
13
14-- theorem: like def, but the result is a Prop and the body is a proof.
15-- Proofs are irrelevant, so theorem bodies are never unfolded during evaluation.
16theorem two_eq : 1 + 1 = 2 := rfl

⚠

Use abbrev for type synonyms you want to be transparent, and def when you want a genuinely distinct name. Choosing def Celsius := Float above means Lean will notautomatically accept a Float where a Celsius is expected in type class search — often exactly what you want, occasionally a source of confusing errors.

partial def

Every Lean function must terminate, and Lean must be able to see why. When it cannot — or when the recursion genuinely may not terminate — mark the definition partial.

lean

1-- Lean cannot prove this terminates (n * 2 is not "smaller" than n)
2partial def doubleUntilBig (n : Nat) : Nat :=
3  if n > 100 then n else doubleUntilBig (n * 2)
4
5#eval doubleUntilBig 1   -- 128

ℹ

partial is a real trade-off, not a magic escape hatch. The function still compiles and runs, but Lean treats its body as opaque: you cannot unfold it in a proof, and rfl/decide will not evaluate it. Use it for I/O loops and interpreters; avoid it for anything you intend to reason about. The Termination lesson shows how to discharge the obligation properly with termination_by instead.

variable: Shared Parameters

When several declarations take the same parameter, variabledeclares it once. Lean adds it to any declaration that mentions it — and only to those.

lean

1variable (k : Nat)
2
3def addK (n : Nat) : Nat := n + k
4#check addK          -- addK (k n : Nat) : Nat  — k was inserted automatically
5
6def noK (n : Nat) : Nat := n + 1
7#check noK           -- noK (n : Nat) : Nat     — k was NOT inserted

⚠

Note the parameter order: k is inserted before n, because variables come first. This trips people up when they add a variable to an existing file and every call site silently changes meaning.

Implicit Arguments

Some arguments can be inferred from context. These are marked with curly braces:

lean

1-- The type α is implicit - Lean infers it
2def identity {α : Type} (x : α) : α := x
3
4-- Lean infers α = Nat from the argument
5#eval identity 42        -- 42
6#eval identity "hello"   -- "hello" (α = String)
7
8-- You can provide implicit args explicitly with @
9#eval @identity Nat 42   -- 42

Deep Dive: Why Implicit Arguments?

Implicit arguments reduce verbosity. Without them, you'd have to writeidentity Nat 42 every time, even though Lean can clearly see 42 is a Nat.

The @ prefix makes all arguments explicit, which is useful when type inference fails or you want to be specific.

Instance-Implicit Arguments

Square brackets [...] denote instance-implicit arguments. Lean automatically finds type class instances:

lean

1-- [BEq α] means "α must have equality defined"
2def contains [BEq α] (xs : List α) (target : α) : Bool :=
3  xs.any (· == target)
4
5-- Lean finds the BEq instance automatically
6#eval contains [1, 2, 3] 2        -- true
7#eval contains ["a", "b"] "c"     -- false
8
9-- Multiple instance arguments: require everything the body actually uses
10def summarise [Ord α] [ToString α] (xs : List α) : String :=
11  let sorted := xs.mergeSort (fun a b => compare a b != .gt)
12  ", ".intercalate (sorted.map toString)
13
14#eval summarise [3, 1, 2]         -- "1, 2, 3"
15
16-- Named instance argument: gives you a handle on the instance itself
17def customCompare [inst : Ord α] (x y : α) : Ordering :=
18  inst.compare x y
19
20#eval customCompare 1 2           -- Ordering.lt

ℹ

Instance arguments are the bridge between type classes and functions. When you write [BEq α], Lean finds the appropriate equality implementation at compile time.

Autobound Implicit Arguments

When you use an undeclared lowercase identifier as a type, Lean automatically makes it an implicit argument:

lean

1-- These are equivalent:
2def first1 (xs : List α) : Option α := xs.head?
3def first2 {α : Type} (xs : List α) : Option α := xs.head?
4
5-- α is automatically bound as {α : Type}
6
7-- Works with multiple type variables
8def zip (xs : List α) (ys : List β) : List (α × β) := 
9  xs.zip ys
10-- Both α and β are autobound
11
12-- Disable with set_option
13set_option autoImplicit false in
14def explicit {α : Type} (x : α) : α := x

Function Types

Functions have types expressed with arrows. Understanding these helps you read library documentation:

lean

1-- Single argument function
2#check (fun x => x + 1 : Nat → Nat)
3
4-- Multiple arguments (curried)
5#check (fun x y => x + y : Nat → Nat → Nat)
6-- Read as: takes a Nat, returns a function Nat → Nat
7
8-- With implicit arguments
9#check @List.map
10-- {α : Type} → {β : Type} → (α → β) → List α → List β

Partial Application

Because multi-argument functions are curried, you can partially apply them:

lean

1def add (x y : Nat) : Nat := x + y
2
3-- Partially apply: fix the first argument
4def add5 := add 5  -- add5 : Nat → Nat
5
6#eval add5 3   -- 8
7#eval add5 10  -- 15
8
9-- Useful with higher-order functions
10#eval [1, 2, 3].map (add 10)  -- [11, 12, 13]

Function Composition

Compose small functions into larger ones using · withFunction.comp or the ∘ operator.

lean

1def double (n : Nat) : Nat := n * 2
2def inc (n : Nat) : Nat := n + 1
3
4def doubleThenInc : Nat → Nat := inc ∘ double
5def incThenDouble : Nat → Nat := double ∘ inc
6
7#eval doubleThenInc 3  -- 7
8#eval incThenDouble 3  -- 8

Exercise: Compose Functions

Define a function that squares a number, then converts it to a string.

lean

1def square (n : Nat) : Nat := n * n
2def toText (n : Nat) : String := toString n
3
4def squareToString : Nat → String :=
5  toText ∘ square
6
7#eval squareToString 12  -- "144"

Where Clauses

For complex functions, use where to define helpers:

lean

1def quadratic (a b c x : Float) : Float := 
2  a * x^2 + b * x + c
3
4-- Cleaner with where
5def quadratic' (a b c x : Float) : Float := 
6  term1 + term2 + term3
7where
8  term1 := a * x^2
9  term2 := b * x
10  term3 := c
11
12#eval quadratic' 1 2 1 3  -- 16.000000

ℹ

where helpers can take arguments and can be recursive, which let cannot. That makes where the standard place to put an accumulator loop:

lean

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

Primitives & Basic Types Next: Local Scope