Mathlib Changelog
v4
Changelog
About
Github
Def
Lean.MessageData.visitWithM
Modification history
2026-03-01 06:36
Mathlib/Tactic/DefEqAbuse.lean
feat(Tactic): add `#defeq_abuse` tactic combinator (#35750) …
Added
Lean.MessageData.visitWithM
View on Github →