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-- Type inferred for function parameters
6def double x := x + x   -- Inferred: Nat → Nat
7
8-- But explicit types are clearer for functions
9def double' (x : Nat) : Nat := x + x

💡

For functions, explicit type annotations serve as documentation and catch errors early. Prefer explicit types in your function signatures.

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]

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
10def sortAndDedupe [Ord α] [BEq α] (xs : List α) : List α :=
11  xs.mergeSort |>.dedup
12
13-- Named instance argument (rare but useful)
14def customCompare [inst : Ord α] (x y : α) : Ordering :=
15  inst.compare x y

ℹ

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
4    def squareToString : Nat → String :=
5      toText ∘ square
6
7#eval squareToString 12

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

Primitives & Basic Types Next: Local Scope