Def Mathlib.Linter.Flexible.extractTacticData

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.extractTacticData View on Github →