diff --git a/src/Lean/Linter.lean b/src/Lean/Linter.lean
index 9f6d3c4127d5..f3eed76302a2 100644
--- a/src/Lean/Linter.lean
+++ b/src/Lean/Linter.lean
@@ -8,6 +8,7 @@ import Lean.Linter.Util
 import Lean.Linter.Builtin
 import Lean.Linter.ConstructorAsVariable
 import Lean.Linter.Deprecated
+import Lean.Linter.Environment
 import Lean.Linter.UnusedVariables
 import Lean.Linter.MissingDocs
 import Lean.Linter.Omit
diff --git a/src/Lean/Linter/Environment.lean b/src/Lean/Linter/Environment.lean
new file mode 100644
index 000000000000..f3fe095e8e3c
--- /dev/null
+++ b/src/Lean/Linter/Environment.lean
@@ -0,0 +1 @@
+import Lean.Linter.Environment.Nolint
diff --git a/src/Lean/Linter/Environment/Nolint.lean b/src/Lean/Linter/Environment/Nolint.lean
new file mode 100644
index 000000000000..5025aa6d61dc
--- /dev/null
+++ b/src/Lean/Linter/Environment/Nolint.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
+-/
+prelude
+
+/-- `@[nolint linterName]` omits the tagged declaration from being checked by
+the linter with name `linterName`. -/
+syntax (name := nolint) "nolint" (ppSpace ident)+ : attr
+
+/-- Defines the user attribute `nolint` for skipping `#lint` -/
+initialize nolintAttr : ParametricAttribute (Array Name) ←
+  registerParametricAttribute {
+    name := `nolint
+    descr := "Do not report this declaration in any of the tests of `#lint`"
+    getParam := fun _ => fun
+      | `(attr| nolint $[$ids]*) => ids.mapM fun id => withRef id <| do
+        let shortName := id.getId.eraseMacroScopes
+        let some (declName, _) := (batteriesLinterExt.getState (← getEnv)).find? shortName
+          | throwError "linter '{shortName}' not found"
+        Elab.addConstInfo id declName
+        pure shortName
+      | _ => Elab.throwUnsupportedSyntax
+  }
+
+/-- Returns true if `decl` should be checked
+using `linter`, i.e., if there is no `nolint` attribute. -/
+def shouldBeLinted [Monad m] [MonadEnv m] (linter : Name) (decl : Name) : m Bool :=
+  return !((nolintAttr.getParam? (← getEnv) decl).getD #[]).contains linter