Types

A structure is a product type
- Possible values are the cross-product of the values of the first field with the values of the second field, etc.
Explore other kinds of types

Sum Types

-- A sum type that can hold either a String or an Int
inductive StringOrInt where
  | str : String → StringOrInt
  | num : Int → StringOrInt
deriving Repr

-- Construct a value of each kind
def greeting : StringOrInt := StringOrInt.str "hello"
def answer : StringOrInt := StringOrInt.num 42

#eval greeting
#eval answer

-- A list can hold a mix of both
def mixed : List StringOrInt := [
  StringOrInt.str "hello",
  StringOrInt.num 42,
  StringOrInt.str "world"
]

#eval mixed

-- Use pattern matching to extract the value
def describe (x : StringOrInt) : String :=
  match x with
  | StringOrInt.str s => s!"string: \"{s}\""
  | StringOrInt.num n => s!"number: {n}"

#eval describe greeting
#eval describe answer

StringOrInt.str "hello"
StringOrInt.num 42
[StringOrInt.str "hello", StringOrInt.num 42, StringOrInt.str "world"]
"string: \"hello\""
"number: 42"

An sum type is a choice between alternatives
- The possible values are the sum of the possibilities of each alternative
- Use inductive to define one: we'll explain the name later (DEBT)
StringOrInt is a type whose values wrap either a String or an Int
- StringOrInt.str constructs a string-flavored value
- StringOrInt.num constructs a number-flavored value
deriving Repr is like Python's __repr__
- We'll explain why it's called deriving later (DEBT)
Since every element of the list has type StringOrInt, the list is homogeneous
Use match to extract the wrapped value
- The compiler checks that you handle both cases
We've already seen a sum type: Option in basics is either some or none

Trees

-- A binary tree with strings at the leaves
inductive Tree where
  | leaf : String → Tree
  | node : Tree → Tree → Tree
deriving Repr

-- Build a tree
def myTree : Tree :=
  Tree.node
    (Tree.node
      (Tree.leaf "alpha")
      (Tree.leaf "beta"))
    (Tree.leaf "gamma")

#eval myTree

-- Calculate total length of all strings in the tree
def totalLength (t : Tree) : Nat :=
  match t with
  | Tree.leaf s => s.length
  | Tree.node left right => totalLength left + totalLength right

#eval totalLength myTree

Tree.node (Tree.node (Tree.leaf "alpha") (Tree.leaf "beta")) (Tree.leaf "gamma")
14

inductive can define recursive types, not just flat sums
- Tree is either a leaf containing a String…
- …or a node containing two Trees
Like defining a Python class where each instance is either a leaf or a branch
- But the compiler enforces that you can't mix the two accidentally
This is why the keyword is inductive
- The definition refers to itself: node takes two Tree arguments
- Like mathematical induction: base cases (leaf) and inductive steps (node)
totalLength uses match on the tree shape
Compiler checks that code handles both leaf and node cases
- Same exhaustiveness guarantee as match on lists

Polymorphism

-- A polymorphic binary tree: leaves can be any type α
inductive Tree (α : Type) where
  | leaf : α → Tree α
  | node : Tree α → Tree α → Tree α
deriving Repr

-- A function that works for trees of any type
def countLeaves (t : Tree α) : Nat :=
  match t with
  | Tree.leaf _ => 1
  | Tree.node left right => countLeaves left + countLeaves right

-- A tree of numbers
def numTree : Tree Nat :=
  Tree.node
    (Tree.node
      (Tree.leaf 1)
      (Tree.leaf 2))
    (Tree.leaf 3)

#eval numTree
#eval countLeaves numTree

Tree.node (Tree.node (Tree.leaf 1) (Tree.leaf 2)) (Tree.leaf 3)
3

Add a type parameter to make a type work with any element type
α (alpha) is the conventional Greek letter for the first type parameter
- Type it as \a in Lean
Same inductive shape as the string-only Tree above
- But now leaf can hold any type
numTree and strTree are the same shape, different leaf types
- The compiler prevents you from putting a string leaf in numTree
countLeaves works on Tree α for any α
- Uses _ in the leaf branch because it doesn't need the value, just the count

