Def Mathlib.Linter.Flexible.toStained

Modification history

2025-12-05 11:03
Mathlib/Tactic/Linter/FlexibleLinter.lean
chore(Tactic/Linters): remove `public section` (#31803) …
Deleted Mathlib.Linter.Flexible.toStainedView on Github →
2024-09-05 20:53
Mathlib/Tactic/Linter/FlexibleLinter.lean
feat: flexible linter and tests (#11821) …
Added Mathlib.Linter.Flexible.toStainedView on Github →