From 5acdd68ad5492225d76443dcedd6df0316684dc6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 Nov 2018 13:29:57 -0800
Subject: [PATCH] feat(library/compiler/init_module): initialize `builtin`
 module

---
 src/library/compiler/builtin.h       | 11 +++++++++++
 src/library/compiler/init_module.cpp |  3 +++
 2 files changed, 14 insertions(+)
 create mode 100644 src/library/compiler/builtin.h

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();