1// Lean compiler output
2// Module: Lean.Widget
3// Imports: Init Lean.Widget.InteractiveCode Lean.Widget.InteractiveDiagnostic Lean.Widget.InteractiveGoal Lean.Widget.TaggedText Lean.Widget.UserWidget
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
14extern "C" {
15#endif
16lean_object* initialize_Init(uint8_t builtin, lean_object*);
17lean_object* initialize_Lean_Widget_InteractiveCode(uint8_t builtin, lean_object*);
18lean_object* initialize_Lean_Widget_InteractiveDiagnostic(uint8_t builtin, lean_object*);
19lean_object* initialize_Lean_Widget_InteractiveGoal(uint8_t builtin, lean_object*);
20lean_object* initialize_Lean_Widget_TaggedText(uint8_t builtin, lean_object*);
21lean_object* initialize_Lean_Widget_UserWidget(uint8_t builtin, lean_object*);
22static bool _G_initialized = false;
23LEAN_EXPORT lean_object* initialize_Lean_Widget(uint8_t builtin, lean_object* w) {
24lean_object * res;
25if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
26_G_initialized = true;
27res = initialize_Init(builtin, lean_io_mk_world());
28if (lean_io_result_is_error(res)) return res;
29lean_dec_ref(res);
30res = initialize_Lean_Widget_InteractiveCode(builtin, lean_io_mk_world());
31if (lean_io_result_is_error(res)) return res;
32lean_dec_ref(res);
33res = initialize_Lean_Widget_InteractiveDiagnostic(builtin, lean_io_mk_world());
34if (lean_io_result_is_error(res)) return res;
35lean_dec_ref(res);
36res = initialize_Lean_Widget_InteractiveGoal(builtin, lean_io_mk_world());
37if (lean_io_result_is_error(res)) return res;
38lean_dec_ref(res);
39res = initialize_Lean_Widget_TaggedText(builtin, lean_io_mk_world());
40if (lean_io_result_is_error(res)) return res;
41lean_dec_ref(res);
42res = initialize_Lean_Widget_UserWidget(builtin, lean_io_mk_world());
43if (lean_io_result_is_error(res)) return res;
44lean_dec_ref(res);
45return lean_io_result_mk_ok(lean_box(0));
46}
47#ifdef __cplusplus
48}
49#endif
50