Module 2 · Lesson 1

Products (Structures)

Structures bundle multiple values together into a single type. They're similar to structs in Rust/C or records in other functional languages.

Defining Structures

Use the structure keyword to define a new data type with named fields:

lean

1structure Point where
2  x : Float
3  y : Float
4
5-- Create instances
6def origin : Point := { x := 0.0, y := 0.0 }
7def p1 : Point := { x := 3.0, y := 4.0 }
8
9-- Access fields with dot notation
10#eval p1.x  -- 3.0
11#eval p1.y  -- 4.0

The where keyword introduces the field list. Each field has a name and a type.

Anonymous Constructor Syntax

For concise construction, use angle brackets ⟨...⟩, typed\< and \> (the longer abbreviations \langle and \rangle work too). There is no ASCII spelling of the brackets themselves — if you want to avoid Unicode entirely, name the constructor:

lean

1structure Point where
2  x : Float
3  y : Float
4
5-- Anonymous constructor (order matters!)
6def p1 : Point := ⟨3.0, 4.0⟩
7
8-- Every structure gets a constructor named .mk — this is the ASCII form
9def p2 : Point := Point.mk 3.0 4.0
10
11-- Named fields: order does NOT matter, and it documents itself
12def p3 : Point := { x := 3.0, y := 4.0 }
13def p4 : Point := { y := 4.0, x := 3.0 }   -- same value as p3
14
15-- There is also a "where" form, handy for long field lists
16def p5 : Point where
17  x := 3.0
18  y := 4.0

⚠

⟨...⟩ only works when Lean already knows the expected type. def p := ⟨3.0, 4.0⟩ fails — there is nothing to tell Lean you meant a Point rather than a pair. Annotate the definition, or use Point.mk.

ℹ

With anonymous constructors, field order matters. Named field syntax { x := ..., y := ... } is clearer for structures with many fields.

Default Field Values

Fields can have default values, making them optional during construction:

lean

1structure Config where
2  host : String := "localhost"
3  port : Nat := 8080
4  debug : Bool := false
5
6-- Use all defaults
7def defaultConfig : Config := {}
8
9-- Override some fields
10def prodConfig : Config := { port := 443, debug := false }
11
12-- Override all
13def customConfig : Config := { host := "api.example.com", port := 9000, debug := true }
14
15#eval defaultConfig.host  -- "localhost"
16#eval prodConfig.port     -- 443

Deriving Common Functionality

Use deriving to automatically generate useful instances:

lean

1structure Person where
2  name : String
3  age : Nat
4  deriving Repr, DecidableEq, Inhabited
5
6def alice : Person := { name := "Alice", age := 30 }
7def bob : Person := { name := "Bob", age := 25 }
8
9-- Repr allows #eval to print the structure
10#eval alice  -- { name := "Alice", age := 30 }
11
12-- DecidableEq allows equality comparison
13#eval alice == bob   -- false
14#eval alice == alice -- true
15
16-- Inhabited provides a default value
17#eval (default : Person)  -- { name := "", age := 0 }

Key Takeaway

deriving Repr is essential for debugging—it makes your structures printable with #eval.

Updating Structures

Structures are immutable, but you can create modified copies with "update" syntax:

lean

1structure Person where
2  name : String
3  age : Nat
4  deriving Repr
5
6def alice : Person := { name := "Alice", age := 30 }
7
8-- Create a new Person with updated age
9def olderAlice : Person := { alice with age := 31 }
10
11-- Original is unchanged
12#eval alice.age      -- 30
13#eval olderAlice.age -- 31

Accessor Functions

You can create small helper functions to keep structure access clean and reusable.

lean

1structure User where
2  name : String
3  score : Nat
4  deriving Repr
5
6def isTopUser (u : User) : Bool := u.score >= 100
7def displayName (u : User) : String := s!"@{u.name}"
8
9#eval isTopUser { name := "alice", score := 120 }  -- true
10#eval displayName { name := "bob", score := 10 }

Functions on Structures

Define functions that work with your structures:

lean

1structure Point where
2  x : Float
3  y : Float
4  deriving Repr
5
6def Point.distance (p1 p2 : Point) : Float :=
7  let dx := p2.x - p1.x
8  let dy := p2.y - p1.y
9  Float.sqrt (dx * dx + dy * dy)
10
11def origin : Point := ⟨0.0, 0.0⟩
12def p : Point := ⟨3.0, 4.0⟩
13
14#eval Point.distance origin p  -- 5.000000
15#eval origin.distance p        -- 5.000000 (method syntax!)

