Lean Class Notes

3. Structures🔗

3.1. Structures🔗

Structures package several fields into one new type.

structure Point where
  x : Float
  y : Float

def origin : Point :=
  { x := 0.4, y := 0.4 }

{ x := 0.400000, y := 0.400000 }#eval origin
0.400000#eval origin.x
0.400000#eval origin.y

def add_points (p1 : Point) (p2 : Point) : Point :=
  { x := p1.x + p2.x, y := p1.y + p2.y }

{ x := 4.000000, y := 5.000000 }#eval add_points {x := 1, y := 1} {x := 3, y := 4}

3.2. Exercises🔗

Define a structure Segment with endpoints a b : ℝ.
Write a function length : Segment → ℝ.
Define a function that adds two segments endpoint-wise.