Def Mathlib.Linter.Style.Header.formatImports

Modification history

2026-10-20 19:29
Mathlib/Tactic/Linter/Header.lean
feat(Tactic/Linter/Header): suggest formatting imports according to the style convention (#44507) …
Added Mathlib.Linter.Style.Header.formatImportsView on Github →