Def Mathlib.Linter.mkWindow

Modification history

2025-12-05 11:03
Mathlib/Tactic/Linter/CommandStart.lean
chore(Tactic/Linters): remove `public section` (#31803) …
Deleted Mathlib.Linter.mkWindowView on Github →
2025-06-17 18:33
Mathlib/Tactic/Linter/CommandStart.lean
feat: a linter to enforce formatting (#24465) …
Added Mathlib.Linter.mkWindowView on Github →