Structures

Structures let you model real-world data with named fields and strong type guarantees. They are Lean's record type — and the first tool that makes your programs read like the domain they describe.

Learning Goals

• Declare a structure and build values three different ways.
• Use deriving to get printing and equality for free.
• Update records without mutating them.
• Attach methods to your own types so dot notation works.
• Give fields defaults and reuse structures with extends.

Defining Structures

A structure declaration creates a new type, a constructor, and one accessor function per field. You can see all three with #check.

1structure User where
2  name : String
3  age  : Nat
4
5#check User        -- User : Type
6#check User.mk     -- User.mk (name : String) (age : Nat) : User
7#check User.name   -- User.name (self : User) : String
8
9def alice : User := { name := "Alice", age := 30 }
10
11#eval alice.name   -- "Alice"
12#eval alice.age    -- 30

alice.name is shorthand for User.name alice. Lean sees that alice has type User and looks the function up in the User namespace. This is the same mechanism that made "Lean".length work back in Level 2.

Making Your Structure Printable

Try #eval alice with the definition above and Lean will refuse: it has no idea how to display a User. Add deriving Repr and Lean writes the printing code for you.

1structure Point where
2  x : Nat
3  y : Nat
4deriving Repr
5
6def origin : Point := { x := 0, y := 0 }
7
8#eval origin       -- { x := 0, y := 0 }

Three Ways to Build a Value

1-- 1. Named fields — clearest, order does not matter
2def a : Point := { x := 3, y := 4 }
3
4-- 2. Anonymous constructor — concise, order does matter
5def b : Point := ⟨3, 4⟩
6
7-- 3. Explicit constructor call
8def c : Point := Point.mk 3 4

The angle brackets ⟨ ⟩ are typed as \< and \>in VS Code. They work whenever Lean already knows which type you are constructing. Prefer named fields for anything with more than two or three fields — positional arguments get misread.

Updating Records

Values in Lean are immutable. “Updating” a record means building a new one that copies the old fields, and { x with ... } is the syntax for it.

1def birthday (u : User) : User :=
2  { u with age := u.age + 1 }
3
4#eval (birthday alice).age   -- 31
5#eval alice.age              -- 30   ← the original is untouched
6
7def shiftX (p : Point) (d : Nat) : Point :=
8  { p with x := p.x + d }
9
10#eval shiftX ⟨3, 4⟩ 10       -- { x := 13, y := 4 }

Default Field Values

Fields can carry defaults, which makes configuration-style structures pleasant to use: supply only what differs from the norm.

1structure Config where
2  host  : String := "localhost"
3  port  : Nat := 8080
4  debug : Bool := false
5deriving Repr
6
7#eval ({} : Config)
8-- { host := "localhost", port := 8080, debug := false }
9
10#eval ({ port := 3000 } : Config)
11-- { host := "localhost", port := 3000, debug := false }

Methods and Dot Notation

To get myRect.area style calls on your own types, define the function inside a namespace matching the type name, taking the value as its first argument.

1namespace Point
2
3def norm1 (p : Point) : Nat := p.x + p.y
4
5def translate (p : Point) (dx dy : Nat) : Point :=
6  ⟨p.x + dx, p.y + dy⟩
7
8end Point
9
10#eval (⟨3, 4⟩ : Point).norm1          -- 7
11#eval (⟨3, 4⟩ : Point).translate 1 1  -- { x := 4, y := 5 }

Note how translate takes extra arguments after the structure: dot notation fills in the first argument of matching type and passes the rest along normally.

What Else You Can Derive

Repr is the one you will reach for first, but it is not alone. BEq gives you ==, and Inhabited gives you a default value.

1structure Pair where
2  a : Nat
3  b : Nat
4deriving Repr, BEq, Inhabited
5
6#eval (⟨1, 2⟩ : Pair) == (⟨1, 2⟩ : Pair)   -- true
7#eval (⟨1, 2⟩ : Pair) == (⟨1, 3⟩ : Pair)   -- false
8#eval (default : Pair)                     -- { a := 0, b := 0 }

Deriving works by generating instances of type classes— the mechanism behind all of Lean's overloaded notation. Level 9 shows you how to write these instances by hand.

Nesting and Extending

Structures compose. A field can be another structure, and accessors chain naturally.

1structure Address where
2  city : String
3  zip  : String
4deriving Repr
5
6structure Person where
7  name    : String
8  address : Address
9deriving Repr
10
11def bob : Person :=
12  { name := "Bob", address := { city := "Paris", zip := "75001" } }
13
14#eval bob.address.city    -- "Paris"

extends builds a structure that contains all the fields of another one, plus its own. Lean also generates a conversion back to the parent type.

1structure Employee extends Person where
2  salary : Nat
3deriving Repr
4
5def carol : Employee :=
6  { name := "Carol"
7  , address := { city := "Lyon", zip := "69001" }
8  , salary := 50000 }
9
10#eval carol.name       -- "Carol"    inherited field
11#eval carol.salary     -- 50000
12#eval carol.toPerson   -- { name := "Carol", address := ... }

Practice

1structure Product where
2  name  : String
3  price : Nat
4deriving Repr
5
6def discount (p : Product) : Product :=
7  { p with price := p.price - p.price / 10 }
8
9#eval discount { name := "Book", price := 100 }
10-- { name := "Book", price := 90 }

1structure Rect where
2  width  : Nat
3  height : Nat
4deriving Repr
5
6namespace Rect
7
8def area (r : Rect) : Nat := r.width * r.height
9def perimeter (r : Rect) : Nat := 2 * (r.width + r.height)
10def isSquare (r : Rect) : Bool := r.width == r.height
11
12end Rect
13
14#eval (⟨3, 4⟩ : Rect).area        -- 12
15#eval (⟨3, 4⟩ : Rect).perimeter   -- 14
16#eval (⟨3, 3⟩ : Rect).isSquare    -- true

Common Mistakes

• Forgetting deriving Repr.The resulting “failed to synthesize” error is intimidating but means only that.
• Expecting mutation. { u with age := 31 } returns a new record; it does not change u. Use the return value.
• Mixing up field order in ⟨ ⟩. Two fields of the same type will silently swap. Use named fields when it matters.
• Defining methods outside the namespace. Dot notation only finds Rect.area, not a top-level area.

Check Yourself

• What three things does structure User where ... generate?
• Why does #eval alice fail while #eval alice.name works?
• What does { p with x := 0 } do to p?
• Where must area live for r.area to compile?