max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/lean/default): missing file

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-14 15:21:53 -08:00
parent 390c9009f7
commit 6785ad9844
2 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/init/lean/default.lean
View file

@ -6,3 +6,4 @@ Authors: Leonardo de Moura
prelude
import init.lean.compiler
import init.lean.frontend
import init.lean.extern

8
src/boot/init/lean/default.cpp
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: init.lean.default
// Imports: init.lean.compiler.default init.lean.elaborator
// Imports: init.lean.compiler.default init.lean.frontend init.lean.extern
#include "runtime/object.h"
#include "runtime/apply.h"
typedef lean::object obj; typedef lean::usize usize;
@ -15,11 +15,13 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
void initialize_init_lean_compiler_default();
void initialize_init_lean_elaborator();
void initialize_init_lean_frontend();
void initialize_init_lean_extern();
static bool _G_initialized = false;
void initialize_init_lean_default() {
if (_G_initialized) return;
_G_initialized = true;
initialize_init_lean_compiler_default();
initialize_init_lean_elaborator();
initialize_init_lean_frontend();
initialize_init_lean_extern();
}