1// Lean compiler output
2// Module: Lean.Meta
3// Imports: Init Lean.Meta.Basic Lean.Meta.LevelDefEq Lean.Meta.WHNF Lean.Meta.InferType Lean.Meta.FunInfo Lean.Meta.ExprDefEq Lean.Meta.DecLevel Lean.Meta.DiscrTree Lean.Meta.Reduce Lean.Meta.Instances Lean.Meta.AbstractMVars Lean.Meta.SynthInstance Lean.Meta.AppBuilder Lean.Meta.Tactic Lean.Meta.KAbstract Lean.Meta.RecursorInfo Lean.Meta.GeneralizeTelescope Lean.Meta.Match Lean.Meta.ReduceEval Lean.Meta.Closure Lean.Meta.AbstractNestedProofs Lean.Meta.ForEachExpr Lean.Meta.Transform Lean.Meta.PPGoal Lean.Meta.UnificationHint Lean.Meta.Inductive Lean.Meta.SizeOf Lean.Meta.IndPredBelow Lean.Meta.Coe Lean.Meta.CollectFVars Lean.Meta.GeneralizeVars Lean.Meta.Injective Lean.Meta.Structure Lean.Meta.Constructions Lean.Meta.CongrTheorems Lean.Meta.Eqns Lean.Meta.CasesOn Lean.Meta.ExprLens Lean.Meta.ExprTraverse Lean.Meta.Eval
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_Meta_Basic(uint8_t builtin, lean_object*);
18lean_object* initialize_Lean_Meta_LevelDefEq(uint8_t builtin, lean_object*);
19lean_object* initialize_Lean_Meta_WHNF(uint8_t builtin, lean_object*);
20lean_object* initialize_Lean_Meta_InferType(uint8_t builtin, lean_object*);
21lean_object* initialize_Lean_Meta_FunInfo(uint8_t builtin, lean_object*);
22lean_object* initialize_Lean_Meta_ExprDefEq(uint8_t builtin, lean_object*);
23lean_object* initialize_Lean_Meta_DecLevel(uint8_t builtin, lean_object*);
24lean_object* initialize_Lean_Meta_DiscrTree(uint8_t builtin, lean_object*);
25lean_object* initialize_Lean_Meta_Reduce(uint8_t builtin, lean_object*);
26lean_object* initialize_Lean_Meta_Instances(uint8_t builtin, lean_object*);
27lean_object* initialize_Lean_Meta_AbstractMVars(uint8_t builtin, lean_object*);
28lean_object* initialize_Lean_Meta_SynthInstance(uint8_t builtin, lean_object*);
29lean_object* initialize_Lean_Meta_AppBuilder(uint8_t builtin, lean_object*);
30lean_object* initialize_Lean_Meta_Tactic(uint8_t builtin, lean_object*);
31lean_object* initialize_Lean_Meta_KAbstract(uint8_t builtin, lean_object*);
32lean_object* initialize_Lean_Meta_RecursorInfo(uint8_t builtin, lean_object*);
33lean_object* initialize_Lean_Meta_GeneralizeTelescope(uint8_t builtin, lean_object*);
34lean_object* initialize_Lean_Meta_Match(uint8_t builtin, lean_object*);
35lean_object* initialize_Lean_Meta_ReduceEval(uint8_t builtin, lean_object*);
36lean_object* initialize_Lean_Meta_Closure(uint8_t builtin, lean_object*);
37lean_object* initialize_Lean_Meta_AbstractNestedProofs(uint8_t builtin, lean_object*);
38lean_object* initialize_Lean_Meta_ForEachExpr(uint8_t builtin, lean_object*);
39lean_object* initialize_Lean_Meta_Transform(uint8_t builtin, lean_object*);
40lean_object* initialize_Lean_Meta_PPGoal(uint8_t builtin, lean_object*);
41lean_object* initialize_Lean_Meta_UnificationHint(uint8_t builtin, lean_object*);
42lean_object* initialize_Lean_Meta_Inductive(uint8_t builtin, lean_object*);
43lean_object* initialize_Lean_Meta_SizeOf(uint8_t builtin, lean_object*);
44lean_object* initialize_Lean_Meta_IndPredBelow(uint8_t builtin, lean_object*);
45lean_object* initialize_Lean_Meta_Coe(uint8_t builtin, lean_object*);
46lean_object* initialize_Lean_Meta_CollectFVars(uint8_t builtin, lean_object*);
47lean_object* initialize_Lean_Meta_GeneralizeVars(uint8_t builtin, lean_object*);
48lean_object* initialize_Lean_Meta_Injective(uint8_t builtin, lean_object*);
49lean_object* initialize_Lean_Meta_Structure(uint8_t builtin, lean_object*);
50lean_object* initialize_Lean_Meta_Constructions(uint8_t builtin, lean_object*);
51lean_object* initialize_Lean_Meta_CongrTheorems(uint8_t builtin, lean_object*);
52lean_object* initialize_Lean_Meta_Eqns(uint8_t builtin, lean_object*);
53lean_object* initialize_Lean_Meta_CasesOn(uint8_t builtin, lean_object*);
54lean_object* initialize_Lean_Meta_ExprLens(uint8_t builtin, lean_object*);
55lean_object* initialize_Lean_Meta_ExprTraverse(uint8_t builtin, lean_object*);
56lean_object* initialize_Lean_Meta_Eval(uint8_t builtin, lean_object*);
57static bool _G_initialized = false;
58LEAN_EXPORT lean_object* initialize_Lean_Meta(uint8_t builtin, lean_object* w) {
59lean_object * res;
60if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
61_G_initialized = true;
62res = initialize_Init(builtin, lean_io_mk_world());
63if (lean_io_result_is_error(res)) return res;
64lean_dec_ref(res);
65res = initialize_Lean_Meta_Basic(builtin, lean_io_mk_world());
66if (lean_io_result_is_error(res)) return res;
67lean_dec_ref(res);
68res = initialize_Lean_Meta_LevelDefEq(builtin, lean_io_mk_world());
69if (lean_io_result_is_error(res)) return res;
70lean_dec_ref(res);
71res = initialize_Lean_Meta_WHNF(builtin, lean_io_mk_world());
72if (lean_io_result_is_error(res)) return res;
73lean_dec_ref(res);
74res = initialize_Lean_Meta_InferType(builtin, lean_io_mk_world());
75if (lean_io_result_is_error(res)) return res;
76lean_dec_ref(res);
77res = initialize_Lean_Meta_FunInfo(builtin, lean_io_mk_world());
78if (lean_io_result_is_error(res)) return res;
79lean_dec_ref(res);
80res = initialize_Lean_Meta_ExprDefEq(builtin, lean_io_mk_world());
81if (lean_io_result_is_error(res)) return res;
82lean_dec_ref(res);
83res = initialize_Lean_Meta_DecLevel(builtin, lean_io_mk_world());
84if (lean_io_result_is_error(res)) return res;
85lean_dec_ref(res);
86res = initialize_Lean_Meta_DiscrTree(builtin, lean_io_mk_world());
87if (lean_io_result_is_error(res)) return res;
88lean_dec_ref(res);
89res = initialize_Lean_Meta_Reduce(builtin, lean_io_mk_world());
90if (lean_io_result_is_error(res)) return res;
91lean_dec_ref(res);
92res = initialize_Lean_Meta_Instances(builtin, lean_io_mk_world());
93if (lean_io_result_is_error(res)) return res;
94lean_dec_ref(res);
95res = initialize_Lean_Meta_AbstractMVars(builtin, lean_io_mk_world());
96if (lean_io_result_is_error(res)) return res;
97lean_dec_ref(res);
98res = initialize_Lean_Meta_SynthInstance(builtin, lean_io_mk_world());
99if (lean_io_result_is_error(res)) return res;
100lean_dec_ref(res);
101res = initialize_Lean_Meta_AppBuilder(builtin, lean_io_mk_world());
102if (lean_io_result_is_error(res)) return res;
103lean_dec_ref(res);
104res = initialize_Lean_Meta_Tactic(builtin, lean_io_mk_world());
105if (lean_io_result_is_error(res)) return res;
106lean_dec_ref(res);
107res = initialize_Lean_Meta_KAbstract(builtin, lean_io_mk_world());
108if (lean_io_result_is_error(res)) return res;
109lean_dec_ref(res);
110res = initialize_Lean_Meta_RecursorInfo(builtin, lean_io_mk_world());
111if (lean_io_result_is_error(res)) return res;
112lean_dec_ref(res);
113res = initialize_Lean_Meta_GeneralizeTelescope(builtin, lean_io_mk_world());
114if (lean_io_result_is_error(res)) return res;
115lean_dec_ref(res);
116res = initialize_Lean_Meta_Match(builtin, lean_io_mk_world());
117if (lean_io_result_is_error(res)) return res;
118lean_dec_ref(res);
119res = initialize_Lean_Meta_ReduceEval(builtin, lean_io_mk_world());
120if (lean_io_result_is_error(res)) return res;
121lean_dec_ref(res);
122res = initialize_Lean_Meta_Closure(builtin, lean_io_mk_world());
123if (lean_io_result_is_error(res)) return res;
124lean_dec_ref(res);
125res = initialize_Lean_Meta_AbstractNestedProofs(builtin, lean_io_mk_world());
126if (lean_io_result_is_error(res)) return res;
127lean_dec_ref(res);
128res = initialize_Lean_Meta_ForEachExpr(builtin, lean_io_mk_world());
129if (lean_io_result_is_error(res)) return res;
130lean_dec_ref(res);
131res = initialize_Lean_Meta_Transform(builtin, lean_io_mk_world());
132if (lean_io_result_is_error(res)) return res;
133lean_dec_ref(res);
134res = initialize_Lean_Meta_PPGoal(builtin, lean_io_mk_world());
135if (lean_io_result_is_error(res)) return res;
136lean_dec_ref(res);
137res = initialize_Lean_Meta_UnificationHint(builtin, lean_io_mk_world());
138if (lean_io_result_is_error(res)) return res;
139lean_dec_ref(res);
140res = initialize_Lean_Meta_Inductive(builtin, lean_io_mk_world());
141if (lean_io_result_is_error(res)) return res;
142lean_dec_ref(res);
143res = initialize_Lean_Meta_SizeOf(builtin, lean_io_mk_world());
144if (lean_io_result_is_error(res)) return res;
145lean_dec_ref(res);
146res = initialize_Lean_Meta_IndPredBelow(builtin, lean_io_mk_world());
147if (lean_io_result_is_error(res)) return res;
148lean_dec_ref(res);
149res = initialize_Lean_Meta_Coe(builtin, lean_io_mk_world());
150if (lean_io_result_is_error(res)) return res;
151lean_dec_ref(res);
152res = initialize_Lean_Meta_CollectFVars(builtin, lean_io_mk_world());
153if (lean_io_result_is_error(res)) return res;
154lean_dec_ref(res);
155res = initialize_Lean_Meta_GeneralizeVars(builtin, lean_io_mk_world());
156if (lean_io_result_is_error(res)) return res;
157lean_dec_ref(res);
158res = initialize_Lean_Meta_Injective(builtin, lean_io_mk_world());
159if (lean_io_result_is_error(res)) return res;
160lean_dec_ref(res);
161res = initialize_Lean_Meta_Structure(builtin, lean_io_mk_world());
162if (lean_io_result_is_error(res)) return res;
163lean_dec_ref(res);
164res = initialize_Lean_Meta_Constructions(builtin, lean_io_mk_world());
165if (lean_io_result_is_error(res)) return res;
166lean_dec_ref(res);
167res = initialize_Lean_Meta_CongrTheorems(builtin, lean_io_mk_world());
168if (lean_io_result_is_error(res)) return res;
169lean_dec_ref(res);
170res = initialize_Lean_Meta_Eqns(builtin, lean_io_mk_world());
171if (lean_io_result_is_error(res)) return res;
172lean_dec_ref(res);
173res = initialize_Lean_Meta_CasesOn(builtin, lean_io_mk_world());
174if (lean_io_result_is_error(res)) return res;
175lean_dec_ref(res);
176res = initialize_Lean_Meta_ExprLens(builtin, lean_io_mk_world());
177if (lean_io_result_is_error(res)) return res;
178lean_dec_ref(res);
179res = initialize_Lean_Meta_ExprTraverse(builtin, lean_io_mk_world());
180if (lean_io_result_is_error(res)) return res;
181lean_dec_ref(res);
182res = initialize_Lean_Meta_Eval(builtin, lean_io_mk_world());
183if (lean_io_result_is_error(res)) return res;
184lean_dec_ref(res);
185return lean_io_result_mk_ok(lean_box(0));
186}
187#ifdef __cplusplus
188}
189#endif
190