Enumerations

-- A sum type with no data: just labels
inductive Season where
  | spring | summer | fall | winter
deriving BEq, Repr

#eval Season.summer
#eval Season.summer == Season.winter
#eval Season.summer == Season.summer

Season.summer
false
true

An enumeration is a sum type where no constructor carries data
- Like Python's enum.Enum
inductive Season defines four possible values with no extra payload
deriving BEq generates the == operator
- Without it, you can't compare Season values
- We'll explain the name BEq later (DEBT)

Sum Types with Data

-- A sum type where each constructor carries different data
inductive Shape where
  | circle (radius : Float)
  | rect (width : Float) (height : Float)
deriving Repr

def s1 : Shape := Shape.circle 3.0
def s2 : Shape := Shape.rect 2.0 5.0

#eval s1
#eval s2

Shape.circle 3.000000
Shape.rect 2.000000 5.000000

Constructors in a sum type can carry one or more data fields
- Shape.circle takes a Float for the radius
- Shape.rect takes two Floats for width and height
Like a tagged union where each tag stores different-shaped data
- Python equivalent: a @dataclass discriminator field plus a union of subclasses

Pattern Matching on Sum Types

-- Pattern matching must handle every constructor
inductive Shape where
  | circle (radius : Float)
  | rect (width : Float) (height : Float)

def area : Shape → Float
  | Shape.circle r => 3.14159 * r * r
  | Shape.rect w h => w * h

#eval area (Shape.circle 3.0)
#eval area (Shape.rect 2.0 5.0)

28.274310
10.000000

match on a sum type works exactly like match on a list
- Each constructor gets its own branch
- The compiler checks that every constructor is handled
area is written in definition-by-cases style
- Shape.circle r => … destructures the constructor and binds r
If you forget a case, the compiler rejects the definition entirely
- Unlike Python, where a missing case silently falls through or raises at runtime

`deriving` Explained

-- 'deriving' generates boilerplate for common type classes
inductive Color where
  | red | green | blue
deriving BEq, Repr

-- 'deriving BEq' lets us compare values with ==
#eval Color.red == Color.green
#eval Color.red == Color.red

-- 'deriving Repr' makes #eval display values readably
#eval Color.blue

false
true
Color.blue

deriving tells the compiler to generate code for common type classes
- (DEBT) A bigger topic we'll return to later
deriving Repr generates a readable display for #eval
deriving BEq generates ==
- Without it, comparing Color values is a compile error

`Option` is a Sum Type

-- Option is defined in the standard library as:
-- inductive Option (α : Type) where
--   | none : Option α
--   | some (val : α) : Option α

-- So you can pattern match on it like any other sum type
def describeOpt (x : Option Int) : String :=
  match x with
  | Option.none => "nothing"
  | Option.some n => s!"got {n}"

#eval describeOpt (Option.some 42)
#eval describeOpt Option.none

"got 42"
"nothing"

Option isn't magic: it's defined as an inductive type in the standard library
- Option.none is a constructor with no data
- Option.some is a constructor that carries one value of type α
Because it's a regular sum type, you can pattern match on it directly
- No special syntax: the same match you already know
Everything we learned about Option in basics was sum types all along

`List` is a Recursive Inductive Type

-- List is defined in the standard library as:
-- inductive List (α : Type) where
--   | nil : List α
--   | cons (head : α) (tail : List α) : List α

-- [] is shorthand for List.nil
-- head :: tail is shorthand for List.cons head tail

#check []
#check 1 :: [2, 3]
#check List.cons 1 (List.cons 2 (List.cons 3 List.nil))

[] : List ?m.1
[1, 2, 3] : List Nat
[1, 2, 3] : List Nat

List is also an inductive type with two constructors
- nil for the empty list (written [])
- cons for adding an element to the front (written head :: tail)
- The name "cons" is short for "construct", and goes back to the 1950s
:: is just syntactic sugar for List.cons
[] is syntactic sugar for List.nil
This is why match on lists uses [] and head :: tail: they are the two constructors of the underlying inductive type

Computing on Inductive Types

