Def Mathlib.Linter.Style.header.headerLinter

Modification history

2024-10-16 03:00
Mathlib/Tactic/Linter/Header.lean
feat: the header linter (#16574) …
Added Mathlib.Linter.Style.header.headerLinterView on Github →