Def Mathlib.Tactic.successIfFailWithMessage

Modification history

2025-01-09 10:38
Mathlib/Tactic/SuccessIfFailWithMsg.lean
feat: Add codeaction and widget to success_if_fail_with_msg tactic (#20378) …
Modified Mathlib.Tactic.successIfFailWithMessageView on Github →
2024-07-15 14:00
Mathlib/Tactic/SuccessIfFailWithMsg.lean
chore(Tactic): reduce use of Implicit, part 2 (#14726)
Modified Mathlib.Tactic.successIfFailWithMessageView on Github →
2023-03-16 04:34
Mathlib/Tactic/SuccessIfFailWithMsg.lean
feat: port `success_if_fail_with_msg` (#2204) …
Added Mathlib.Tactic.successIfFailWithMessageView on Github →