Def introMerge

Modification history

2025-10-31 08:48
Mathlib/Tactic/TacticAnalysis/Declarations.lean
feat: tryAtEachStep linters run on a fraction of goals (#31039) …
Deleted introMergeView on Github →
2025-09-13 11:53
Mathlib/Tactic/TacticAnalysis/Declarations.lean
feat(TacticAnalysis): add a linter for merging consequent intro tactics (#28862) …
Added introMergeView on Github →