// Lean compiler output // Module: module // Imports: public import Init public meta import Lean #include #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" #pragma clang diagnostic ignored "-Wunused-label" #elif defined(__GNUC__) && !defined(__CLANG__) #pragma GCC diagnostic ignored "-Wunused-parameter" #pragma GCC diagnostic ignored "-Wunused-label" #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif #ifdef __cplusplus extern "C" { #endif static lean_object* l_termMk__str___closed__0; static lean_object* l_termMk__str___closed__4; static lean_object* l_termMk__str___closed__2; static lean_object* l___aux__module______elabRules__termMk__str__1___redArg___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg(); static lean_object* l_termMk__str___closed__3; uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*); static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__0; lean_object* l_Lean_mkStrLit(lean_object*); static lean_object* l_termMk__str___closed__1; LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1___redArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_termMk__str; LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___boxed(lean_object*); static lean_object* l___aux__module______elabRules__termMk__str__1___redArg___closed__0; static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__1; LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Name_mkStr1(lean_object*); extern lean_object* l_Lean_Elab_unsupportedSyntaxExceptionId; static lean_object* _init_l_termMk__str___closed__0() { _start: { lean_object* x_1; x_1 = lean_mk_string_unchecked("termMk_str", 10, 10); return x_1; } } static lean_object* _init_l_termMk__str___closed__1() { _start: { lean_object* x_1; lean_object* x_2; x_1 = l_termMk__str___closed__0; x_2 = l_Lean_Name_mkStr1(x_1); return x_2; } } static lean_object* _init_l_termMk__str___closed__2() { _start: { lean_object* x_1; x_1 = lean_mk_string_unchecked("mk_str", 6, 6); return x_1; } } static lean_object* _init_l_termMk__str___closed__3() { _start: { lean_object* x_1; lean_object* x_2; x_1 = l_termMk__str___closed__2; x_2 = lean_alloc_ctor(5, 1, 0); lean_ctor_set(x_2, 0, x_1); return x_2; } } static lean_object* _init_l_termMk__str___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_termMk__str___closed__3; x_2 = lean_unsigned_to_nat(1024u); x_3 = l_termMk__str___closed__1; x_4 = lean_alloc_ctor(3, 3, 0); lean_ctor_set(x_4, 0, x_3); lean_ctor_set(x_4, 1, x_2); lean_ctor_set(x_4, 2, x_1); return x_4; } } static lean_object* _init_l_termMk__str() { _start: { lean_object* x_1; x_1 = l_termMk__str___closed__4; return x_1; } } static lean_object* _init_l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__0() { _start: { lean_object* x_1; x_1 = l_Lean_Elab_unsupportedSyntaxExceptionId; return x_1; } } static lean_object* _init_l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); x_2 = l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__0; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); return x_3; } } LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg() { _start: { lean_object* x_2; lean_object* x_3; x_2 = l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__1; x_3 = lean_alloc_ctor(1, 1, 0); lean_ctor_set(x_3, 0, x_2); return x_3; } } LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { _start: { lean_object* x_9; x_9 = l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg(); return x_9; } } static lean_object* _init_l___aux__module______elabRules__termMk__str__1___redArg___closed__0() { _start: { lean_object* x_1; x_1 = lean_mk_string_unchecked("elab'd", 6, 6); return x_1; } } static lean_object* _init_l___aux__module______elabRules__termMk__str__1___redArg___closed__1() { _start: { lean_object* x_1; lean_object* x_2; x_1 = l___aux__module______elabRules__termMk__str__1___redArg___closed__0; x_2 = l_Lean_mkStrLit(x_1); return x_2; } } LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1___redArg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { _start: { lean_object* x_9; uint8_t x_10; x_9 = l_termMk__str___closed__1; x_10 = l_Lean_Syntax_isOfKind(x_1, x_9); if (x_10 == 0) { lean_object* x_11; x_11 = l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg(); return x_11; } else { lean_object* x_12; lean_object* x_13; x_12 = l___aux__module______elabRules__termMk__str__1___redArg___closed__1; x_13 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_13, 0, x_12); return x_13; } } } LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { _start: { lean_object* x_10; x_10 = l___aux__module______elabRules__termMk__str__1___redArg(x_1, x_3, x_4, x_5, x_6, x_7, x_8); return x_10; } } LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { _start: { lean_object* x_9; x_9 = l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0(x_1, x_2, x_3, x_4, x_5, x_6, x_7); lean_dec(x_7); lean_dec_ref(x_6); lean_dec(x_5); lean_dec_ref(x_4); lean_dec(x_3); lean_dec_ref(x_2); return x_9; } } LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) { _start: { lean_object* x_10; x_10 = l___aux__module______elabRules__termMk__str__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); lean_dec(x_8); lean_dec_ref(x_7); lean_dec(x_6); lean_dec_ref(x_5); lean_dec(x_4); lean_dec_ref(x_3); lean_dec(x_2); return x_10; } } LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___boxed(lean_object* x_1) { _start: { lean_object* x_2; x_2 = l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg(); return x_2; } } LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1___redArg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { _start: { lean_object* x_9; x_9 = l___aux__module______elabRules__termMk__str__1___redArg(x_1, x_2, x_3, x_4, x_5, x_6, x_7); lean_dec(x_7); lean_dec_ref(x_6); lean_dec(x_5); lean_dec_ref(x_4); lean_dec(x_3); lean_dec_ref(x_2); return x_9; } } lean_object* meta_initialize_Init(uint8_t builtin); lean_object* meta_initialize_Lean(uint8_t builtin); static bool _G_initialized = false; LEAN_EXPORT lean_object* initialize_module(uint8_t builtin) { lean_object * res; if (_G_initialized) return lean_io_result_mk_ok(lean_box(0)); _G_initialized = true; res = meta_initialize_Init(builtin); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); res = meta_initialize_Lean(builtin); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l_termMk__str___closed__0 = _init_l_termMk__str___closed__0(); lean_mark_persistent(l_termMk__str___closed__0); l_termMk__str___closed__1 = _init_l_termMk__str___closed__1(); lean_mark_persistent(l_termMk__str___closed__1); l_termMk__str___closed__2 = _init_l_termMk__str___closed__2(); lean_mark_persistent(l_termMk__str___closed__2); l_termMk__str___closed__3 = _init_l_termMk__str___closed__3(); lean_mark_persistent(l_termMk__str___closed__3); l_termMk__str___closed__4 = _init_l_termMk__str___closed__4(); lean_mark_persistent(l_termMk__str___closed__4); l_termMk__str = _init_l_termMk__str(); lean_mark_persistent(l_termMk__str); l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__0 = _init_l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__0(); lean_mark_persistent(l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__0); l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__1 = _init_l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__1(); lean_mark_persistent(l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__1); l___aux__module______elabRules__termMk__str__1___redArg___closed__0 = _init_l___aux__module______elabRules__termMk__str__1___redArg___closed__0(); lean_mark_persistent(l___aux__module______elabRules__termMk__str__1___redArg___closed__0); l___aux__module______elabRules__termMk__str__1___redArg___closed__1 = _init_l___aux__module______elabRules__termMk__str__1___redArg___closed__1(); lean_mark_persistent(l___aux__module______elabRules__termMk__str__1___redArg___closed__1); return lean_io_result_mk_ok(lean_box(0)); } #ifdef __cplusplus } #endif