Def Mathlib.Linter.HashCommandLinter.hashCommandLinter

Modification history

2024-05-24 03:47

Mathlib/Tactic/Linter/HashCommandLinter.lean

feat: syntax linter for `#`-commands (#11019) …

Added Mathlib.Linter.HashCommandLinter.hashCommandLinter View on Github →