Notice the method syntax: origin.distance p. When a function is in the Point namespace and takes a Point as its first argument, you can call it with dot notation.

💡

Dot notation is smarter than "first argument": Lean uses the value as the first explicit argument whose type is Point, wherever it appears in the signature. So if you write def Point.scaleBy (k : Float) (p : Point) : Point, then p.scaleBy 2.0 still works — pslots into the Point position, not position one.

Field accessors are ordinary functions, which means you can pass them around:

lean

1#check Point.x            -- Point.x (self : Point) : Float
2
3-- So p.x is literally Point.x p, and the accessor composes like any function
4#eval [⟨1.0, 2.0⟩, ⟨3.0, 4.0⟩].map Point.x   -- [1.000000, 3.000000]

Nested Structures

Structures can contain other structures:

lean

1structure Address where
2  street : String
3  city : String
4  deriving Repr
5
6structure Person where
7  name : String
8  address : Address
9  deriving Repr
10
11def alice : Person := {
12  name := "Alice"
13  address := { street := "123 Main St", city := "Boston" }
14}
15
16#eval alice.address.city  -- "Boston"
17
18-- Nested update
19def movedAlice : Person := {
20  alice with
21  address := { alice.address with city := "Cambridge" }
22}

Structure Inheritance with extends

A structure can extendsone or more others. The parent's fields become part of the child, and — crucially — the child is usable wherever the parent is expected.

lean

1structure Animal where
2  name : String
3  deriving Repr
4
5structure Dog extends Animal where
6  breed : String
7  deriving Repr
8
9-- Construct it in one go: parent fields are just more fields
10def rex : Dog := { name := "Rex", breed := "Labrador" }
11
12#eval rex           -- { toAnimal := { name := "Rex" }, breed := "Labrador" }
13#eval rex.name      -- "Rex"       — parent fields are accessed directly
14#eval rex.toAnimal  -- { name := "Rex" }  — the parent value, if you need it
15
16-- A Dog can be used where an Animal is expected
17def describe (a : Animal) : String := s!"This is {a.name}"
18#eval describe rex.toAnimal   -- "This is Rex"

ℹ

Notice how Dog is actually represented: it has a single field toAnimal : Animal plus its own breed. Lean generates the flattened accessors (rex.name) on top of that. This is why the Repr output shows the nesting: inheritance here is composition with sugar, not a vtable.

lean

1-- Multiple inheritance is allowed, and shared parents are merged
2structure HasName where
3  name : String
4
5structure HasAge where
6  age : Nat
7
8structure Employee extends HasName, HasAge where
9  salary : Nat
10
11def e : Employee := { name := "Ada", age := 36, salary := 100 }
12#eval e.name ++ toString e.age   -- "Ada36"

Deep Dive: Structures vs Classes

Lean also has a class keyword. A class is a structure — the difference is that its values (instances) are found automatically by the elaborator rather than passed by hand. Use structure for data, and class for an interface you want Lean to resolve for you. Module 4 covers this.

What Lean does not have is dynamic dispatch: there is no runtime polymorphism where an Animal-typed value might secretly be a Dogand call an overridden method. If you need "one of several shapes", that is a sum type — the next lesson.

Exercise: Update a Record

Create a function that increments a person's age and returns the updated record.

lean

1structure Person where
2  name : String
3  age : Nat
4
5def birthday (p : Person) : Person :=
6  { p with age := p.age + 1 }
7
8#eval birthday { name := "Eve", age := 29 }

Pattern Matching on Structures

You can destructure structures in function parameters:

lean

1structure Point where
2  x : Float
3  y : Float
4
5-- Destructure in the parameter list
6def magnitude : Point → Float
7  | ⟨x, y⟩ => Float.sqrt (x * x + y * y)
8
9-- Or use a match expression
10def magnitude' (p : Point) : Float :=
11  match p with
12  | ⟨x, y⟩ => Float.sqrt (x * x + y * y)
13
14-- Or just use field access
15def magnitude'' (p : Point) : Float :=
16  Float.sqrt (p.x * p.x + p.y * p.y)
17
18#eval magnitude ⟨3.0, 4.0⟩  -- 5.0

Debugging & Troubleshooting Next: Inductive Types