Similarly to how syntax linters in Lean core do it: https://github.com/leanprover/lean4/blob/206eb73cd9de4b58abbb2eae20a41fd9b7af187b/src/Lean/Linter/Basic.lean#L75
The relevant code seems to be at:
|
s := m!"-- Found {failed} error{if failed == 1 then "" else "s" |
cf. #FLT > unused argument linter issue @ 💬
(It might also be good for the documentation of environment linters to mention the term "environment linter" and disucss the distinction with "syntax linters" as well).
Similarly to how syntax linters in Lean core do it: https://github.com/leanprover/lean4/blob/206eb73cd9de4b58abbb2eae20a41fd9b7af187b/src/Lean/Linter/Basic.lean#L75
The relevant code seems to be at:
batteries/Batteries/Tactic/Lint/Frontend.lean
Line 194 in 6f7d05f
cf. #FLT > unused argument linter issue @ 💬
(It might also be good for the documentation of environment linters to mention the term "environment linter" and disucss the distinction with "syntax linters" as well).