diff --git a/library/init/lean/compiler/export.lean b/library/init/lean/compiler/export.lean
new file mode 100644
index 0000000000..2f0a1db317
--- /dev/null
+++ b/library/init/lean/compiler/export.lean
@@ -0,0 +1,12 @@
+/-
+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
+
+namespace Lean
+@[extern "lean_get_export_name_for"]
+constant getExportNameFor (env : @& Environment) (n : @& Name) : Option Name := default _
+end Lean
diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean
index 1a6ec0fedf..7635c5b29d 100644
--- a/library/init/lean/compiler/ir/emitcpp.lean
+++ b/library/init/lean/compiler/ir/emitcpp.lean
@@ -7,6 +7,7 @@ prelude
 import init.control.conditional
 import init.lean.runtime
 import init.lean.name_mangling
+import init.lean.compiler.export
 import init.lean.compiler.initattr
 import init.lean.compiler.ir.compilerm
 import init.lean.compiler.ir.emitutil
@@ -15,9 +16,6 @@ import init.lean.compiler.ir.simpcase
 
 namespace Lean
 namespace IR
-@[extern "lean_get_export_name_for"]
-constant getExportNameFor (env : @& Environment) (n : @& Name) : Option Name := default _
-
 namespace EmitCpp
 
 def leanMainFn := "_lean_main"