明らかな場合はパターンマッチの枝が省略できるという例

[Seasawher]

def NonemptyList (α : Type) := { xs : List α // xs.length > 0}

def head {α : Type} (xs : NonemptyList α) : α :=
  match xs with
  -- パターンマッチが省略できる（Lean が賢いから）
  | ⟨x :: _xs, _⟩ => x