Module 1 · Level 3

Functions

Functions are the heart of Lean. Learn to define them with explicit types and use pattern matching to make them expressive.

Definitions with def

lean

1def add (x : Nat) (y : Nat) : Nat := x + y
2#eval add 3 5
3
4def greet (name : String) : String := "Hello, " ++ name
5#eval greet "Lean"

Lean uses match to branch on values.

lean

1def isZero (n : Nat) : Bool :=
2  match n with
3  | 0 => true
4  | _ => false
5
6#eval isZero 0
7#eval isZero 4

Exercise: Option Defaults

Define a function that extracts a value from Option Nat and returns a default when it is none.

lean

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

💡

Lean encourages small, pure functions. Keep them focused and let the types guide you.

Key Takeaway

Functions in Lean are pure by default. Pattern matching is the standard way to branch on data.