-- A tiny expression language: numbers, addition, multiplication
inductive Expr where
  | num (n : Int)
  | add (left : Expr) (right : Expr)
  | mul (left : Expr) (right : Expr)
deriving Repr

-- Evaluate an expression by recursing on its structure
def eval : Expr → Int
  | Expr.num n => n
  | Expr.add l r => eval l + eval r
  | Expr.mul l r => eval l * eval r

def e : Expr := Expr.add (Expr.num 3) (Expr.mul (Expr.num 4) (Expr.num 5))
#eval e
#eval eval e

Expr.add (Expr.num 3) (Expr.mul (Expr.num 4) (Expr.num 5))
23

Create a tiny expression language in four lines
- Expr.num wraps a plain integer
- Expr.add and Expr.mul each contain two sub-expressions
eval is a recursive function that mirrors the type structure
"Define a type, then write functions by cases" is the heart of Lean

Generic Sum Types

-- A generic sum type for success or failure
inductive Result (α : Type) (β : Type) where
  | ok (val : α)
  | err (msg : β)
deriving Repr

def divide (a : Int) (b : Int) : Result Int String :=
  if b == 0 then
    Result.err "division by zero"
  else
    Result.ok (a / b)

#eval divide 10 2
#eval divide 10 0

Result.ok 5
Result.err "division by zero"

A sum type can have multiple type parameters
- Result α β is generic over both the success type and the error type
Like Rust's Result or Haskell's Either
Cleaner than Python's convention of returning (value, error) tuples
- The compiler forces the caller to handle both ok and err

`match` with Conditions

-- Use conditionals inside match branches when constructors aren't enough
def describe (n : Int) : String :=
  match n with
  | n' =>
    if n' > 0 then "positive"
    else if n' < 0 then "negative"
    else "zero"

#eval describe 5
#eval describe (-3)
#eval describe 0

"positive"
"negative"
"zero"

Sometimes constructors alone aren't enough: you need finer discrimination
match arms are just expressions, so you can use if/else if/else inside them
- The n' pattern matches any Int, then the conditional further refines the result
- Pronounced "en prime"
The compiler still checks that the match is exhaustive
- A single n' branch covers all Int values, so no catch-all is needed here

Nested Patterns

-- Match on nested types: destructure an Option containing a List
def describeOptList (x : Option (List Int)) : String :=
  match x with
  | Option.none => "nothing"
  | Option.some [] => "empty list"
  | Option.some [n] => s!"singleton: {n}"
  | Option.some _ => "longer list"

#eval describeOptList Option.none
#eval describeOptList (Option.some [])
#eval describeOptList (Option.some [7])
#eval describeOptList (Option.some [1, 2, 3])

"nothing"
"empty list"
"singleton: 7"
"longer list"

Types combine: you can have an Option containing a List
match handles this by nesting patterns
- Option.some [] matches a some wrapping an empty list
- Option.some [n] destructures the list inside the option
Like Python's structural pattern matching (match/case)
- But again, the compiler verifies that every combination is covered

Product Types are Inductive

-- A structure groups related values under one name
structure Point where
  x : Float
  y : Float
deriving Repr

-- A product type is really an inductive with a single constructor
inductive Point' where
  | mk (x : Float) (y : Float)
deriving Repr

def p1 : Point := { x := 1.0, y := 2.0 }
def p2 : Point' := Point'.mk 1.0 2.0

#eval p1
#eval p2

{ x := 1.000000, y := 2.000000 }
Point'.mk 1.000000 2.000000

structure is syntactic sugar for inductive with exactly one constructor
- Point.mk 1.0 2.0 and { x := 1.0, y := 2.0 } are equivalent
Product types (structures) and sum types are both inductive under the hood
- A structure has one constructor; a sum type has two or more
The type system unifies both concepts

A Command Interpreter

-- A tiny command language in three lines of type definition
inductive Cmd where
  | forward (steps : Nat)
  | turn (degrees : Int)
  | say (msg : String)
deriving Repr

-- Pattern matching plus recursion equals an interpreter
def run (cmds : List Cmd) : String :=
  match cmds with
  | [] => "done"
  | Cmd.say msg :: rest => s!"said '{msg}'; {run rest}"
  | Cmd.forward n :: rest => s!"moved {n}; {run rest}"
  | Cmd.turn d :: rest => s!"turned {d}°; {run rest}"

