Model data with a structure
Define named fields, construct records and update one field safely.
In this course 8 / 13
A structure groups values that belong together and gives each component a name. structure Point where creates a new type; the indented field declarations say that every Point contains an x coordinate and a y coordinate.
Construct a value with { x := 2, y := 5 }. Read a field with p.x. These names make the code explain itself and prevent the accidental coordinate swaps that are easy with an anonymous pair.
A record update starts from an existing value and replaces selected fields: { p with x := p.x + amount }. Every field not named in the update is copied from p, so y remains unchanged.
The read-only checks below your answer construct points, inspect fields and call your function. They test the public interface of the type you define, just as code elsewhere in a project would.
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 }).widthThe update changes width and copies height. Your exercise defines a different record and lets the caller choose the amount of movement.
Structures model one concept with named fields. Construct them with field assignments, read them with dot notation and update only what changes.
Define Point with natural-number fields x and y. Then define shiftX, which adds an amount to x while preserving y.
Suggested steps
- Declare
Pointwithxandyfields - Define
shiftXwith 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.
\to in the editor, or click: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 rflKnowledge check
Answer without looking back, then check your reasoning.
correct