λleanlab

Programs

Structures

Group named fields into your own data type, then write a function that uses it.

Open Structures.lean in editor
structure Point where
  x : Int
  y : Int
  deriving Repr

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

def main : IO Unit := do
  let origin : Point := { x := 0, y := 0 }
  let moved := moveRight origin 5
  IO.println s!"Position: ({moved.x}, {moved.y})"

Explanation

structure

Defines a record with named fields. Point contains two integers.

Int

Integers include negative and positive whole numbers, as well as zero.

{ p with x := … }

Creates an updated copy of p while keeping its other fields.

Expected output

Reference only. Run the file to check its actual result.

Position: (5, 0)

Exercise

Add moveUp, then move the origin right 5 and up 3.