Show error in type even with parse error in proof

Stream: lean4

[Floris van Doorn]

If the type of a theorem has an elaboration error and the proof of the theorem has a parse error, the elaboration error is not shown. This often causes beginners to think that there is no error in the type of a theorem.

Example: in each of these theorems the type is nonsense and should show an error, but doesn't.

theorem foo1 : 3 4 := by
  simp [

theorem foo2 : 3 4 := by
  sim

theorem foo3 : 3 4 := by

theorem foo4 : 3 4 := by {

theorem foo5 : 3 4 := by
  constructor
  ·

[Floris van Doorn]

lean4#3556