feat(library/compiler/init_module): initialize builtin module
This commit is contained in:
parent
b501613f8c
commit
5acdd68ad5
2 changed files with 14 additions and 0 deletions
11
src/library/compiler/builtin.h
Normal file
11
src/library/compiler/builtin.h
Normal file
|
|
@ -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();
|
||||
}
|
||||
|
|
@ -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();
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue