Def Mathlib.Linter.Flexible.extractCtxAndGoals

Modification history

2025-12-17 02:05
Mathlib/Tactic/Linter/FlexibleLinter.lean
feat(Linter/FlexibleLinter): generate Try this: simp only suggestions (#32425) …
Deleted Mathlib.Linter.Flexible.extractCtxAndGoalsView on Github →
2024-09-05 20:53
Mathlib/Tactic/Linter/FlexibleLinter.lean
feat: flexible linter and tests (#11821) …
Added Mathlib.Linter.Flexible.extractCtxAndGoalsView on Github →