1// Lean compiler output
2// Module: Lean.Linter
3// Imports: Init Lean.Linter.Util Lean.Linter.Builtin Lean.Linter.Deprecated Lean.Linter.UnusedVariables Lean.Linter.MissingDocs
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_Linter_Util(uint8_t builtin, lean_object*);
18lean_object* initialize_Lean_Linter_Builtin(uint8_t builtin, lean_object*);
19lean_object* initialize_Lean_Linter_Deprecated(uint8_t builtin, lean_object*);
20lean_object* initialize_Lean_Linter_UnusedVariables(uint8_t builtin, lean_object*);
21lean_object* initialize_Lean_Linter_MissingDocs(uint8_t builtin, lean_object*);
22static bool _G_initialized = false;
23LEAN_EXPORT lean_object* initialize_Lean_Linter(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_Linter_Util(builtin, lean_io_mk_world());
31if (lean_io_result_is_error(res)) return res;
32lean_dec_ref(res);
33res = initialize_Lean_Linter_Builtin(builtin, lean_io_mk_world());
34if (lean_io_result_is_error(res)) return res;
35lean_dec_ref(res);
36res = initialize_Lean_Linter_Deprecated(builtin, lean_io_mk_world());
37if (lean_io_result_is_error(res)) return res;
38lean_dec_ref(res);
39res = initialize_Lean_Linter_UnusedVariables(builtin, lean_io_mk_world());
40if (lean_io_result_is_error(res)) return res;
41lean_dec_ref(res);
42res = initialize_Lean_Linter_MissingDocs(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