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.