Defines the user attribute builtin_nolint for skipping environment linters.
def
Lean.Linter.EnvLinter.shouldBeLinted
{m : Type → Type}
[Monad m]
[MonadEnv m]
(linter decl : Name)
:
m Bool
Returns true if decl should be checked
using linter, i.e., if there is no builtin_nolint attribute.
Equations
- Lean.Linter.EnvLinter.shouldBeLinted linter decl = do let __do_lift ← Lean.getEnv pure !((Lean.Linter.EnvLinter.builtinNolintAttr.getParam? __do_lift decl).getD #[]).contains linter