1 | // Lean compiler output |
2 | // Module: Lean |
3 | // Imports: Init Lean.Data Lean.Compiler Lean.Environment Lean.Modifiers Lean.ProjFns Lean.Runtime Lean.ResolveName Lean.Attributes Lean.Parser Lean.ReducibilityAttrs Lean.Elab Lean.Class Lean.LocalContext Lean.MetavarContext Lean.AuxRecursor Lean.Meta Lean.Util Lean.Eval Lean.Structure Lean.PrettyPrinter Lean.CoreM Lean.InternalExceptionId Lean.Server Lean.ScopedEnvExtension Lean.DocString Lean.DeclarationRange Lean.LazyInitExtension Lean.LoadDynlib Lean.Widget Lean.Log Lean.Linter Lean.SubExpr |
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_Lean_Data(uint8_t builtin, lean_object*); |
18 | lean_object* initialize_Lean_Compiler(uint8_t builtin, lean_object*); |
19 | lean_object* initialize_Lean_Environment(uint8_t builtin, lean_object*); |
20 | lean_object* initialize_Lean_Modifiers(uint8_t builtin, lean_object*); |
21 | lean_object* initialize_Lean_ProjFns(uint8_t builtin, lean_object*); |
22 | lean_object* initialize_Lean_Runtime(uint8_t builtin, lean_object*); |
23 | lean_object* initialize_Lean_ResolveName(uint8_t builtin, lean_object*); |
24 | lean_object* initialize_Lean_Attributes(uint8_t builtin, lean_object*); |
25 | lean_object* initialize_Lean_Parser(uint8_t builtin, lean_object*); |
26 | lean_object* initialize_Lean_ReducibilityAttrs(uint8_t builtin, lean_object*); |
27 | lean_object* initialize_Lean_Elab(uint8_t builtin, lean_object*); |
28 | lean_object* initialize_Lean_Class(uint8_t builtin, lean_object*); |
29 | lean_object* initialize_Lean_LocalContext(uint8_t builtin, lean_object*); |
30 | lean_object* initialize_Lean_MetavarContext(uint8_t builtin, lean_object*); |
31 | lean_object* initialize_Lean_AuxRecursor(uint8_t builtin, lean_object*); |
32 | lean_object* initialize_Lean_Meta(uint8_t builtin, lean_object*); |
33 | lean_object* initialize_Lean_Util(uint8_t builtin, lean_object*); |
34 | lean_object* initialize_Lean_Eval(uint8_t builtin, lean_object*); |
35 | lean_object* initialize_Lean_Structure(uint8_t builtin, lean_object*); |
36 | lean_object* initialize_Lean_PrettyPrinter(uint8_t builtin, lean_object*); |
37 | lean_object* initialize_Lean_CoreM(uint8_t builtin, lean_object*); |
38 | lean_object* initialize_Lean_InternalExceptionId(uint8_t builtin, lean_object*); |
39 | lean_object* initialize_Lean_Server(uint8_t builtin, lean_object*); |
40 | lean_object* initialize_Lean_ScopedEnvExtension(uint8_t builtin, lean_object*); |
41 | lean_object* initialize_Lean_DocString(uint8_t builtin, lean_object*); |
42 | lean_object* initialize_Lean_DeclarationRange(uint8_t builtin, lean_object*); |
43 | lean_object* initialize_Lean_LazyInitExtension(uint8_t builtin, lean_object*); |
44 | lean_object* initialize_Lean_LoadDynlib(uint8_t builtin, lean_object*); |
45 | lean_object* initialize_Lean_Widget(uint8_t builtin, lean_object*); |
46 | lean_object* initialize_Lean_Log(uint8_t builtin, lean_object*); |
47 | lean_object* initialize_Lean_Linter(uint8_t builtin, lean_object*); |
48 | lean_object* initialize_Lean_SubExpr(uint8_t builtin, lean_object*); |
49 | static bool _G_initialized = false; |
50 | LEAN_EXPORT lean_object* initialize_Lean(uint8_t builtin, lean_object* w) { |
51 | lean_object * res; |
52 | if (_G_initialized) return lean_io_result_mk_ok(lean_box(0)); |
53 | _G_initialized = true; |
54 | res = initialize_Init(builtin, lean_io_mk_world()); |
55 | if (lean_io_result_is_error(res)) return res; |
56 | lean_dec_ref(res); |
57 | res = initialize_Lean_Data(builtin, lean_io_mk_world()); |
58 | if (lean_io_result_is_error(res)) return res; |
59 | lean_dec_ref(res); |
60 | res = initialize_Lean_Compiler(builtin, lean_io_mk_world()); |
61 | if (lean_io_result_is_error(res)) return res; |
62 | lean_dec_ref(res); |
63 | res = initialize_Lean_Environment(builtin, lean_io_mk_world()); |
64 | if (lean_io_result_is_error(res)) return res; |
65 | lean_dec_ref(res); |
66 | res = initialize_Lean_Modifiers(builtin, lean_io_mk_world()); |
67 | if (lean_io_result_is_error(res)) return res; |
68 | lean_dec_ref(res); |
69 | res = initialize_Lean_ProjFns(builtin, lean_io_mk_world()); |
70 | if (lean_io_result_is_error(res)) return res; |
71 | lean_dec_ref(res); |
72 | res = initialize_Lean_Runtime(builtin, lean_io_mk_world()); |
73 | if (lean_io_result_is_error(res)) return res; |
74 | lean_dec_ref(res); |
75 | res = initialize_Lean_ResolveName(builtin, lean_io_mk_world()); |
76 | if (lean_io_result_is_error(res)) return res; |
77 | lean_dec_ref(res); |
78 | res = initialize_Lean_Attributes(builtin, lean_io_mk_world()); |
79 | if (lean_io_result_is_error(res)) return res; |
80 | lean_dec_ref(res); |
81 | res = initialize_Lean_Parser(builtin, lean_io_mk_world()); |
82 | if (lean_io_result_is_error(res)) return res; |
83 | lean_dec_ref(res); |
84 | res = initialize_Lean_ReducibilityAttrs(builtin, lean_io_mk_world()); |
85 | if (lean_io_result_is_error(res)) return res; |
86 | lean_dec_ref(res); |
87 | res = initialize_Lean_Elab(builtin, lean_io_mk_world()); |
88 | if (lean_io_result_is_error(res)) return res; |
89 | lean_dec_ref(res); |
90 | res = initialize_Lean_Class(builtin, lean_io_mk_world()); |
91 | if (lean_io_result_is_error(res)) return res; |
92 | lean_dec_ref(res); |
93 | res = initialize_Lean_LocalContext(builtin, lean_io_mk_world()); |
94 | if (lean_io_result_is_error(res)) return res; |
95 | lean_dec_ref(res); |
96 | res = initialize_Lean_MetavarContext(builtin, lean_io_mk_world()); |
97 | if (lean_io_result_is_error(res)) return res; |
98 | lean_dec_ref(res); |
99 | res = initialize_Lean_AuxRecursor(builtin, lean_io_mk_world()); |
100 | if (lean_io_result_is_error(res)) return res; |
101 | lean_dec_ref(res); |
102 | res = initialize_Lean_Meta(builtin, lean_io_mk_world()); |
103 | if (lean_io_result_is_error(res)) return res; |
104 | lean_dec_ref(res); |
105 | res = initialize_Lean_Util(builtin, lean_io_mk_world()); |
106 | if (lean_io_result_is_error(res)) return res; |
107 | lean_dec_ref(res); |
108 | res = initialize_Lean_Eval(builtin, lean_io_mk_world()); |
109 | if (lean_io_result_is_error(res)) return res; |
110 | lean_dec_ref(res); |
111 | res = initialize_Lean_Structure(builtin, lean_io_mk_world()); |
112 | if (lean_io_result_is_error(res)) return res; |
113 | lean_dec_ref(res); |
114 | res = initialize_Lean_PrettyPrinter(builtin, lean_io_mk_world()); |
115 | if (lean_io_result_is_error(res)) return res; |
116 | lean_dec_ref(res); |
117 | res = initialize_Lean_CoreM(builtin, lean_io_mk_world()); |
118 | if (lean_io_result_is_error(res)) return res; |
119 | lean_dec_ref(res); |
120 | res = initialize_Lean_InternalExceptionId(builtin, lean_io_mk_world()); |
121 | if (lean_io_result_is_error(res)) return res; |
122 | lean_dec_ref(res); |
123 | res = initialize_Lean_Server(builtin, lean_io_mk_world()); |
124 | if (lean_io_result_is_error(res)) return res; |
125 | lean_dec_ref(res); |
126 | res = initialize_Lean_ScopedEnvExtension(builtin, lean_io_mk_world()); |
127 | if (lean_io_result_is_error(res)) return res; |
128 | lean_dec_ref(res); |
129 | res = initialize_Lean_DocString(builtin, lean_io_mk_world()); |
130 | if (lean_io_result_is_error(res)) return res; |
131 | lean_dec_ref(res); |
132 | res = initialize_Lean_DeclarationRange(builtin, lean_io_mk_world()); |
133 | if (lean_io_result_is_error(res)) return res; |
134 | lean_dec_ref(res); |
135 | res = initialize_Lean_LazyInitExtension(builtin, lean_io_mk_world()); |
136 | if (lean_io_result_is_error(res)) return res; |
137 | lean_dec_ref(res); |
138 | res = initialize_Lean_LoadDynlib(builtin, lean_io_mk_world()); |
139 | if (lean_io_result_is_error(res)) return res; |
140 | lean_dec_ref(res); |
141 | res = initialize_Lean_Widget(builtin, lean_io_mk_world()); |
142 | if (lean_io_result_is_error(res)) return res; |
143 | lean_dec_ref(res); |
144 | res = initialize_Lean_Log(builtin, lean_io_mk_world()); |
145 | if (lean_io_result_is_error(res)) return res; |
146 | lean_dec_ref(res); |
147 | res = initialize_Lean_Linter(builtin, lean_io_mk_world()); |
148 | if (lean_io_result_is_error(res)) return res; |
149 | lean_dec_ref(res); |
150 | res = initialize_Lean_SubExpr(builtin, lean_io_mk_world()); |
151 | if (lean_io_result_is_error(res)) return res; |
152 | lean_dec_ref(res); |
153 | return lean_io_result_mk_ok(lean_box(0)); |
154 | } |
155 | #ifdef __cplusplus |
156 | } |
157 | #endif |
158 | |