# 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.

```lean id="r8bp2h"
structure Point where
  x : Nat
  y : Nat
deriving Repr
```

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

```lean id="xf8e0h"
#check Point
#check Point.x
#check Point.y
```

Typical output:

```text id="lmkg2f"
Point : Type
Point.x : Point -> Nat
Point.y : Point -> Nat
```

The field names become projection functions.

## Constructing a Structure

Use record syntax.

```lean id="fu9nlx"
def origin : Point :=
  { x := 0, y := 0 }

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

#eval origin
#eval p
```

Expected output:

```text id="cjoi7q"
{ 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.

```lean id="n7bxkc"
#eval p.x
#eval p.y
```

Expected output:

```text id="wh59a6"
3
4
```

The expression:

```lean id="mc175f"
p.x
```

is notation for:

```lean id="ykvlp7"
Point.x p
```

This means fields are ordinary functions.

## Functions over Structures

A function can consume a structure by using projections.

```lean id="bzl4tm"
def Point.sum (p : Point) : Nat :=
  p.x + p.y

#eval p.sum
```

Expected output:

```text id="6v7grw"
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.

```lean id="c25kg4"
def Point.swap : Point -> Point
| { x := a, y := b } => { x := b, y := a }

#eval p.swap
```

Expected output:

```text id="0y57bo"
{ 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.

```lean id="se2ro7"
def moveRight (p : Point) : Point :=
  { p with x := p.x + 1 }

#eval moveRight p
```

Expected output:

```text id="0snu4n"
{ x := 4, y := 4 }
```

All fields not mentioned are copied from `p`.

## Structures with Parameters

A structure may depend on a type parameter.

```lean id="97f2uu"
structure PairBox (α : Type) where
  first : α
  second : α
deriving Repr
```

Use it with different types:

```lean id="dd1dgm"
def natPair : PairBox Nat :=
  { first := 1, second := 2 }

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

#eval natPair
#eval stringPair
```

Expected output:

```text id="c6urle"
{ first := 1, second := 2 }
{ first := "a", second := "b" }
```

## Implicit Parameters in Structures

For reusable structures, universe-polymorphic parameters are common.

```lean id="mnw2iy"
universe u

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

Lean can infer the parameter from a value.

```lean id="wkbmcr"
def boxedNat : Box Nat :=
  { value := 10 }

#check boxedNat.value
```

## Structures as Bundles

A structure can bundle data with properties.

```lean id="v4vkp7"
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.

```lean id="fhgc37"
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.

```lean id="equutl"
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.

```lean id="xohpzr"
structure ColoredPoint extends Point where
  color : String
deriving Repr
```

Construct a value:

```lean id="idjms5"
def cp : ColoredPoint :=
  { x := 3, y := 4, color := "red" }

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

Expected output:

```text id="n0rir3"
{ 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`.

```lean id="l9n189"
#check Point.mk
```

Output:

```text id="x50som"
Point.mk : Nat -> Nat -> Point
```

You can construct values positionally:

```lean id="m7tq5v"
def q : Point :=
  Point.mk 8 9
```

Record syntax is usually clearer than positional construction.

## Custom Constructor Names

You can name the constructor.

```lean id="s01sf1"
structure User where
  mk ::
  name : String
  age : Nat
deriving Repr
```

Now:

```lean id="tegk1q"
#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.

```lean id="jpqypv"
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.

```lean id="vjqpcl"
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.