Group values in a structure

Named fields, building records, and updating one field.

14 minBeginnerstructurefieldsrecord update

0/11 completed in this course

In this course 8 / 11

Some values belong together: a point has an x and a y. A structure makes them one value with named parts:

structure Point where
  x : Nat
  y : Nat

#eval ({ x := 2, y := 5 } : Point).y

Lean replies

Build a value with { x := 2, y := 5 } and read a field with a dot: p.x. The names make the code say what it means, and Lean will not let you mix up an x and a y.

To change one field, copy the value and replace that field: { p with x := p.x + 1 }. Every field you do not mention is copied unchanged.

Worked example

structure Size where
  width : Nat
  height : Nat

def growWidth (s : Size) : Size :=
  { s with width := s.width + 1 }

#eval (growWidth { width := 3, height := 8 }).width   -- 4
#eval (growWidth { width := 3, height := 8 }).height  -- 8

The update changes width and keeps height. Your exercise does the same for a point, with the amount chosen by the caller.

Takeaway

A structure groups named fields into one value. Build it with { … }, read it with a dot, and update only what changes with with.

Exercise 1 of 3

Define Point with natural-number fields x and y. Then define shiftX (p : Point) (amount : Nat) : Point, which adds amount to x and keeps y.

Suggested steps

Declare Point with x and y fields
Define shiftX with a point and an amount
Use a record update that changes x

These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.

Exercise.lean

Loading editor…

These lines run underneath whatever you write. They are what decides the exercise, so your names and types have to match them.

example : Point.x { x := 2, y := 5 } = 2 := by rfl
example : shiftX { x := 2, y := 5 } 3 = { x := 5, y := 5 } := by rfl
example (p : Point) : (shiftX p 0).y = p.y := by rfl

ReadyLn 1, Col 1Lean 4

Draft saved in this browser

Stuck?

Worked example

Knowledge check