Head.lean

def headOpt (xs : List α) : Option α :=
  match xs with
  | x :: _ => some x
  | [] => none -- need to introduce `Option` to handle the empty list case

def head (xs : List α) (h : xs ≠ []) : α :=
  match xs with
  | x :: _ => x
  -- no need to handle empty list case as it is impossible