Programs

Pattern matching

Describe a small set of possibilities and handle each one explicitly.

inductive Light where
  | red
  | amber
  | green

def instruction (light : Light) : String :=
  match light with
  | .red => "Stop"
  | .amber => "Get ready"
  | .green => "Go"

def main : IO Unit := do
  IO.println (instruction .red)
  IO.println (instruction .green)

Explanation

`inductive`

Defines a new type by listing its constructors. Light has three possible values.

`match … with`

Inspects a value. Lean checks that the cases cover every possible constructor.

`.red`

Constructor shorthand. Lean infers the namespace Light from the expected type.

Expected output

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

Stop
Go

Exercise

Add a flashing constructor and update instruction to handle it.