Module 2 · Level 4

Structures

Structures let you model real-world data with named fields and strong type guarantees.

Defining Structures

lean

1structure User where
2  name : String
3  age : Nat
4
5#check User
6
7def alice : User := { name := "Alice", age := 30 }
8#eval alice.name

Lean supports record updates with { .. } syntax.

lean

1def birthday (user : User) : User :=
2  { user with age := user.age + 1 }
3
4#eval (birthday alice).age

Exercise: Product Modeling

Create a Product structure with a name and price, then write a function that applies a 10% discount.

lean

1structure Product where
2  name : String
3  price : Nat
4
5def discount (p : Product) : Product :=
6  { p with price := p.price - p.price / 10 }

ℹ

Structures are Lean's record types. They are invaluable for modeling domain data.

Key Takeaway

Structures model data with named fields and give you predictable, type-safe access.