minimize_errors.lean:2:0: error: type mismatch, term
  λ (a : ℕ), a
has type
  ℕ → ℕ
but is expected to have type
  ℕ → ℕ → ℕ
f : ℕ → ℕ → ℕ
g : ℕ → ℕ → ℕ
def g : ℕ → ℕ → ℕ :=
f
def h : ℕ → ℕ → ℕ :=
h._main
