1.17 Structures and Records

A structure is a type whose values are built from named fields. Structures are used when a concept is best represented by several pieces of data grouped together. They are also the foundation for many larger interfaces in Lean, including algebraic structures, configuration records, and bundled mathematical objects.

Problem

You want to define a record type, construct values with named fields, access those fields, and prove simple facts about structured data.

Solution

Use structure to declare a type with fields.

structure Point where
  x : Nat
  y : Nat
deriving Repr

This declares a type Point with two fields, x and y.

#check Point
#check Point.x
#check Point.y

Typical output:

Point : Type
Point.x : Point -> Nat
Point.y : Point -> Nat

The field names become projection functions.

Constructing a Structure

Use record syntax.

def origin : Point :=
  { x := 0, y := 0 }

def p : Point :=
  { x := 3, y := 4 }

#eval origin
#eval p

Expected output:

{ x := 0, y := 0 }
{ x := 3, y := 4 }

The field names make construction explicit and stable under field order changes.

Accessing Fields

Fields can be accessed by projection.

#eval p.x
#eval p.y

Expected output:

3
4

The expression:

p.x

is notation for:

Point.x p

This means fields are ordinary functions.

Functions over Structures

A function can consume a structure by using projections.

def Point.sum (p : Point) : Nat :=
  p.x + p.y

#eval p.sum

Expected output:

7

The name Point.sum places the function in the Point namespace. Lean allows dot notation when the first explicit argument has type Point.

Pattern Matching on Structures

You can decompose a structure by pattern matching.

def Point.swap : Point -> Point
| { x := a, y := b } => { x := b, y := a }

#eval p.swap

Expected output:

{ x := 4, y := 3 }

This form is useful when the function uses most fields directly.

Updating Structures

Use record update syntax to copy a value while changing selected fields.

def moveRight (p : Point) : Point :=
  { p with x := p.x + 1 }

#eval moveRight p

Expected output:

{ x := 4, y := 4 }

All fields not mentioned are copied from p.

Structures with Parameters

A structure may depend on a type parameter.

structure PairBox (α : Type) where
  first : α
  second : α
deriving Repr

Use it with different types:

def natPair : PairBox Nat :=
  { first := 1, second := 2 }

def stringPair : PairBox String :=
  { first := "a", second := "b" }

#eval natPair
#eval stringPair

Expected output:

{ first := 1, second := 2 }
{ first := "a", second := "b" }

Implicit Parameters in Structures

For reusable structures, universe-polymorphic parameters are common.

universe u

structure Box (α : Type u) where
  value : α

Lean can infer the parameter from a value.

def boxedNat : Box Nat :=
  { value := 10 }

#check boxedNat.value

Structures as Bundles

A structure can bundle data with properties.

structure PositiveNat where
  value : Nat
  positive : value > 0

A value of this type contains both a natural number and a proof that it is positive.

def fivePositive : PositiveNat :=
  { value := 5, positive := by decide }

The proof field is checked like any other field. This pattern is common in formal mathematics.

Proving Facts about Structures

Field projections give direct access to stored data.

theorem fivePositive_gt_zero : fivePositive.value > 0 := by
  exact fivePositive.positive

The proof is already part of the structure.

Extending Structures

One structure can extend another.

structure ColoredPoint extends Point where
  color : String
deriving Repr

Construct a value:

def cp : ColoredPoint :=
  { x := 3, y := 4, color := "red" }

#eval cp
#eval cp.x
#eval cp.color

Expected output:

{ toPoint := { x := 3, y := 4 }, color := "red" }
3
"red"

Extension lets a new structure reuse fields from an existing one.

Constructor Names

Lean creates a constructor for each structure. By default, it is named mk.

#check Point.mk

Output:

Point.mk : Nat -> Nat -> Point

You can construct values positionally:

def q : Point :=
  Point.mk 8 9

Record syntax is usually clearer than positional construction.

Custom Constructor Names

You can name the constructor.

structure User where
  mk ::
  name : String
  age : Nat
deriving Repr

Now:

#check User.mk

Custom constructor names are useful when the default mk would be unclear in generated terms.

Structure Equality

Two structure values are equal when their fields are equal.

theorem point_ext (p q : Point) (hx : p.x = q.x) (hy : p.y = q.y) : p = q := by
  cases p
  cases q
  simp at hx hy
  simp [hx, hy]

For many structures, Lean also provides extensionality support, depending on available declarations and imports. The practical principle is simple: to prove equality of records, prove equality of corresponding fields.

Common Pitfalls

If Lean cannot print a structure value, add deriving Repr.

If record construction fails, check that every required field is supplied.

If a field name is ambiguous, use the qualified projection name.

If record update fails, verify that Lean knows the type of the base record.

If a proof field fails, inspect its expected proposition with the editor goal view.

Recipe: Define a Configuration Record

Structures are useful for options and configuration.

structure SearchConfig where
  limit : Nat
  caseSensitive : Bool
  timeoutMs : Nat
deriving Repr

def defaultConfig : SearchConfig :=
  { limit := 10, caseSensitive := false, timeoutMs := 1000 }

def strictConfig : SearchConfig :=
  { defaultConfig with caseSensitive := true, limit := 5 }

#eval defaultConfig
#eval strictConfig

This gives a stable interface for passing grouped parameters through code.

Takeaway

A structure defines a record type with named fields. Values are built with record syntax, fields are accessed by projections, and updates copy existing records with selected changes. Structures scale from simple data records to bundled mathematical objects with proof fields, making them one of the central organizing tools in Lean.