have tactic error recovery

Stream: lean4

[Floris van Doorn]

With the new have syntax, can we recover from errors more gracefully? That is: if the proof term contains an error then the tactic execution still continues with the new hypothesis added. Compare:

example : True := by
  have h : True :=
    False.elim -- expected error
  assumption -- bad error: no goals to be solved

example : True := by
  have h : True := by
    exact False.elim -- expected error
  assumption -- no error as expected

Note that to avoid this error I am switching from tactic mode to term mode to tactic mode to term mode. And these "no goals to be solved" errors can be really confusing to new users.

[Notification Bot]

A message was moved here from #lean4 > have syntax without ":= by" by Floris van Doorn.

[Eric Wieser]

This also applies to let, replace, obtain, etc

[Kyle Miller]

Here's a possible solution to this: lean4#3633

My interpretation of the underlying issue is that elabTermEnsuringType doesn't take errToSorry into account when it throws the type mismatch error. This PR makes it respect errToSorry, since it's a frontend to the main term elaborator.