def program : List Cmd := [
  Cmd.forward 3,
  Cmd.say "hello",
  Cmd.turn 90
]

#eval run program

"moved 3; said 'hello'; turned 90°; done"

Define a tiny domain-specific language in three lines of type definition
- Cmd.forward n moves forward n steps
- Cmd.turn d turns d degrees
- Cmd.say msg prints a message
run is an interpreter: pattern matching plus recursion over the command list
This is the payoff: define your data shapes with inductive, then process them with match

Exercises

Fix: Missing Constructor in Match

-- This function should describe a StringOrInt, but the match
-- is missing a case. Fix it.
inductive StringOrInt where
  | str : String → StringOrInt
  | num : Int → StringOrInt

def describe (x : StringOrInt) : String :=
  match x with
  | StringOrInt.str s => s!"string: \"{s}\""

hint

The describe function only handles StringOrInt.str but not StringOrInt.num
Add a branch for the num constructor that formats the integer value

Fix: Missing `deriving` Clause

-- Comparing Color values should work, but the code won't compile.
-- Fix it by adding a `deriving` clause.
inductive Color where
  | red | green | blue

def isRed (c : Color) : Bool :=
  c == Color.red

hint

Color is missing a deriving clause
The == operator needs a BEq instance to compare values
Add deriving BEq (and Repr wouldn't hurt) to the inductive line

Fix: Missing Base Case in Recursion

-- This function should sum all numbers in a tree, but the match
-- is missing the leaf case. Fix it.
inductive IntTree where
  | leaf : Int → IntTree
  | node : IntTree → IntTree → IntTree

def totalSum (t : IntTree) : Int :=
  match t with
  | IntTree.node left right => totalSum left + totalSum right

hint

totalSum handles IntTree.node but not IntTree.leaf
The compiler rejects incomplete pattern matches on inductive types
Add a branch for IntTree.leaf n that returns n

Fix: Unhandled Error Case

-- This function should describe both success and failure,
-- but the match only handles the ok case. Fix it.
inductive Result (α : Type) (β : Type) where
  | ok (val : α)
  | err (msg : β)

def describe (r : Result Int String) : String :=
  match r with
  | Result.ok n => s!"success: {n}"

hint

describe only matches Result.ok but not Result.err
The compiler checks that every constructor of a sum type is handled
Add a branch for Result.err msg that formats the error message

Fix: Missing Case in `eval`

-- This eval function should handle all expression types,
-- but the mul case is missing. Fix it.
inductive Expr where
  | num (n : Int)
  | add (left : Expr) (right : Expr)
  | mul (left : Expr) (right : Expr)

def eval : Expr → Int
  | Expr.num n => n
  | Expr.add l r => eval l + eval r

hint

eval handles Expr.num and Expr.add but not Expr.mul
The compiler reports which constructors are missing
Add a line for Expr.mul l r that calls eval on both sides and multiplies

Fix: Wrong Return Type

-- Count the leaves in a polymorphic tree. The return type
-- annotation is wrong. Fix it.
inductive Tree (α : Type) where
  | leaf : α → Tree α
  | node : Tree α → Tree α → Tree α

def countLeaves (t : Tree α) : String :=
  match t with
  | Tree.leaf _ => 1
  | Tree.node left right => countLeaves left + countLeaves right

hint

The countLeaves function body returns Nat values (1, + on Nat)
But the type annotation says String
Fix the return type annotation to match what the body actually computes

Write: Weekday or Weekend

-- Write a function 'isWeekend' that returns true for Saturday and Sunday.
inductive Day where
  | monday | tuesday | wednesday | thursday | friday | saturday | sunday
deriving BEq, Repr

def isWeekend (d : Day) : Bool :=
  false

#guard isWeekend Day.saturday == true
#guard isWeekend Day.sunday == true
#guard isWeekend Day.monday == false

hint

Use match on the Day argument to check which day it is
Return true for Day.saturday and Day.sunday, false for everything else
Use _ as a catch-all for the five weekdays to keep the code short

Write: Tree Height

-- Write a function 'height' that computes the height of a Tree.
-- The height of a leaf is 0; a node's height is 1 + max of children.
inductive Tree (α : Type) where
  | leaf : α → Tree α
  | node : Tree α → Tree α → Tree α
deriving Repr

def height (t : Tree α) : Nat :=
  0

#guard height (Tree.leaf "x") == 0
#guard height (Tree.node (Tree.leaf "a") (Tree.leaf "b")) == 1
#guard height (Tree.node (Tree.node (Tree.leaf "a") (Tree.leaf "b")) (Tree.leaf "c")) == 2

hint

Use match t with to handle the two constructors: Tree.leaf and Tree.node
A leaf has height 0; a node's height is 1 plus the larger of its children
Use Nat.max to compare two Nat values

Write: Map from Scratch

-- Write 'myMap' that works like List.map, but using the inductive
-- List constructors directly (List.nil and List.cons) instead of
-- the [] and :: shorthand. This reveals what's really happening.
def myMap (f : α → β) (xs : List α) : List β :=
  []

#guard myMap (fun x => x + 1) [] == []
#guard myMap (fun x => x + 1) [1, 2, 3] == [2, 3, 4]

hint

Use match on the list with the inductive constructors: List.nil and List.cons
List.nil is the empty list; List.cons h t puts element h at the front of list t
In the cons case, apply f to the head and recurse on the tail

Write: Safe Division

-- Write 'safeDiv' that returns an Option Int:
-- Option.some of the quotient if b ≠ 0, Option.none otherwise.
def safeDiv (a : Int) (b : Int) : Option Int :=
  Option.none

#guard safeDiv 10 2 == Option.some 5
#guard safeDiv 10 0 == Option.none
#guard safeDiv 0 5 == Option.some 0

hint

Check if b is zero using an if/else expression
Return Option.none when b == 0, Option.some (a / b) otherwise
This is like Python's None but the compiler forces callers to handle it

Write: Mirror a Tree

-- Write 'mirrorTree' that swaps left and right subtrees of every node.
-- A leaf is unchanged.
inductive Tree (α : Type) where
  | leaf : α → Tree α
  | node : Tree α → Tree α → Tree α
deriving BEq, Repr

def mirrorTree (t : Tree α) : Tree α :=
  t

#guard mirrorTree (Tree.leaf 1) == Tree.leaf 1
#guard mirrorTree (Tree.node (Tree.leaf "a") (Tree.leaf "b")) == Tree.node (Tree.leaf "b") (Tree.leaf "a")

hint

Use match t with to distinguish Tree.leaf from Tree.node
A leaf is unchanged: return it as-is
For a node, create a new node with left and right subtrees swapped using recursion

Write: Get or Else

-- Write 'getOrElse' that returns the value inside an Option if it's 'some',
-- or a default value if it's 'none'.
def getOrElse (opt : Option α) (default : α) : α :=
  default

#guard getOrElse (Option.some 5) 0 == 5
#guard getOrElse (Option.none : Option Int) 0 == 0
#guard getOrElse (Option.some "hello") "world" == "hello"

hint

Use match opt with to handle Option.some and Option.none
Option.some val means return val (ignore the default)
Option.none means return the default argument

Types

Sum Types

Trees

Polymorphism

Enumerations

Sum Types with Data

Pattern Matching on Sum Types

deriving Explained

Option is a Sum Type

List is a Recursive Inductive Type

Computing on Inductive Types

Generic Sum Types

match with Conditions

Nested Patterns

Product Types are Inductive

A Command Interpreter

Exercises

Fix: Missing Constructor in Match

Fix: Missing deriving Clause

Fix: Missing Base Case in Recursion

Fix: Unhandled Error Case

Fix: Missing Case in eval

Fix: Wrong Return Type

Write: Weekday or Weekend

Write: Tree Height

Write: Map from Scratch

Write: Safe Division

Write: Mirror a Tree

Write: Get or Else

`deriving` Explained

`Option` is a Sum Type

`List` is a Recursive Inductive Type

`match` with Conditions

Fix: Missing `deriving` Clause

Fix: Missing Case in `eval`