Enums and pattern matching

Enums describe sum values: exactly one variant is present at a time. The enum definition is a proposition-level constraint, while its values are runtime data.

def Color : prop := enum
  | Red
  | Green
  | Blue

def describe (color : Color) : str :=
  match color with
  | Red => "red"
  | Green => "green"
  | Blue => "blue"

Variants may carry named payloads:

def Option (A : prop) : prop := enum
  | None
  | Some of (value : A)

def unwrap_or {A : prop} (option : Option A) (fallback : A) : A :=
  match option with
  | None => fallback
  | Some value => value

The compiler checks that a match is exhaustive. A final _ branch can cover the remaining variants:

def is_some {A : prop} (option : Option A) : bool :=
  match option with
  | Some _ => true
  | _ => false

Match branches refine the context with the selected constructor and bind payloads. This makes refinement information available while checking the branch body. The C backend lowers enums to a tagged representation and match expressions to branches over the tag.