Structure Mathlib.Linter.Flexible.TacticData

Modification history

2025-12-17 02:05
Mathlib/Tactic/Linter/FlexibleLinter.lean
feat(Linter/FlexibleLinter): generate Try this: simp only suggestions (#32425) …
Added Mathlib.Linter.Flexible.TacticDataView on Github →