Def Mathlib.Linter.mkFormatError

Modification history

2026-01-31 13:23
Mathlib/Tactic/Linter/Whitespace.lean
perf(Linter/Whitespace): revert #26240 (#34645) …
Modified Mathlib.Linter.mkFormatErrorView on Github →
2026-01-23 09:36
Mathlib/Tactic/Linter/Whitespace.lean
perf(Linter/Whitespace): use string slices more (#26240) …
Modified Mathlib.Linter.mkFormatErrorView on Github →
2025-06-17 18:33
Mathlib/Tactic/Linter/CommandStart.lean
feat: a linter to enforce formatting (#24465) …
Added Mathlib.Linter.mkFormatErrorView on Github →