1 | // Lean compiler output |
---|---|
2 | // Module: Lake.Config |
3 | // Imports: Init Lake.Config.Monad |
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_Config_Monad(uint8_t builtin, lean_object*); |
18 | static bool _G_initialized = false; |
19 | LEAN_EXPORT lean_object* initialize_Lake_Config(uint8_t builtin, lean_object* w) { |
20 | lean_object * res; |
21 | if (_G_initialized) return lean_io_result_mk_ok(lean_box(0)); |
22 | _G_initialized = true; |
23 | res = initialize_Init(builtin, lean_io_mk_world()); |
24 | if (lean_io_result_is_error(res)) return res; |
25 | lean_dec_ref(res); |
26 | res = initialize_Lake_Config_Monad(builtin, lean_io_mk_world()); |
27 | if (lean_io_result_is_error(res)) return res; |
28 | lean_dec_ref(res); |
29 | return lean_io_result_mk_ok(lean_box(0)); |
30 | } |
31 | #ifdef __cplusplus |
32 | } |
33 | #endif |
34 |