Commit 2022-08-24 14:06 260313ce

feat: recover as a tactic combinator (#336) Following a suggestion of @digama0 recover is implemented as wrapping tactics so that if goals are closed incorrectly they are reopened. Below are examples (test suggested by @gebner). Some code is from Aesop.

/-- problematic tactic for testing recovery -/
elab "this" "is" "a" "problem" : tactic =>
  Lean.Elab.Tactic.setGoals []
/- The main test-/
example : 1 = 1 := by
  recover this is a problem
  rfl
/- Tests that recover does no harm -/
example : 3 < 4 := by
    recover decide
example : 1 = 1 := by
    recover skip ; rfl
example : 2 = 2 := by
    recover skip
    rfl