diff --git a/library/init/lean/compiler/default.lean b/library/init/lean/compiler/default.lean
index 5b1732fe7f..2365a77636 100644
--- a/library/init/lean/compiler/default.lean
+++ b/library/init/lean/compiler/default.lean
@@ -10,4 +10,5 @@ import init.lean.compiler.constfolding
 import init.lean.compiler.closedtermcache
 import init.lean.compiler.externattr
 import init.lean.compiler.implementedbyattr
+import init.lean.compiler.effectfulattr
 import init.lean.compiler.ir
diff --git a/library/init/lean/compiler/effectfulattr.lean b/library/init/lean/compiler/effectfulattr.lean
new file mode 100644
index 0000000000..fd3206cd4d
--- /dev/null
+++ b/library/init/lean/compiler/effectfulattr.lean
@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.lean.environment
+import init.lean.attributes
+
+namespace Lean
+
+def mkEffectfulAttr : IO TagAttribute :=
+registerTagAttribute `effectful "mark that a declaration has implicit effects, and the compiler should avoid optimizations such as common subexpression elimination and closed term extraction"
+
+@[init mkEffectfulAttr]
+constant effectfulAttr : TagAttribute := default _
+
+@[export lean_has_effectful_attribute]
+def hasEffectfulAttribute (env : Environment) (n : Name) : Bool :=
+effectfulAttr.hasTag env n
+
+end Lean