Commit 2025-01-09 10:38 f3e168c0

feat: Add codeaction and widget to success_if_fail_with_msg tactic (#20378) make the success_if_fail_with_msg tactic give a codeaction when the tactics given fail with a different error, to update the expected error message. example:

example : Nat → Nat → True := by
  success_if_fail_with_msg "no goals" -- Update with tactic error message: "no goals to be solved"
    intro
    intro
    trivial
    trivial
  intros; trivial