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.

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.

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]

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