Commit 2024-10-16 03:00 cd2b4684

feat: the header linter (#16574) This syntax linter checks that

• the copyright statement is correctly formatted;
• Mathlib.Tactic is not imported;
• makes sure that the module docs are the first non-import command of each file. The linter is off by default on projects downstream of mathlib, but it is on by default on mathlib. This subsumes the corresponding text-based linters. These will be removed in a future PR.