feat: recover as a tactic combinator

[siddhartha-gadgil]

trafficstars

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