1 | // Lean compiler output |
2 | // Module: Lake.Build |
3 | // Imports: Init Lake.Build.Monad Lake.Build.Actions Lake.Build.Index Lake.Build.Module Lake.Build.Package Lake.Build.Library Lake.Build.Imports |
4 | #include <lean/lean.h> |
5 | #if defined(__clang__) |
6 | #pragma clang diagnostic ignored "-Wunused-parameter" |
7 | #pragma clang diagnostic ignored "-Wunused-label" |
8 | #elif defined(__GNUC__) && !defined(__CLANG__) |
9 | #pragma GCC diagnostic ignored "-Wunused-parameter" |
10 | #pragma GCC diagnostic ignored "-Wunused-label" |
11 | #pragma GCC diagnostic ignored "-Wunused-but-set-variable" |
12 | #endif |
13 | #ifdef __cplusplus |
14 | extern "C" { |
15 | #endif |
16 | lean_object* initialize_Init(uint8_t builtin, lean_object*); |
17 | lean_object* initialize_Lake_Build_Monad(uint8_t builtin, lean_object*); |
18 | lean_object* initialize_Lake_Build_Actions(uint8_t builtin, lean_object*); |
19 | lean_object* initialize_Lake_Build_Index(uint8_t builtin, lean_object*); |
20 | lean_object* initialize_Lake_Build_Module(uint8_t builtin, lean_object*); |
21 | lean_object* initialize_Lake_Build_Package(uint8_t builtin, lean_object*); |
22 | lean_object* initialize_Lake_Build_Library(uint8_t builtin, lean_object*); |
23 | lean_object* initialize_Lake_Build_Imports(uint8_t builtin, lean_object*); |
24 | static bool _G_initialized = false; |
25 | LEAN_EXPORT lean_object* initialize_Lake_Build(uint8_t builtin, lean_object* w) { |
26 | lean_object * res; |
27 | if (_G_initialized) return lean_io_result_mk_ok(lean_box(0)); |
28 | _G_initialized = true; |
29 | res = initialize_Init(builtin, lean_io_mk_world()); |
30 | if (lean_io_result_is_error(res)) return res; |
31 | lean_dec_ref(res); |
32 | res = initialize_Lake_Build_Monad(builtin, lean_io_mk_world()); |
33 | if (lean_io_result_is_error(res)) return res; |
34 | lean_dec_ref(res); |
35 | res = initialize_Lake_Build_Actions(builtin, lean_io_mk_world()); |
36 | if (lean_io_result_is_error(res)) return res; |
37 | lean_dec_ref(res); |
38 | res = initialize_Lake_Build_Index(builtin, lean_io_mk_world()); |
39 | if (lean_io_result_is_error(res)) return res; |
40 | lean_dec_ref(res); |
41 | res = initialize_Lake_Build_Module(builtin, lean_io_mk_world()); |
42 | if (lean_io_result_is_error(res)) return res; |
43 | lean_dec_ref(res); |
44 | res = initialize_Lake_Build_Package(builtin, lean_io_mk_world()); |
45 | if (lean_io_result_is_error(res)) return res; |
46 | lean_dec_ref(res); |
47 | res = initialize_Lake_Build_Library(builtin, lean_io_mk_world()); |
48 | if (lean_io_result_is_error(res)) return res; |
49 | lean_dec_ref(res); |
50 | res = initialize_Lake_Build_Imports(builtin, lean_io_mk_world()); |
51 | if (lean_io_result_is_error(res)) return res; |
52 | lean_dec_ref(res); |
53 | return lean_io_result_mk_ok(lean_box(0)); |
54 | } |
55 | #ifdef __cplusplus |
56 | } |
57 | #endif |
58 | |