elab12.lean:1:33: error: type expected at
  0
term has type
  ℕ
elab12.lean:1:41: error: function expected at
  rfl
term has type
  ?m_2 = ?m_2
Additional information:
elab12.lean:1:41: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  too many arguments
λ (a : ℕ), have H : ⁇, from ⁇, ⁇ : ∀ (a : ℕ), a = a
elab12.lean:4:45: error: function expected at
  rfl
term has type
  ?m_2 = ?m_2
Additional information:
elab12.lean:4:45: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  too many arguments
elab12.lean:5:2: error: function expected at
  H
term has type
  a = a
λ (a : ℕ), have H : a = a, from ⁇, ⁇ : ∀ (a : ℕ), a = a
elab12.lean:7:47: error: invalid have-expression, term
  a + 0
has type
  ℕ : Type
but is expected to have type
  a = a : Prop
elab12.lean:8:2: error: function expected at
  H
term has type
  a = a
λ (a : ℕ), have H : a = a, from ⁇, ⁇ : ∀ (a : ℕ), a = a
elab12.lean:11:2: error: function expected at
  H
term has type
  a = a
λ (a : ℕ), have H : a = a, from rfl, ⁇ : ∀ (a : ℕ), a = a
λ (a : ℕ), have H : a = a, from rfl, H : ∀ (a : ℕ), a = a
