diff --git a/src/library/compiler/builtin.h b/src/library/compiler/builtin.h
new file mode 100644
index 0000000000..f063ab4545
--- /dev/null
+++ b/src/library/compiler/builtin.h
@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+namespace lean {
+void initialize_builtin();
+void finalize_builtin();
+}
diff --git a/src/library/compiler/init_module.cpp b/src/library/compiler/init_module.cpp
index b6d4b0d9b4..3619e36405 100644
--- a/src/library/compiler/init_module.cpp
+++ b/src/library/compiler/init_module.cpp
@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/compiler/closed_term_cache.h"
 #include "library/compiler/ir.h"
 #include "library/compiler/compiler.h"
+#include "library/compiler/builtin.h"
 
 namespace lean {
 void initialize_compiler_module() {
@@ -25,9 +26,11 @@ void initialize_compiler_module() {
     initialize_llnf();
     initialize_ir();
     initialize_compiler();
+    initialize_builtin();
 }
 
 void finalize_compiler_module() {
+    finalize_builtin();
     finalize_compiler();
     finalize_ir();
     finalize_llnf();