max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Lean stage0 autoupdater 2026-03-20 16:28:23 +00:00
parent 6f98a76d01
commit 4d6accd55d
36 changed files with 96142 additions and 91959 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/include/lean/lean.h generated
View file

@ -3245,6 +3245,8 @@ static inline double lean_float_once(double* loc, lean_once_cell_t* tok, double
return lean_float_once_cold(loc, tok, init);
}
LEAN_EXPORT lean_object * lean_run_main(lean_object * (*main_fn)(int, char **), int argc, char ** argv);
#ifdef __cplusplus
}
#endif

4
stage0/src/library/ir_interpreter.cpp generated
View file

@ -1177,8 +1177,8 @@ uint32 run_main(elab_environment const & env, options const & opts, list_ref<str
return interpreter::with_interpreter<uint32>(env, opts, "main", [&](interpreter & interp) { return interp.run_main(args); });
}
/* runMain (env : Environment) (opts : Iptions) (args : List String) : BaseIO UInt32 */
extern "C" LEAN_EXPORT uint32_t lean_run_main(b_obj_arg env, b_obj_arg opts, b_obj_arg args) {
/* runMain (env : Environment) (opts : Options) (args : List String) : BaseIO UInt32 */
extern "C" LEAN_EXPORT uint32_t lean_eval_main(b_obj_arg env, b_obj_arg opts, b_obj_arg args) {
uint32 ret = run_main(TO_REF(elab_environment, env), TO_REF(options, opts), TO_REF(list_ref<string_ref>, args));
return ret;
}

35
stage0/src/runtime/thread.cpp generated
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include <utility>
#include <vector>
#include <iostream>
#include <cstring>
#ifdef LEAN_WINDOWS
#include <windows.h>
#else
@ -20,7 +21,11 @@ Author: Leonardo de Moura
#include "runtime/stack_overflow.h"
#ifndef LEAN_DEFAULT_THREAD_STACK_SIZE
#define LEAN_DEFAULT_THREAD_STACK_SIZE 8*1024*1024 // 8Mb
#ifdef LEAN_EMSCRIPTEN
#define LEAN_DEFAULT_THREAD_STACK_SIZE 8*1024*1024 // 8MB for 32-bit
#else
#define LEAN_DEFAULT_THREAD_STACK_SIZE 1024*1024*1024 // 1GB for 64-bit
#endif
#endif
namespace lean {
@ -96,8 +101,10 @@ struct lthread::imp {
imp(runnable const & p) {
runnable * f = new std::function<void()>(mk_thread_proc(p, get_max_heartbeat()));
// Without `IS_A_RESERVATION`, `m_thread_stack_size` would be the initial *commit* size,
// quickly exhausting the available address space with our large default stack size.
m_thread = CreateThread(nullptr, m_thread_stack_size,
_main, f, 0, nullptr);
_main, f, STACK_SIZE_PARAM_IS_A_RESERVATION, nullptr);
if (m_thread == NULL) {
throw exception("failed to create thread");
}
@ -163,6 +170,30 @@ extern "C" LEAN_EXPORT lean_obj_res lean_internal_set_thread_stack_size(size_t s
return lean_box(0);
}
extern "C" LEAN_EXPORT lean_object * lean_run_main(lean_object * (*main_fn)(int, char **), int argc, char ** argv) {
#ifdef LEAN_MULTI_THREAD
const char * stack_size_env = std::getenv("LEAN_STACK_SIZE_KB");
if (stack_size_env) {
size_t sz = std::strtoull(stack_size_env, nullptr, 10);
sz = sz / 4 * 4 * 1024; // as in `Shell`
if (sz > 0) {
lthread::set_thread_stack_size(sz);
}
}
const char * use_thread_env = std::getenv("LEAN_MAIN_USE_THREAD");
if (use_thread_env && std::strcmp(use_thread_env, "0") == 0) {
return main_fn(argc, argv);
}
// Start new thread to use given/default stack size
lean_object * res = nullptr;
lthread t([&]() { res = main_fn(argc, argv); });
t.join();
return res;
#else
return main_fn(argc, argv);
#endif
}
LEAN_THREAD_VALUE(bool, g_finalizing, false);
bool in_thread_finalization() {

10
stage0/stdlib/Lake/Build/Trace.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lake.Build.Trace
// Imports: public import Lean.Data.Json import Init.Data.Nat.Fold import Lake.Util.String public import Init.Data.String.Search public import Init.Data.String.Extra import Init.Data.Option.Coe
// Imports: public import Lean.Data.Json import Init.Data.Nat.Fold meta import Init.Data.Nat.Fold import Lake.Util.String public import Init.Data.String.Search public import Init.Data.String.Extra import Init.Data.Option.Coe
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -3753,15 +3753,20 @@ l_Lake_BuildTrace_instNilTrace = _init_l_Lake_BuildTrace_instNilTrace();
lean_mark_persistent(l_Lake_BuildTrace_instNilTrace);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* runtime_initialize_Init_Data_Nat_Fold(uint8_t builtin);
static bool _G_meta_initialized = false;
LEAN_EXPORT lean_object* meta_initialize_Lake_Build_Trace(uint8_t builtin) {
lean_object * res;
if (_G_meta_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_meta_initialized = true;
res = runtime_initialize_Init_Data_Nat_Fold(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* initialize_Lean_Data_Json(uint8_t builtin);
lean_object* initialize_Init_Data_Nat_Fold(uint8_t builtin);
lean_object* initialize_Init_Data_Nat_Fold(uint8_t builtin);
lean_object* initialize_Lake_Util_String(uint8_t builtin);
lean_object* initialize_Init_Data_String_Search(uint8_t builtin);
lean_object* initialize_Init_Data_String_Extra(uint8_t builtin);
@ -3777,6 +3782,9 @@ lean_dec_ref(res);
res = initialize_Init_Data_Nat_Fold(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Nat_Fold(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lake_Util_String(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

3
stage0/stdlib/Lean/Compiler/LCNF/Bind.c generated
View file

@ -41,6 +41,7 @@ lean_object* l_Lean_mkFVar(lean_object*);
lean_object* l_Lean_Compiler_LCNF_instantiateForall(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* lean_expr_instantiate_rev(lean_object*, lean_object*);
uint8_t l_Lean_isMarkedBorrowed(lean_object*);
lean_object* l_Lean_Expr_fvar___override(lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* l_Lean_Expr_headBeta(lean_object*);
@ -3167,7 +3168,7 @@ lean_inc_ref(v_body_764_);
lean_dec_ref(v_type_755_);
v_d_765_ = lean_expr_instantiate_rev(v_binderType_763_, v_xs_756_);
lean_dec_ref(v_binderType_763_);
v___x_766_ = 0;
v___x_766_ = l_Lean_isMarkedBorrowed(v_d_765_);
v___x_767_ = l_Lean_Compiler_LCNF_mkAuxParam(v_pu_754_, v_d_765_, v___x_766_, v_a_758_, v_a_759_, v_a_760_, v_a_761_);
if (lean_obj_tag(v___x_767_) == 0)
{

2838
stage0/stdlib/Lean/Compiler/LCNF/EmitC.c generated
View file

File diff suppressed because it is too large Load diff

20933
stage0/stdlib/Lean/Compiler/LCNF/InferBorrow.c generated
View file

File diff suppressed because it is too large Load diff

5
stage0/stdlib/Lean/Compiler/LCNF/ToDecl.c generated
View file

@ -127,7 +127,7 @@ lean_object* l_Lean_ConstantInfo_type(lean_object*);
lean_object* l_Lean_Compiler_LCNF_toLCNFType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_hasInitAttr(lean_object*, lean_object*);
lean_object* l_Lean_ConstantInfo_value_x3f(lean_object*, uint8_t);
lean_object* l_Lean_Compiler_LCNF_ToLCNF_toLCNF(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_LCNF_ToLCNF_toLCNF(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_LCNF_eraseFunDecl___redArg(uint8_t, lean_object*, uint8_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_macroInline___lam__0(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_macroInline___lam__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -11252,7 +11252,8 @@ lean_inc(v_a_3780_);
lean_inc_ref(v_a_3779_);
lean_inc(v_a_3778_);
lean_inc_ref(v_a_3777_);
v___x_3972_ = l_Lean_Compiler_LCNF_ToLCNF_toLCNF(v_a_3970_, v_a_3777_, v_a_3778_, v_a_3779_, v_a_3780_);
lean_inc(v_a_3957_);
v___x_3972_ = l_Lean_Compiler_LCNF_ToLCNF_toLCNF(v_a_3970_, v_a_3957_, v_a_3777_, v_a_3778_, v_a_3779_, v_a_3780_);
if (lean_obj_tag(v___x_3972_) == 0)
{
lean_object* v_a_3973_;

31388
stage0/stdlib/Lean/Compiler/LCNF/ToLCNF.c generated
View file

File diff suppressed because it is too large Load diff

1251
stage0/stdlib/Lean/Compiler/MetaAttr.c generated
View file

File diff suppressed because it is too large Load diff

10
stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Data.Lsp.LanguageFeatures
// Imports: public import Lean.Data.Lsp.Basic public import Lean.Expr public import Init.Data.String.Search public import Init.Data.Array.GetLit
// Imports: public import Lean.Data.Lsp.Basic public import Lean.Expr public import Init.Data.String.Search public import Init.Data.Array.GetLit meta import Lean.Data.Json.FromToJson.Basic
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -53269,17 +53269,22 @@ l_Lean_Lsp_instInhabitedCallHierarchyOutgoingCall = _init_l_Lean_Lsp_instInhabit
lean_mark_persistent(l_Lean_Lsp_instInhabitedCallHierarchyOutgoingCall);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* runtime_initialize_Lean_Data_Json_FromToJson_Basic(uint8_t builtin);
static bool _G_meta_initialized = false;
LEAN_EXPORT lean_object* meta_initialize_Lean_Data_Lsp_LanguageFeatures(uint8_t builtin) {
lean_object * res;
if (_G_meta_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_meta_initialized = true;
res = runtime_initialize_Lean_Data_Json_FromToJson_Basic(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* initialize_Lean_Data_Lsp_Basic(uint8_t builtin);
lean_object* initialize_Lean_Expr(uint8_t builtin);
lean_object* initialize_Init_Data_String_Search(uint8_t builtin);
lean_object* initialize_Init_Data_Array_GetLit(uint8_t builtin);
lean_object* initialize_Lean_Data_Json_FromToJson_Basic(uint8_t builtin);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Data_Lsp_LanguageFeatures(uint8_t builtin) {
lean_object * res;
@ -53297,6 +53302,9 @@ lean_dec_ref(res);
res = initialize_Init_Data_Array_GetLit(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Data_Json_FromToJson_Basic(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_Data_Lsp_LanguageFeatures(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

2421
stage0/stdlib/Lean/Elab/BuiltinNotation.c generated
View file

File diff suppressed because it is too large Load diff

704
stage0/stdlib/Lean/Elab/BuiltinTerm.c generated
View file

@ -230,9 +230,11 @@ lean_object* l_Array_zip___redArg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArgs(lean_object*);
lean_object* l_Lean_Elab_Term_mkNoImplicitLambdaAnnotation(lean_object*);
lean_object* l_Lean_Level_succ___override(lean_object*);
lean_object* l_Lean_compileDecls(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTermAndSynthesize(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkAuxDefinitionFor(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_setInlineAttribute(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_markMeta(lean_object*, lean_object*);
extern lean_object* l_Lean_noncomputableExt;
uint8_t l_Lean_isNoncomputable(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_DataValue_sameCtor(lean_object*, lean_object*);
@ -2331,8 +2333,8 @@ LEAN_EXPORT lean_object* l_Lean_mkAuxDeclName___at___00Lean_Elab_Term_elabPrivat
LEAN_EXPORT lean_object* l_Lean_mkAuxDeclName___at___00Lean_Elab_Term_elabPrivateDecl_spec__0___redArg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkAuxDeclName___at___00Lean_Elab_Term_elabPrivateDecl_spec__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkAuxDeclName___at___00Lean_Elab_Term_elabPrivateDecl_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_Term_elabPrivateDecl___lam__0(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl___lam__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl___lam__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static const lean_string_object l_Lean_Elab_Term_elabPrivateDecl___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 12, .m_capacity = 12, .m_length = 11, .m_data = "privateDecl"};
static const lean_object* l_Lean_Elab_Term_elabPrivateDecl___closed__0 = (const lean_object*)&l_Lean_Elab_Term_elabPrivateDecl___closed__0_value;
static const lean_ctor_object l_Lean_Elab_Term_elabPrivateDecl___closed__1_value_aux_0 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)(((size_t)(0) << 1) | 1)),((lean_object*)&l_Lean_Elab_Term_elabProp___regBuiltin_Lean_Elab_Term_elabProp__1___closed__0_value),LEAN_SCALAR_PTR_LITERAL(70, 193, 83, 126, 233, 67, 208, 165)}};
@ -30113,311 +30115,533 @@ lean_dec_ref(v___y_11642_);
return v_res_11649_;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl___lam__0(lean_object* v___x_11650_, lean_object* v_expectedType_x3f_11651_, lean_object* v_a_11652_, uint8_t v_isExporting_11653_, lean_object* v___y_11654_, lean_object* v___y_11655_, lean_object* v___y_11656_, lean_object* v___y_11657_, lean_object* v___y_11658_, lean_object* v___y_11659_){
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl___lam__0(lean_object* v___x_11650_, lean_object* v_expectedType_x3f_11651_, lean_object* v___x_11652_, lean_object* v_a_11653_, uint8_t v___x_11654_, uint8_t v_isExporting_11655_, lean_object* v___y_11656_, lean_object* v___y_11657_, lean_object* v___y_11658_, lean_object* v___y_11659_, lean_object* v___y_11660_, lean_object* v___y_11661_){
_start:
{
lean_object* v___x_11661_;
lean_object* v___y_11664_; lean_object* v___y_11665_; lean_object* v___y_11666_; lean_object* v___x_11686_;
lean_inc(v___y_11661_);
lean_inc_ref(v___y_11660_);
lean_inc(v___y_11659_);
lean_inc_ref(v___y_11658_);
lean_inc(v___y_11657_);
lean_inc_ref(v___y_11656_);
lean_inc_ref(v___y_11654_);
v___x_11661_ = l_Lean_Elab_Term_elabTermAndSynthesize(v___x_11650_, v_expectedType_x3f_11651_, v___y_11654_, v___y_11655_, v___y_11656_, v___y_11657_, v___y_11658_, v___y_11659_);
if (lean_obj_tag(v___x_11661_) == 0)
v___x_11686_ = l_Lean_Elab_Term_elabTermAndSynthesize(v___x_11650_, v_expectedType_x3f_11651_, v___y_11656_, v___y_11657_, v___y_11658_, v___y_11659_, v___y_11660_, v___y_11661_);
if (lean_obj_tag(v___x_11686_) == 0)
{
lean_object* v_a_11662_; lean_object* v___x_11663_; uint8_t v___y_11665_; uint8_t v_isNoncomputableSection_11687_;
v_a_11662_ = lean_ctor_get(v___x_11661_, 0);
lean_inc(v_a_11662_);
lean_dec_ref(v___x_11661_);
v___x_11663_ = lean_st_ref_get(v___y_11659_);
v_isNoncomputableSection_11687_ = lean_ctor_get_uint8(v___y_11654_, sizeof(void*)*8 + 4);
if (v_isNoncomputableSection_11687_ == 0)
{
lean_object* v_declName_x3f_11688_;
v_declName_x3f_11688_ = lean_ctor_get(v___y_11654_, 0);
lean_inc(v_declName_x3f_11688_);
lean_dec_ref(v___y_11654_);
if (lean_obj_tag(v_declName_x3f_11688_) == 0)
{
lean_dec(v___x_11663_);
v___y_11665_ = v_isExporting_11653_;
goto v___jp_11664_;
}
else
{
lean_object* v_env_11689_; lean_object* v_val_11690_; lean_object* v___x_11691_; lean_object* v_toEnvExtension_11692_; lean_object* v_asyncMode_11693_; uint8_t v___x_11694_;
v_env_11689_ = lean_ctor_get(v___x_11663_, 0);
lean_object* v_a_11687_; lean_object* v___x_11688_; lean_object* v_env_11689_; lean_object* v_declName_x3f_11690_; uint8_t v_isNoncomputableSection_11691_; uint8_t v___y_11693_;
v_a_11687_ = lean_ctor_get(v___x_11686_, 0);
lean_inc(v_a_11687_);
lean_dec_ref(v___x_11686_);
v___x_11688_ = lean_st_ref_get(v___y_11661_);
v_env_11689_ = lean_ctor_get(v___x_11688_, 0);
lean_inc_ref(v_env_11689_);
lean_dec(v___x_11663_);
v_val_11690_ = lean_ctor_get(v_declName_x3f_11688_, 0);
lean_inc(v_val_11690_);
lean_dec_ref(v_declName_x3f_11688_);
v___x_11691_ = l_Lean_noncomputableExt;
v_toEnvExtension_11692_ = lean_ctor_get(v___x_11691_, 0);
lean_inc_ref(v_toEnvExtension_11692_);
v_asyncMode_11693_ = lean_ctor_get(v_toEnvExtension_11692_, 2);
lean_inc(v_asyncMode_11693_);
lean_dec_ref(v_toEnvExtension_11692_);
v___x_11694_ = l_Lean_isNoncomputable(v_env_11689_, v_val_11690_, v_asyncMode_11693_);
lean_dec(v_asyncMode_11693_);
if (v___x_11694_ == 0)
lean_dec(v___x_11688_);
v_declName_x3f_11690_ = lean_ctor_get(v___y_11656_, 0);
lean_inc(v_declName_x3f_11690_);
v_isNoncomputableSection_11691_ = lean_ctor_get_uint8(v___y_11656_, sizeof(void*)*8 + 4);
lean_dec_ref(v___y_11656_);
if (v_isNoncomputableSection_11691_ == 0)
{
v___y_11665_ = v_isExporting_11653_;
goto v___jp_11664_;
if (lean_obj_tag(v_declName_x3f_11690_) == 0)
{
lean_dec_ref(v_env_11689_);
v___y_11693_ = v_isExporting_11655_;
goto v___jp_11692_;
}
else
{
v___y_11665_ = v_isNoncomputableSection_11687_;
goto v___jp_11664_;
lean_object* v_val_11746_; lean_object* v___x_11747_; lean_object* v_toEnvExtension_11748_; lean_object* v_asyncMode_11749_; uint8_t v___x_11750_;
v_val_11746_ = lean_ctor_get(v_declName_x3f_11690_, 0);
v___x_11747_ = l_Lean_noncomputableExt;
v_toEnvExtension_11748_ = lean_ctor_get(v___x_11747_, 0);
lean_inc_ref(v_toEnvExtension_11748_);
v_asyncMode_11749_ = lean_ctor_get(v_toEnvExtension_11748_, 2);
lean_inc(v_asyncMode_11749_);
lean_dec_ref(v_toEnvExtension_11748_);
lean_inc(v_val_11746_);
v___x_11750_ = l_Lean_isNoncomputable(v_env_11689_, v_val_11746_, v_asyncMode_11749_);
lean_dec(v_asyncMode_11749_);
if (v___x_11750_ == 0)
{
v___y_11693_ = v_isExporting_11655_;
goto v___jp_11692_;
}
else
{
v___y_11693_ = v_isNoncomputableSection_11691_;
goto v___jp_11692_;
}
}
}
else
{
uint8_t v___x_11695_;
lean_dec(v___x_11663_);
lean_dec_ref(v___y_11654_);
v___x_11695_ = 0;
v___y_11665_ = v___x_11695_;
goto v___jp_11664_;
uint8_t v___x_11751_;
lean_dec_ref(v_env_11689_);
v___x_11751_ = 0;
v___y_11693_ = v___x_11751_;
goto v___jp_11692_;
}
v___jp_11664_:
v___jp_11692_:
{
uint8_t v___x_11666_; lean_object* v___x_11667_;
v___x_11666_ = 0;
uint8_t v___x_11694_; lean_object* v___x_11695_;
v___x_11694_ = 0;
lean_inc(v___y_11661_);
lean_inc_ref(v___y_11660_);
lean_inc(v___y_11659_);
lean_inc_ref(v___y_11658_);
lean_inc(v___y_11657_);
lean_inc_ref(v___y_11656_);
lean_inc(v_a_11652_);
v___x_11667_ = l_Lean_Meta_mkAuxDefinitionFor(v_a_11652_, v_a_11662_, v___x_11666_, v___y_11665_, v___y_11656_, v___y_11657_, v___y_11658_, v___y_11659_);
if (lean_obj_tag(v___x_11667_) == 0)
lean_inc(v_a_11653_);
v___x_11695_ = l_Lean_Meta_mkAuxDefinitionFor(v_a_11653_, v_a_11687_, v___x_11694_, v___x_11694_, v___y_11658_, v___y_11659_, v___y_11660_, v___y_11661_);
if (lean_obj_tag(v___x_11695_) == 0)
{
if (v___y_11665_ == 0)
if (v___y_11693_ == 0)
{
lean_dec(v_declName_x3f_11690_);
lean_dec(v___y_11661_);
lean_dec_ref(v___y_11660_);
lean_dec(v___y_11659_);
lean_dec_ref(v___y_11658_);
lean_dec(v___y_11657_);
lean_dec_ref(v___y_11656_);
lean_dec(v_a_11652_);
return v___x_11667_;
lean_dec(v_a_11653_);
return v___x_11695_;
}
else
{
lean_object* v_a_11668_; uint8_t v___x_11669_; lean_object* v___x_11670_;
v_a_11668_ = lean_ctor_get(v___x_11667_, 0);
lean_inc(v_a_11668_);
lean_dec_ref(v___x_11667_);
v___x_11669_ = 0;
v___x_11670_ = l_Lean_Meta_setInlineAttribute(v_a_11652_, v___x_11669_, v___y_11656_, v___y_11657_, v___y_11658_, v___y_11659_);
lean_dec(v___y_11659_);
lean_object* v_a_11696_; uint8_t v___x_11697_; lean_object* v___x_11698_;
v_a_11696_ = lean_ctor_get(v___x_11695_, 0);
lean_inc(v_a_11696_);
lean_dec_ref(v___x_11695_);
v___x_11697_ = 0;
lean_inc(v_a_11653_);
v___x_11698_ = l_Lean_Meta_setInlineAttribute(v_a_11653_, v___x_11697_, v___y_11658_, v___y_11659_, v___y_11660_, v___y_11661_);
lean_dec_ref(v___y_11658_);
lean_dec(v___y_11657_);
lean_dec_ref(v___y_11656_);
if (lean_obj_tag(v___x_11670_) == 0)
if (lean_obj_tag(v___x_11698_) == 0)
{
lean_object* v___x_11672_; uint8_t v_isShared_11673_; uint8_t v_isSharedCheck_11677_;
v_isSharedCheck_11677_ = !lean_is_exclusive(v___x_11670_);
if (v_isSharedCheck_11677_ == 0)
lean_object* v___x_11699_;
lean_dec_ref(v___x_11698_);
v___x_11699_ = lean_st_ref_get(v___y_11661_);
if (lean_obj_tag(v_declName_x3f_11690_) == 0)
{
lean_object* v_unused_11678_;
v_unused_11678_ = lean_ctor_get(v___x_11670_, 0);
lean_dec(v_unused_11678_);
v___x_11672_ = v___x_11670_;
v_isShared_11673_ = v_isSharedCheck_11677_;
goto v_resetjp_11671_;
lean_dec(v___x_11699_);
lean_dec(v___y_11659_);
v___y_11664_ = v_a_11696_;
v___y_11665_ = v___y_11660_;
v___y_11666_ = v___y_11661_;
goto v___jp_11663_;
}
else
{
lean_dec(v___x_11670_);
v___x_11672_ = lean_box(0);
v_isShared_11673_ = v_isSharedCheck_11677_;
goto v_resetjp_11671_;
}
v_resetjp_11671_:
{
lean_object* v___x_11675_;
if (v_isShared_11673_ == 0)
{
lean_ctor_set(v___x_11672_, 0, v_a_11668_);
v___x_11675_ = v___x_11672_;
goto v_reusejp_11674_;
}
else
{
lean_object* v_reuseFailAlloc_11676_;
v_reuseFailAlloc_11676_ = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(v_reuseFailAlloc_11676_, 0, v_a_11668_);
v___x_11675_ = v_reuseFailAlloc_11676_;
goto v_reusejp_11674_;
}
v_reusejp_11674_:
{
return v___x_11675_;
}
}
}
else
{
lean_object* v_a_11679_; lean_object* v___x_11681_; uint8_t v_isShared_11682_; uint8_t v_isSharedCheck_11686_;
lean_dec(v_a_11668_);
v_a_11679_ = lean_ctor_get(v___x_11670_, 0);
v_isSharedCheck_11686_ = !lean_is_exclusive(v___x_11670_);
if (v_isSharedCheck_11686_ == 0)
{
v___x_11681_ = v___x_11670_;
v_isShared_11682_ = v_isSharedCheck_11686_;
goto v_resetjp_11680_;
}
else
{
lean_inc(v_a_11679_);
lean_dec(v___x_11670_);
v___x_11681_ = lean_box(0);
v_isShared_11682_ = v_isSharedCheck_11686_;
goto v_resetjp_11680_;
}
v_resetjp_11680_:
{
lean_object* v___x_11684_;
if (v_isShared_11682_ == 0)
{
v___x_11684_ = v___x_11681_;
goto v_reusejp_11683_;
}
else
{
lean_object* v_reuseFailAlloc_11685_;
v_reuseFailAlloc_11685_ = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(v_reuseFailAlloc_11685_, 0, v_a_11679_);
v___x_11684_ = v_reuseFailAlloc_11685_;
goto v_reusejp_11683_;
}
v_reusejp_11683_:
{
return v___x_11684_;
}
}
}
}
}
else
lean_object* v_val_11700_; lean_object* v_env_11701_; uint8_t v___x_11702_;
v_val_11700_ = lean_ctor_get(v_declName_x3f_11690_, 0);
lean_inc(v_val_11700_);
lean_dec_ref(v_declName_x3f_11690_);
v_env_11701_ = lean_ctor_get(v___x_11699_, 0);
lean_inc_ref(v_env_11701_);
lean_dec(v___x_11699_);
v___x_11702_ = l_Lean_isMarkedMeta(v_env_11701_, v_val_11700_);
if (v___x_11702_ == 0)
{
lean_dec(v___y_11659_);
lean_dec_ref(v___y_11658_);
lean_dec(v___y_11657_);
lean_dec_ref(v___y_11656_);
lean_dec(v_a_11652_);
return v___x_11667_;
}
}
v___y_11664_ = v_a_11696_;
v___y_11665_ = v___y_11660_;
v___y_11666_ = v___y_11661_;
goto v___jp_11663_;
}
else
{
lean_object* v___x_11703_; lean_object* v_env_11704_; lean_object* v_nextMacroScope_11705_; lean_object* v_ngen_11706_; lean_object* v_auxDeclNGen_11707_; lean_object* v_traceState_11708_; lean_object* v_messages_11709_; lean_object* v_infoState_11710_; lean_object* v_snapshotTasks_11711_; lean_object* v___x_11713_; uint8_t v_isShared_11714_; uint8_t v_isSharedCheck_11736_;
v___x_11703_ = lean_st_ref_take(v___y_11661_);
v_env_11704_ = lean_ctor_get(v___x_11703_, 0);
v_nextMacroScope_11705_ = lean_ctor_get(v___x_11703_, 1);
v_ngen_11706_ = lean_ctor_get(v___x_11703_, 2);
v_auxDeclNGen_11707_ = lean_ctor_get(v___x_11703_, 3);
v_traceState_11708_ = lean_ctor_get(v___x_11703_, 4);
v_messages_11709_ = lean_ctor_get(v___x_11703_, 6);
v_infoState_11710_ = lean_ctor_get(v___x_11703_, 7);
v_snapshotTasks_11711_ = lean_ctor_get(v___x_11703_, 8);
v_isSharedCheck_11736_ = !lean_is_exclusive(v___x_11703_);
if (v_isSharedCheck_11736_ == 0)
{
lean_object* v_unused_11737_;
v_unused_11737_ = lean_ctor_get(v___x_11703_, 5);
lean_dec(v_unused_11737_);
v___x_11713_ = v___x_11703_;
v_isShared_11714_ = v_isSharedCheck_11736_;
goto v_resetjp_11712_;
}
else
{
lean_inc(v_snapshotTasks_11711_);
lean_inc(v_infoState_11710_);
lean_inc(v_messages_11709_);
lean_inc(v_traceState_11708_);
lean_inc(v_auxDeclNGen_11707_);
lean_inc(v_ngen_11706_);
lean_inc(v_nextMacroScope_11705_);
lean_inc(v_env_11704_);
lean_dec(v___x_11703_);
v___x_11713_ = lean_box(0);
v_isShared_11714_ = v_isSharedCheck_11736_;
goto v_resetjp_11712_;
}
v_resetjp_11712_:
{
lean_object* v___x_11715_; lean_object* v___x_11716_; lean_object* v___x_11718_;
lean_inc(v_a_11653_);
v___x_11715_ = l_Lean_markMeta(v_env_11704_, v_a_11653_);
v___x_11716_ = lean_obj_once(&l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Term_elabDoubleQuotedName_spec__0_spec__0___closed__5, &l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Term_elabDoubleQuotedName_spec__0_spec__0___closed__5_once, _init_l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Term_elabDoubleQuotedName_spec__0_spec__0___closed__5);
if (v_isShared_11714_ == 0)
{
lean_ctor_set(v___x_11713_, 5, v___x_11716_);
lean_ctor_set(v___x_11713_, 0, v___x_11715_);
v___x_11718_ = v___x_11713_;
goto v_reusejp_11717_;
}
else
{
lean_object* v_reuseFailAlloc_11735_;
v_reuseFailAlloc_11735_ = lean_alloc_ctor(0, 9, 0);
lean_ctor_set(v_reuseFailAlloc_11735_, 0, v___x_11715_);
lean_ctor_set(v_reuseFailAlloc_11735_, 1, v_nextMacroScope_11705_);
lean_ctor_set(v_reuseFailAlloc_11735_, 2, v_ngen_11706_);
lean_ctor_set(v_reuseFailAlloc_11735_, 3, v_auxDeclNGen_11707_);
lean_ctor_set(v_reuseFailAlloc_11735_, 4, v_traceState_11708_);
lean_ctor_set(v_reuseFailAlloc_11735_, 5, v___x_11716_);
lean_ctor_set(v_reuseFailAlloc_11735_, 6, v_messages_11709_);
lean_ctor_set(v_reuseFailAlloc_11735_, 7, v_infoState_11710_);
lean_ctor_set(v_reuseFailAlloc_11735_, 8, v_snapshotTasks_11711_);
v___x_11718_ = v_reuseFailAlloc_11735_;
goto v_reusejp_11717_;
}
v_reusejp_11717_:
{
lean_object* v___x_11719_; lean_object* v___x_11720_; lean_object* v_mctx_11721_; lean_object* v_zetaDeltaFVarIds_11722_; lean_object* v_postponed_11723_; lean_object* v_diag_11724_; lean_object* v___x_11726_; uint8_t v_isShared_11727_; uint8_t v_isSharedCheck_11733_;
v___x_11719_ = lean_st_ref_set(v___y_11661_, v___x_11718_);
v___x_11720_ = lean_st_ref_take(v___y_11659_);
v_mctx_11721_ = lean_ctor_get(v___x_11720_, 0);
v_zetaDeltaFVarIds_11722_ = lean_ctor_get(v___x_11720_, 2);
v_postponed_11723_ = lean_ctor_get(v___x_11720_, 3);
v_diag_11724_ = lean_ctor_get(v___x_11720_, 4);
v_isSharedCheck_11733_ = !lean_is_exclusive(v___x_11720_);
if (v_isSharedCheck_11733_ == 0)
{
lean_object* v_unused_11734_;
v_unused_11734_ = lean_ctor_get(v___x_11720_, 1);
lean_dec(v_unused_11734_);
v___x_11726_ = v___x_11720_;
v_isShared_11727_ = v_isSharedCheck_11733_;
goto v_resetjp_11725_;
}
else
{
lean_inc(v_diag_11724_);
lean_inc(v_postponed_11723_);
lean_inc(v_zetaDeltaFVarIds_11722_);
lean_inc(v_mctx_11721_);
lean_dec(v___x_11720_);
v___x_11726_ = lean_box(0);
v_isShared_11727_ = v_isSharedCheck_11733_;
goto v_resetjp_11725_;
}
v_resetjp_11725_:
{
lean_object* v___x_11728_; lean_object* v___x_11730_;
v___x_11728_ = lean_obj_once(&l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Term_elabDoubleQuotedName_spec__0_spec__0___closed__6, &l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Term_elabDoubleQuotedName_spec__0_spec__0___closed__6_once, _init_l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Term_elabDoubleQuotedName_spec__0_spec__0___closed__6);
if (v_isShared_11727_ == 0)
{
lean_ctor_set(v___x_11726_, 1, v___x_11728_);
v___x_11730_ = v___x_11726_;
goto v_reusejp_11729_;
}
else
{
lean_object* v_reuseFailAlloc_11732_;
v_reuseFailAlloc_11732_ = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(v_reuseFailAlloc_11732_, 0, v_mctx_11721_);
lean_ctor_set(v_reuseFailAlloc_11732_, 1, v___x_11728_);
lean_ctor_set(v_reuseFailAlloc_11732_, 2, v_zetaDeltaFVarIds_11722_);
lean_ctor_set(v_reuseFailAlloc_11732_, 3, v_postponed_11723_);
lean_ctor_set(v_reuseFailAlloc_11732_, 4, v_diag_11724_);
v___x_11730_ = v_reuseFailAlloc_11732_;
goto v_reusejp_11729_;
}
v_reusejp_11729_:
{
lean_object* v___x_11731_;
v___x_11731_ = lean_st_ref_set(v___y_11659_, v___x_11730_);
lean_dec(v___y_11659_);
lean_dec_ref(v___y_11658_);
lean_dec(v___y_11657_);
lean_dec_ref(v___y_11656_);
lean_dec_ref(v___y_11654_);
lean_dec(v_a_11652_);
return v___x_11661_;
v___y_11664_ = v_a_11696_;
v___y_11665_ = v___y_11660_;
v___y_11666_ = v___y_11661_;
goto v___jp_11663_;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl___lam__0___boxed(lean_object* v___x_11696_, lean_object* v_expectedType_x3f_11697_, lean_object* v_a_11698_, lean_object* v_isExporting_11699_, lean_object* v___y_11700_, lean_object* v___y_11701_, lean_object* v___y_11702_, lean_object* v___y_11703_, lean_object* v___y_11704_, lean_object* v___y_11705_, lean_object* v___y_11706_){
_start:
{
uint8_t v_isExporting_boxed_11707_; lean_object* v_res_11708_;
v_isExporting_boxed_11707_ = lean_unbox(v_isExporting_11699_);
v_res_11708_ = l_Lean_Elab_Term_elabPrivateDecl___lam__0(v___x_11696_, v_expectedType_x3f_11697_, v_a_11698_, v_isExporting_boxed_11707_, v___y_11700_, v___y_11701_, v___y_11702_, v___y_11703_, v___y_11704_, v___y_11705_);
return v_res_11708_;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl(lean_object* v_stx_11718_, lean_object* v_expectedType_x3f_11719_, lean_object* v_a_11720_, lean_object* v_a_11721_, lean_object* v_a_11722_, lean_object* v_a_11723_, lean_object* v_a_11724_, lean_object* v_a_11725_){
_start:
{
lean_object* v___x_11727_; uint8_t v___x_11728_;
v___x_11727_ = ((lean_object*)(l_Lean_Elab_Term_elabPrivateDecl___closed__1));
lean_inc(v_stx_11718_);
v___x_11728_ = l_Lean_Syntax_isOfKind(v_stx_11718_, v___x_11727_);
if (v___x_11728_ == 0)
{
lean_object* v___x_11729_;
lean_dec(v_a_11725_);
lean_dec_ref(v_a_11724_);
lean_dec(v_a_11723_);
lean_dec_ref(v_a_11722_);
lean_dec(v_a_11721_);
lean_dec_ref(v_a_11720_);
lean_dec(v_expectedType_x3f_11719_);
lean_dec(v_stx_11718_);
v___x_11729_ = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Term_elabLetMVar_spec__0___redArg();
return v___x_11729_;
}
else
{
lean_object* v___x_11730_; lean_object* v_env_11731_; uint8_t v_isExporting_11732_; lean_object* v___x_11733_; lean_object* v___x_11734_;
v___x_11730_ = lean_st_ref_get(v_a_11725_);
v_env_11731_ = lean_ctor_get(v___x_11730_, 0);
lean_inc_ref(v_env_11731_);
lean_dec(v___x_11730_);
v_isExporting_11732_ = lean_ctor_get_uint8(v_env_11731_, sizeof(void*)*8);
lean_dec_ref(v_env_11731_);
v___x_11733_ = lean_unsigned_to_nat(1u);
v___x_11734_ = l_Lean_Syntax_getArg(v_stx_11718_, v___x_11733_);
lean_dec(v_stx_11718_);
if (v_isExporting_11732_ == 0)
lean_object* v_a_11738_; lean_object* v___x_11740_; uint8_t v_isShared_11741_; uint8_t v_isSharedCheck_11745_;
lean_dec(v_a_11696_);
lean_dec(v_declName_x3f_11690_);
lean_dec(v___y_11661_);
lean_dec_ref(v___y_11660_);
lean_dec(v___y_11659_);
lean_dec(v_a_11653_);
v_a_11738_ = lean_ctor_get(v___x_11698_, 0);
v_isSharedCheck_11745_ = !lean_is_exclusive(v___x_11698_);
if (v_isSharedCheck_11745_ == 0)
{
lean_object* v___x_11735_;
v___x_11735_ = l_Lean_Elab_Term_elabTerm(v___x_11734_, v_expectedType_x3f_11719_, v___x_11728_, v___x_11728_, v_a_11720_, v_a_11721_, v_a_11722_, v_a_11723_, v_a_11724_, v_a_11725_);
return v___x_11735_;
v___x_11740_ = v___x_11698_;
v_isShared_11741_ = v_isSharedCheck_11745_;
goto v_resetjp_11739_;
}
else
{
lean_object* v___x_11736_; lean_object* v___x_11737_; lean_object* v_a_11738_; lean_object* v___x_11739_; lean_object* v___f_11740_; lean_object* v___x_11741_;
v___x_11736_ = ((lean_object*)(l_Lean_Elab_Term_elabPrivateDecl___closed__3));
v___x_11737_ = l_Lean_mkAuxDeclName___at___00Lean_Elab_Term_elabPrivateDecl_spec__0___redArg(v___x_11736_, v_a_11725_);
v_a_11738_ = lean_ctor_get(v___x_11737_, 0);
lean_inc(v_a_11738_);
lean_dec_ref(v___x_11737_);
v___x_11739_ = lean_box(v_isExporting_11732_);
v___f_11740_ = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabPrivateDecl___lam__0___boxed), 11, 4);
lean_closure_set(v___f_11740_, 0, v___x_11734_);
lean_closure_set(v___f_11740_, 1, v_expectedType_x3f_11719_);
lean_closure_set(v___f_11740_, 2, v_a_11738_);
lean_closure_set(v___f_11740_, 3, v___x_11739_);
v___x_11741_ = l_Lean_withoutExporting___at___00Lean_Elab_Term_elabDoubleQuotedName_spec__1___redArg(v___f_11740_, v___x_11728_, v_a_11720_, v_a_11721_, v_a_11722_, v_a_11723_, v_a_11724_, v_a_11725_);
return v___x_11741_;
lean_dec(v___x_11698_);
v___x_11740_ = lean_box(0);
v_isShared_11741_ = v_isSharedCheck_11745_;
goto v_resetjp_11739_;
}
v_resetjp_11739_:
{
lean_object* v___x_11743_;
if (v_isShared_11741_ == 0)
{
v___x_11743_ = v___x_11740_;
goto v_reusejp_11742_;
}
else
{
lean_object* v_reuseFailAlloc_11744_;
v_reuseFailAlloc_11744_ = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(v_reuseFailAlloc_11744_, 0, v_a_11738_);
v___x_11743_ = v_reuseFailAlloc_11744_;
goto v_reusejp_11742_;
}
v_reusejp_11742_:
{
return v___x_11743_;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl___boxed(lean_object* v_stx_11742_, lean_object* v_expectedType_x3f_11743_, lean_object* v_a_11744_, lean_object* v_a_11745_, lean_object* v_a_11746_, lean_object* v_a_11747_, lean_object* v_a_11748_, lean_object* v_a_11749_, lean_object* v_a_11750_){
}
else
{
lean_dec(v_declName_x3f_11690_);
lean_dec(v___y_11661_);
lean_dec_ref(v___y_11660_);
lean_dec(v___y_11659_);
lean_dec_ref(v___y_11658_);
lean_dec(v_a_11653_);
return v___x_11695_;
}
}
}
else
{
lean_dec(v___y_11661_);
lean_dec_ref(v___y_11660_);
lean_dec(v___y_11659_);
lean_dec_ref(v___y_11658_);
lean_dec_ref(v___y_11656_);
lean_dec(v_a_11653_);
return v___x_11686_;
}
v___jp_11663_:
{
lean_object* v___x_11667_; lean_object* v___x_11668_; lean_object* v___x_11669_;
v___x_11667_ = lean_mk_empty_array_with_capacity(v___x_11652_);
v___x_11668_ = lean_array_push(v___x_11667_, v_a_11653_);
v___x_11669_ = l_Lean_compileDecls(v___x_11668_, v___x_11654_, v___y_11665_, v___y_11666_);
if (lean_obj_tag(v___x_11669_) == 0)
{
lean_object* v___x_11671_; uint8_t v_isShared_11672_; uint8_t v_isSharedCheck_11676_;
v_isSharedCheck_11676_ = !lean_is_exclusive(v___x_11669_);
if (v_isSharedCheck_11676_ == 0)
{
lean_object* v_unused_11677_;
v_unused_11677_ = lean_ctor_get(v___x_11669_, 0);
lean_dec(v_unused_11677_);
v___x_11671_ = v___x_11669_;
v_isShared_11672_ = v_isSharedCheck_11676_;
goto v_resetjp_11670_;
}
else
{
lean_dec(v___x_11669_);
v___x_11671_ = lean_box(0);
v_isShared_11672_ = v_isSharedCheck_11676_;
goto v_resetjp_11670_;
}
v_resetjp_11670_:
{
lean_object* v___x_11674_;
if (v_isShared_11672_ == 0)
{
lean_ctor_set(v___x_11671_, 0, v___y_11664_);
v___x_11674_ = v___x_11671_;
goto v_reusejp_11673_;
}
else
{
lean_object* v_reuseFailAlloc_11675_;
v_reuseFailAlloc_11675_ = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(v_reuseFailAlloc_11675_, 0, v___y_11664_);
v___x_11674_ = v_reuseFailAlloc_11675_;
goto v_reusejp_11673_;
}
v_reusejp_11673_:
{
return v___x_11674_;
}
}
}
else
{
lean_object* v_a_11678_; lean_object* v___x_11680_; uint8_t v_isShared_11681_; uint8_t v_isSharedCheck_11685_;
lean_dec_ref(v___y_11664_);
v_a_11678_ = lean_ctor_get(v___x_11669_, 0);
v_isSharedCheck_11685_ = !lean_is_exclusive(v___x_11669_);
if (v_isSharedCheck_11685_ == 0)
{
v___x_11680_ = v___x_11669_;
v_isShared_11681_ = v_isSharedCheck_11685_;
goto v_resetjp_11679_;
}
else
{
lean_inc(v_a_11678_);
lean_dec(v___x_11669_);
v___x_11680_ = lean_box(0);
v_isShared_11681_ = v_isSharedCheck_11685_;
goto v_resetjp_11679_;
}
v_resetjp_11679_:
{
lean_object* v___x_11683_;
if (v_isShared_11681_ == 0)
{
v___x_11683_ = v___x_11680_;
goto v_reusejp_11682_;
}
else
{
lean_object* v_reuseFailAlloc_11684_;
v_reuseFailAlloc_11684_ = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(v_reuseFailAlloc_11684_, 0, v_a_11678_);
v___x_11683_ = v_reuseFailAlloc_11684_;
goto v_reusejp_11682_;
}
v_reusejp_11682_:
{
return v___x_11683_;
}
}
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl___lam__0___boxed(lean_object* v___x_11752_, lean_object* v_expectedType_x3f_11753_, lean_object* v___x_11754_, lean_object* v_a_11755_, lean_object* v___x_11756_, lean_object* v_isExporting_11757_, lean_object* v___y_11758_, lean_object* v___y_11759_, lean_object* v___y_11760_, lean_object* v___y_11761_, lean_object* v___y_11762_, lean_object* v___y_11763_, lean_object* v___y_11764_){
_start:
{
lean_object* v_res_11751_;
v_res_11751_ = l_Lean_Elab_Term_elabPrivateDecl(v_stx_11742_, v_expectedType_x3f_11743_, v_a_11744_, v_a_11745_, v_a_11746_, v_a_11747_, v_a_11748_, v_a_11749_);
return v_res_11751_;
uint8_t v___x_6945__boxed_11765_; uint8_t v_isExporting_boxed_11766_; lean_object* v_res_11767_;
v___x_6945__boxed_11765_ = lean_unbox(v___x_11756_);
v_isExporting_boxed_11766_ = lean_unbox(v_isExporting_11757_);
v_res_11767_ = l_Lean_Elab_Term_elabPrivateDecl___lam__0(v___x_11752_, v_expectedType_x3f_11753_, v___x_11754_, v_a_11755_, v___x_6945__boxed_11765_, v_isExporting_boxed_11766_, v___y_11758_, v___y_11759_, v___y_11760_, v___y_11761_, v___y_11762_, v___y_11763_);
lean_dec(v___x_11754_);
return v_res_11767_;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl(lean_object* v_stx_11777_, lean_object* v_expectedType_x3f_11778_, lean_object* v_a_11779_, lean_object* v_a_11780_, lean_object* v_a_11781_, lean_object* v_a_11782_, lean_object* v_a_11783_, lean_object* v_a_11784_){
_start:
{
lean_object* v___x_11786_; uint8_t v___x_11787_;
v___x_11786_ = ((lean_object*)(l_Lean_Elab_Term_elabPrivateDecl___closed__1));
lean_inc(v_stx_11777_);
v___x_11787_ = l_Lean_Syntax_isOfKind(v_stx_11777_, v___x_11786_);
if (v___x_11787_ == 0)
{
lean_object* v___x_11788_;
lean_dec(v_a_11784_);
lean_dec_ref(v_a_11783_);
lean_dec(v_a_11782_);
lean_dec_ref(v_a_11781_);
lean_dec(v_a_11780_);
lean_dec_ref(v_a_11779_);
lean_dec(v_expectedType_x3f_11778_);
lean_dec(v_stx_11777_);
v___x_11788_ = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Term_elabLetMVar_spec__0___redArg();
return v___x_11788_;
}
else
{
lean_object* v___x_11789_; lean_object* v_env_11790_; uint8_t v_isExporting_11791_; lean_object* v___x_11792_; lean_object* v___x_11793_;
v___x_11789_ = lean_st_ref_get(v_a_11784_);
v_env_11790_ = lean_ctor_get(v___x_11789_, 0);
lean_inc_ref(v_env_11790_);
lean_dec(v___x_11789_);
v_isExporting_11791_ = lean_ctor_get_uint8(v_env_11790_, sizeof(void*)*8);
lean_dec_ref(v_env_11790_);
v___x_11792_ = lean_unsigned_to_nat(1u);
v___x_11793_ = l_Lean_Syntax_getArg(v_stx_11777_, v___x_11792_);
lean_dec(v_stx_11777_);
if (v_isExporting_11791_ == 0)
{
lean_object* v___x_11794_;
v___x_11794_ = l_Lean_Elab_Term_elabTerm(v___x_11793_, v_expectedType_x3f_11778_, v___x_11787_, v___x_11787_, v_a_11779_, v_a_11780_, v_a_11781_, v_a_11782_, v_a_11783_, v_a_11784_);
return v___x_11794_;
}
else
{
lean_object* v___x_11795_; lean_object* v___x_11796_; lean_object* v_a_11797_; lean_object* v___x_11798_; lean_object* v___x_11799_; lean_object* v___f_11800_; lean_object* v___x_11801_;
v___x_11795_ = ((lean_object*)(l_Lean_Elab_Term_elabPrivateDecl___closed__3));
v___x_11796_ = l_Lean_mkAuxDeclName___at___00Lean_Elab_Term_elabPrivateDecl_spec__0___redArg(v___x_11795_, v_a_11784_);
v_a_11797_ = lean_ctor_get(v___x_11796_, 0);
lean_inc(v_a_11797_);
lean_dec_ref(v___x_11796_);
v___x_11798_ = lean_box(v___x_11787_);
v___x_11799_ = lean_box(v_isExporting_11791_);
v___f_11800_ = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabPrivateDecl___lam__0___boxed), 13, 6);
lean_closure_set(v___f_11800_, 0, v___x_11793_);
lean_closure_set(v___f_11800_, 1, v_expectedType_x3f_11778_);
lean_closure_set(v___f_11800_, 2, v___x_11792_);
lean_closure_set(v___f_11800_, 3, v_a_11797_);
lean_closure_set(v___f_11800_, 4, v___x_11798_);
lean_closure_set(v___f_11800_, 5, v___x_11799_);
v___x_11801_ = l_Lean_withoutExporting___at___00Lean_Elab_Term_elabDoubleQuotedName_spec__1___redArg(v___f_11800_, v___x_11787_, v_a_11779_, v_a_11780_, v_a_11781_, v_a_11782_, v_a_11783_, v_a_11784_);
return v___x_11801_;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl___boxed(lean_object* v_stx_11802_, lean_object* v_expectedType_x3f_11803_, lean_object* v_a_11804_, lean_object* v_a_11805_, lean_object* v_a_11806_, lean_object* v_a_11807_, lean_object* v_a_11808_, lean_object* v_a_11809_, lean_object* v_a_11810_){
_start:
{
lean_object* v_res_11811_;
v_res_11811_ = l_Lean_Elab_Term_elabPrivateDecl(v_stx_11802_, v_expectedType_x3f_11803_, v_a_11804_, v_a_11805_, v_a_11806_, v_a_11807_, v_a_11808_, v_a_11809_);
return v_res_11811_;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl___regBuiltin_Lean_Elab_Term_elabPrivateDecl__1(){
_start:
{
lean_object* v___x_11759_; lean_object* v___x_11760_; lean_object* v___x_11761_; lean_object* v___x_11762_; lean_object* v___x_11763_;
v___x_11759_ = l_Lean_Elab_Term_termElabAttribute;
v___x_11760_ = ((lean_object*)(l_Lean_Elab_Term_elabPrivateDecl___closed__1));
v___x_11761_ = ((lean_object*)(l_Lean_Elab_Term_elabPrivateDecl___regBuiltin_Lean_Elab_Term_elabPrivateDecl__1___closed__1));
v___x_11762_ = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabPrivateDecl___boxed), 9, 0);
v___x_11763_ = l_Lean_KeyedDeclsAttribute_addBuiltin___redArg(v___x_11759_, v___x_11760_, v___x_11761_, v___x_11762_);
return v___x_11763_;
lean_object* v___x_11819_; lean_object* v___x_11820_; lean_object* v___x_11821_; lean_object* v___x_11822_; lean_object* v___x_11823_;
v___x_11819_ = l_Lean_Elab_Term_termElabAttribute;
v___x_11820_ = ((lean_object*)(l_Lean_Elab_Term_elabPrivateDecl___closed__1));
v___x_11821_ = ((lean_object*)(l_Lean_Elab_Term_elabPrivateDecl___regBuiltin_Lean_Elab_Term_elabPrivateDecl__1___closed__1));
v___x_11822_ = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabPrivateDecl___boxed), 9, 0);
v___x_11823_ = l_Lean_KeyedDeclsAttribute_addBuiltin___redArg(v___x_11819_, v___x_11820_, v___x_11821_, v___x_11822_);
return v___x_11823_;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl___regBuiltin_Lean_Elab_Term_elabPrivateDecl__1___boxed(lean_object* v_a_11764_){
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabPrivateDecl___regBuiltin_Lean_Elab_Term_elabPrivateDecl__1___boxed(lean_object* v_a_11824_){
_start:
{
lean_object* v_res_11765_;
v_res_11765_ = l_Lean_Elab_Term_elabPrivateDecl___regBuiltin_Lean_Elab_Term_elabPrivateDecl__1();
return v_res_11765_;
lean_object* v_res_11825_;
v_res_11825_ = l_Lean_Elab_Term_elabPrivateDecl___regBuiltin_Lean_Elab_Term_elabPrivateDecl__1();
return v_res_11825_;
}
}
lean_object* runtime_initialize_Lean_Meta_Diagnostics(uint8_t builtin);

11663
stage0/stdlib/Lean/Elab/DeclModifiers.c generated
View file

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Lean/Elab/DocString/Builtin/Scopes.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.DocString.Builtin.Scopes
// Imports: public import Lean.Elab.DocString import Lean.Elab.DocString.Builtin.Parsing
// Imports: public import Lean.Elab.DocString public import Lean.Elab.DocString.Builtin.Parsing
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"

10
stage0/stdlib/Lean/Elab/ErrorExplanation.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.ErrorExplanation
// Imports: public import Lean.Widget.UserWidget
// Imports: public import Lean.Widget.UserWidget meta import Lean.Widget.UserWidget
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -9412,14 +9412,19 @@ if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* runtime_initialize_Lean_Widget_UserWidget(uint8_t builtin);
static bool _G_meta_initialized = false;
LEAN_EXPORT lean_object* meta_initialize_Lean_Elab_ErrorExplanation(uint8_t builtin) {
lean_object * res;
if (_G_meta_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_meta_initialized = true;
res = runtime_initialize_Lean_Widget_UserWidget(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* initialize_Lean_Widget_UserWidget(uint8_t builtin);
lean_object* initialize_Lean_Widget_UserWidget(uint8_t builtin);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Elab_ErrorExplanation(uint8_t builtin) {
lean_object * res;
@ -9428,6 +9433,9 @@ _G_initialized = true;
res = initialize_Lean_Widget_UserWidget(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Widget_UserWidget(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_Elab_ErrorExplanation(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

44763
stage0/stdlib/Lean/Elab/MutualDef.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Elab/MutualInductive.c generated
View file

@ -329,7 +329,7 @@ lean_object* l_Lean_Elab_sortDeclLevelParams(lean_object*, lean_object*, lean_ob
lean_object* l_Lean_Meta_removeUnused(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_collectFVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArgs(lean_object*);
lean_object* l_Lean_KeyedDeclsAttribute_Def___private__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_KeyedDeclsAttribute_evalIdentKey(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_KeyedDeclsAttribute_init___redArg(lean_object*, lean_object*);
lean_object* l_Lean_KeyedDeclsAttribute_getEntries___redArg(lean_object*, lean_object*, lean_object*);
uint8_t l_List_isEmpty___redArg(lean_object*);
@ -3630,7 +3630,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_MutualInductive_0__Lean_Elab_Comm
_start:
{
lean_object* v___x_351_;
v___x_351_ = l_Lean_KeyedDeclsAttribute_Def___private__1(v_stx_347_, v___y_348_, v___y_349_);
v___x_351_ = l_Lean_KeyedDeclsAttribute_evalIdentKey(v_stx_347_, v___y_348_, v___y_349_);
return v___x_351_;
}
}

16666
stage0/stdlib/Lean/Elab/PreDefinition/Basic.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Elab/Quotation/Precheck.c generated
View file

@ -87,7 +87,7 @@ extern lean_object* l_Lean_Elab_unsupportedSyntaxExceptionId;
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l_Lean_MessageData_ofSyntax(lean_object*);
lean_object* l_Lean_indentD(lean_object*);
lean_object* l_Lean_KeyedDeclsAttribute_Def___private__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_KeyedDeclsAttribute_evalIdentKey(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_mkStr5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_KeyedDeclsAttribute_init___redArg(lean_object*, lean_object*);
lean_object* l_Lean_KeyedDeclsAttribute_getValues___redArg(lean_object*, lean_object*, lean_object*);
@ -1118,7 +1118,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation_initFn___lam__0_00___x40_Lea
_start:
{
lean_object* v___x_215_;
v___x_215_ = l_Lean_KeyedDeclsAttribute_Def___private__1(v_stx_211_, v___y_212_, v___y_213_);
v___x_215_ = l_Lean_KeyedDeclsAttribute_evalIdentKey(v_stx_211_, v___y_212_, v___y_213_);
return v___x_215_;
}
}

10
stage0/stdlib/Lean/ErrorExplanation.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.ErrorExplanation
// Imports: public import Lean.Message public import Lean.EnvExtension public import Lean.DocString.Links
// Imports: public import Lean.Message public import Lean.EnvExtension public import Lean.DocString.Links meta import Lean.Message
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -1924,16 +1924,21 @@ lean_mark_persistent(l_Lean_errorExplanationExt);
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* runtime_initialize_Lean_Message(uint8_t builtin);
static bool _G_meta_initialized = false;
LEAN_EXPORT lean_object* meta_initialize_Lean_ErrorExplanation(uint8_t builtin) {
lean_object * res;
if (_G_meta_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_meta_initialized = true;
res = runtime_initialize_Lean_Message(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* initialize_Lean_Message(uint8_t builtin);
lean_object* initialize_Lean_EnvExtension(uint8_t builtin);
lean_object* initialize_Lean_DocString_Links(uint8_t builtin);
lean_object* initialize_Lean_Message(uint8_t builtin);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_ErrorExplanation(uint8_t builtin) {
lean_object * res;
@ -1948,6 +1953,9 @@ lean_dec_ref(res);
res = initialize_Lean_DocString_Links(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Message(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_ErrorExplanation(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

12587
stage0/stdlib/Lean/KeyedDeclsAttribute.c generated
View file

File diff suppressed because it is too large Load diff

4085
stage0/stdlib/Lean/Meta/Constructions/CtorIdx.c generated
View file

File diff suppressed because it is too large Load diff

3437
stage0/stdlib/Lean/Meta/Eval.c generated
View file

File diff suppressed because it is too large Load diff

13901
stage0/stdlib/Lean/Meta/Match/Match.c generated
View file

File diff suppressed because it is too large Load diff

8939
stage0/stdlib/Lean/Meta/Match/MatchEqs.c generated
View file

File diff suppressed because it is too large Load diff

3581
stage0/stdlib/Lean/Meta/Native.c generated
View file

File diff suppressed because it is too large Load diff

10
stage0/stdlib/Lean/Meta/Tactic/Grind/CheckResult.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Meta.Tactic.Grind.CheckResult
// Imports: public import Init.Data.Repr import Init.MetaTypes
// Imports: public import Init.Data.Repr meta import Init.MetaTypes
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -722,7 +722,6 @@ return v_r_200_;
}
}
lean_object* runtime_initialize_Init_Data_Repr(uint8_t builtin);
lean_object* runtime_initialize_Init_MetaTypes(uint8_t builtin);
static bool _G_runtime_initialized = false;
LEAN_EXPORT lean_object* runtime_initialize_Lean_Meta_Tactic_Grind_CheckResult(uint8_t builtin) {
lean_object * res;
@ -731,18 +730,19 @@ _G_runtime_initialized = true;
res = runtime_initialize_Init_Data_Repr(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Init_MetaTypes(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Meta_Grind_instInhabitedCheckResult_default = _init_l_Lean_Meta_Grind_instInhabitedCheckResult_default();
l_Lean_Meta_Grind_instInhabitedCheckResult = _init_l_Lean_Meta_Grind_instInhabitedCheckResult();
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* runtime_initialize_Init_MetaTypes(uint8_t builtin);
static bool _G_meta_initialized = false;
LEAN_EXPORT lean_object* meta_initialize_Lean_Meta_Tactic_Grind_CheckResult(uint8_t builtin) {
lean_object * res;
if (_G_meta_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_meta_initialized = true;
res = runtime_initialize_Init_MetaTypes(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* initialize_Init_Data_Repr(uint8_t builtin);

10
stage0/stdlib/Lean/Meta/Tactic/TryThis.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Meta.Tactic.TryThis
// Imports: import Lean.Server.CodeActions import Lean.Meta.Tactic.ExposeNames public import Lean.Widget.UserWidget
// Imports: import Lean.Server.CodeActions import Lean.Meta.Tactic.ExposeNames public import Lean.Widget.UserWidget meta import Lean.Widget.UserWidget
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -9707,16 +9707,21 @@ if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* runtime_initialize_Lean_Widget_UserWidget(uint8_t builtin);
static bool _G_meta_initialized = false;
LEAN_EXPORT lean_object* meta_initialize_Lean_Meta_Tactic_TryThis(uint8_t builtin) {
lean_object * res;
if (_G_meta_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_meta_initialized = true;
res = runtime_initialize_Lean_Widget_UserWidget(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* initialize_Lean_Server_CodeActions(uint8_t builtin);
lean_object* initialize_Lean_Meta_Tactic_ExposeNames(uint8_t builtin);
lean_object* initialize_Lean_Widget_UserWidget(uint8_t builtin);
lean_object* initialize_Lean_Widget_UserWidget(uint8_t builtin);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Meta_Tactic_TryThis(uint8_t builtin) {
lean_object * res;
@ -9731,6 +9736,9 @@ lean_dec_ref(res);
res = initialize_Lean_Widget_UserWidget(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Widget_UserWidget(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_Meta_Tactic_TryThis(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

18
stage0/stdlib/Lean/Parser/Command.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Parser.Command
// Imports: public import Lean.Parser.Do import Lean.DocString.Parser
// Imports: public import Lean.Parser.Do import Lean.DocString.Parser meta import Lean.Parser.Do meta import Lean.DocString.Parser
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -38900,15 +38900,25 @@ if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* runtime_initialize_Lean_Parser_Do(uint8_t builtin);
lean_object* runtime_initialize_Lean_DocString_Parser(uint8_t builtin);
static bool _G_meta_initialized = false;
LEAN_EXPORT lean_object* meta_initialize_Lean_Parser_Command(uint8_t builtin) {
lean_object * res;
if (_G_meta_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_meta_initialized = true;
res = runtime_initialize_Lean_Parser_Do(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_DocString_Parser(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* initialize_Lean_Parser_Do(uint8_t builtin);
lean_object* initialize_Lean_DocString_Parser(uint8_t builtin);
lean_object* initialize_Lean_Parser_Do(uint8_t builtin);
lean_object* initialize_Lean_DocString_Parser(uint8_t builtin);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Parser_Command(uint8_t builtin) {
lean_object * res;
@ -38920,6 +38930,12 @@ lean_dec_ref(res);
res = initialize_Lean_DocString_Parser(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Parser_Do(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_DocString_Parser(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_Parser_Command(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

12
stage0/stdlib/Lean/Parser/Module.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Parser.Module
// Imports: public import Lean.Parser.Module.Syntax meta import Lean.Parser.Module.Syntax import Init.While
// Imports: public import Lean.Parser.Module.Syntax meta import Lean.Parser.Module.Syntax import Init.While meta import Lean.Parser.Extra
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -326,7 +326,7 @@ _start:
lean_object* v___x_8_; lean_object* v___x_9_; lean_object* v___x_10_; lean_object* v___x_11_; lean_object* v___x_12_; lean_object* v___x_13_;
v___x_8_ = ((lean_object*)(l_Lean_Parser_Module_updateTokens___closed__2));
v___x_9_ = lean_unsigned_to_nat(26u);
v___x_10_ = lean_unsigned_to_nat(23u);
v___x_10_ = lean_unsigned_to_nat(24u);
v___x_11_ = ((lean_object*)(l_Lean_Parser_Module_updateTokens___closed__1));
v___x_12_ = ((lean_object*)(l_Lean_Parser_Module_updateTokens___closed__0));
v___x_13_ = l_mkPanicMessageWithDecl(v___x_12_, v___x_11_, v___x_10_, v___x_9_, v___x_8_);
@ -4441,6 +4441,7 @@ lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* runtime_initialize_Lean_Parser_Module_Syntax(uint8_t builtin);
lean_object* runtime_initialize_Lean_Parser_Extra(uint8_t builtin);
static bool _G_meta_initialized = false;
LEAN_EXPORT lean_object* meta_initialize_Lean_Parser_Module(uint8_t builtin) {
lean_object * res;
@ -4449,11 +4450,15 @@ _G_meta_initialized = true;
res = runtime_initialize_Lean_Parser_Module_Syntax(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_Parser_Extra(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* initialize_Lean_Parser_Module_Syntax(uint8_t builtin);
lean_object* initialize_Lean_Parser_Module_Syntax(uint8_t builtin);
lean_object* initialize_Init_While(uint8_t builtin);
lean_object* initialize_Lean_Parser_Extra(uint8_t builtin);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Parser_Module(uint8_t builtin) {
lean_object * res;
@ -4468,6 +4473,9 @@ lean_dec_ref(res);
res = initialize_Init_While(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Parser_Extra(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_Parser_Module(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

10
stage0/stdlib/Lean/Parser/Term/Basic.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Parser.Term.Basic
// Imports: public import Lean.Parser.Attr public import Lean.Parser.Level public import Lean.Parser.Term.Doc
// Imports: public import Lean.Parser.Attr public import Lean.Parser.Level public import Lean.Parser.Term.Doc meta import Lean.Parser.Basic
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -7855,11 +7855,15 @@ l_Lean_Parser_Term_structInstField = _init_l_Lean_Parser_Term_structInstField();
lean_mark_persistent(l_Lean_Parser_Term_structInstField);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* runtime_initialize_Lean_Parser_Basic(uint8_t builtin);
static bool _G_meta_initialized = false;
LEAN_EXPORT lean_object* meta_initialize_Lean_Parser_Term_Basic(uint8_t builtin) {
lean_object * res;
if (_G_meta_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_meta_initialized = true;
res = runtime_initialize_Lean_Parser_Basic(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___private_Lean_Parser_Term_Basic_0__Lean_Parser_Term_binderDefaultM = _init_l___private_Lean_Parser_Term_Basic_0__Lean_Parser_Term_binderDefaultM();
lean_mark_persistent(l___private_Lean_Parser_Term_Basic_0__Lean_Parser_Term_binderDefaultM);
return lean_io_result_mk_ok(lean_box(0));
@ -7867,6 +7871,7 @@ return lean_io_result_mk_ok(lean_box(0));
lean_object* initialize_Lean_Parser_Attr(uint8_t builtin);
lean_object* initialize_Lean_Parser_Level(uint8_t builtin);
lean_object* initialize_Lean_Parser_Term_Doc(uint8_t builtin);
lean_object* initialize_Lean_Parser_Basic(uint8_t builtin);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Parser_Term_Basic(uint8_t builtin) {
lean_object * res;
@ -7881,6 +7886,9 @@ lean_dec_ref(res);
res = initialize_Lean_Parser_Term_Doc(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Parser_Basic(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_Parser_Term_Basic(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

7663
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c generated
View file

File diff suppressed because it is too large Load diff

382
stage0/stdlib/Lean/PrettyPrinter/Delaborator/DeclWithSig.c generated Normal file
View file

@ -0,0 +1,382 @@
// Lean compiler output
// Module: Lean.PrettyPrinter.Delaborator.DeclWithSig
// Imports: public import Lean.Parser.Types import Lean.Parser.Command
#include <lean/lean.h>
#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
lean_object* l_Lean_Name_mkStr4(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAntiquot_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_declSig_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_maxPrec;
lean_object* l_Lean_Parser_termParser_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_andthen_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_leadingNode_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_orelse_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_declSig_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_termParser_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute;
lean_object* l_Lean_Name_mkStr5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_withAntiquot_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___redArg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PrettyPrinter_formatterAttribute;
lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t, uint8_t);
lean_object* l_Lean_Parser_termParser(lean_object*);
extern lean_object* l_Lean_Parser_Command_declSig;
lean_object* l_Lean_Parser_andthen(lean_object*, lean_object*);
lean_object* l_Lean_Parser_leadingNode(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_withAntiquot(lean_object*, lean_object*);
lean_object* l_Lean_Parser_withCache(lean_object*, lean_object*);
static const lean_string_object l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 5, .m_capacity = 5, .m_length = 4, .m_data = "Lean"};
static const lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__0 = (const lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__0_value;
static const lean_string_object l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 14, .m_capacity = 14, .m_length = 13, .m_data = "PrettyPrinter"};
static const lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__1 = (const lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__1_value;
static const lean_string_object l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 12, .m_capacity = 12, .m_length = 11, .m_data = "Delaborator"};
static const lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__2 = (const lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__2_value;
static const lean_string_object l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__3_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 14, .m_capacity = 14, .m_length = 13, .m_data = "declSigWithId"};
static const lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__3 = (const lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__3_value;
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4_value_aux_0 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)(((size_t)(0) << 1) | 1)),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__0_value),LEAN_SCALAR_PTR_LITERAL(70, 193, 83, 126, 233, 67, 208, 165)}};
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4_value_aux_1 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4_value_aux_0),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__1_value),LEAN_SCALAR_PTR_LITERAL(120, 167, 117, 148, 131, 202, 42, 4)}};
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4_value_aux_2 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4_value_aux_1),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__2_value),LEAN_SCALAR_PTR_LITERAL(79, 126, 247, 124, 241, 28, 11, 244)}};
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4_value_aux_2),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__3_value),LEAN_SCALAR_PTR_LITERAL(125, 120, 113, 218, 19, 40, 2, 236)}};
static const lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4 = (const lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4_value;
static const lean_closure_object l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__5_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_closure_object) + sizeof(void*)*4, .m_other = 0, .m_tag = 245}, .m_fun = (void*)l_Lean_Parser_mkAntiquot_formatter___boxed, .m_arity = 9, .m_num_fixed = 4, .m_objs = {((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__3_value),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4_value),((lean_object*)(((size_t)(1) << 1) | 1)),((lean_object*)(((size_t)(0) << 1) | 1))} };
static const lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__5 = (const lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__5_value;
static lean_once_cell_t l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__6_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__6;
static const lean_closure_object l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__7_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_closure_object) + sizeof(void*)*0, .m_other = 0, .m_tag = 245}, .m_fun = (void*)l_Lean_Parser_Command_declSig_formatter___boxed, .m_arity = 5, .m_num_fixed = 0, .m_objs = {} };
static const lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__7 = (const lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__7_value;
static lean_once_cell_t l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__8_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__8;
static lean_once_cell_t l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__9_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__9;
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static const lean_string_object l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 10, .m_capacity = 10, .m_length = 9, .m_data = "formatter"};
static const lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__0 = (const lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__0_value;
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__1_value_aux_0 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)(((size_t)(0) << 1) | 1)),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__0_value),LEAN_SCALAR_PTR_LITERAL(70, 193, 83, 126, 233, 67, 208, 165)}};
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__1_value_aux_1 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__1_value_aux_0),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__1_value),LEAN_SCALAR_PTR_LITERAL(120, 167, 117, 148, 131, 202, 42, 4)}};
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__1_value_aux_2 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__1_value_aux_1),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__2_value),LEAN_SCALAR_PTR_LITERAL(79, 126, 247, 124, 241, 28, 11, 244)}};
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__1_value_aux_3 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__1_value_aux_2),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__3_value),LEAN_SCALAR_PTR_LITERAL(125, 120, 113, 218, 19, 40, 2, 236)}};
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__1_value_aux_3),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__0_value),LEAN_SCALAR_PTR_LITERAL(192, 11, 240, 161, 120, 65, 104, 126)}};
static const lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__1 = (const lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__1_value;
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3();
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___boxed(lean_object*);
static const lean_closure_object l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_closure_object) + sizeof(void*)*4, .m_other = 0, .m_tag = 245}, .m_fun = (void*)l_Lean_Parser_mkAntiquot_parenthesizer___boxed, .m_arity = 9, .m_num_fixed = 4, .m_objs = {((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__3_value),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4_value),((lean_object*)(((size_t)(1) << 1) | 1)),((lean_object*)(((size_t)(0) << 1) | 1))} };
static const lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__0 = (const lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__0_value;
static lean_once_cell_t l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__1_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__1;
static const lean_closure_object l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__2_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_closure_object) + sizeof(void*)*0, .m_other = 0, .m_tag = 245}, .m_fun = (void*)l_Lean_Parser_Command_declSig_parenthesizer___boxed, .m_arity = 5, .m_num_fixed = 0, .m_objs = {} };
static const lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__2 = (const lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__2_value;
static lean_once_cell_t l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__3_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__3;
static lean_once_cell_t l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__4_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__4;
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static const lean_string_object l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 14, .m_capacity = 14, .m_length = 13, .m_data = "parenthesizer"};
static const lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__0 = (const lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__0_value;
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__1_value_aux_0 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)(((size_t)(0) << 1) | 1)),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__0_value),LEAN_SCALAR_PTR_LITERAL(70, 193, 83, 126, 233, 67, 208, 165)}};
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__1_value_aux_1 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__1_value_aux_0),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__1_value),LEAN_SCALAR_PTR_LITERAL(120, 167, 117, 148, 131, 202, 42, 4)}};
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__1_value_aux_2 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__1_value_aux_1),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__2_value),LEAN_SCALAR_PTR_LITERAL(79, 126, 247, 124, 241, 28, 11, 244)}};
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__1_value_aux_3 = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__1_value_aux_2),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__3_value),LEAN_SCALAR_PTR_LITERAL(125, 120, 113, 218, 19, 40, 2, 236)}};
static const lean_ctor_object l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__1_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__1_value_aux_3),((lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__0_value),LEAN_SCALAR_PTR_LITERAL(156, 108, 232, 98, 107, 255, 86, 176)}};
static const lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__1 = (const lean_object*)&l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__1_value;
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7();
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___boxed(lean_object*);
static lean_once_cell_t l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__0_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__0;
static lean_once_cell_t l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__1_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__1;
static lean_once_cell_t l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__2_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__2;
static lean_once_cell_t l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__3_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__3;
static lean_once_cell_t l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__4_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__4;
static lean_once_cell_t l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__5_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__5;
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId;
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__6(void){
_start:
{
lean_object* v___x_17_; lean_object* v___x_18_;
v___x_17_ = l_Lean_Parser_maxPrec;
v___x_18_ = lean_alloc_closure((void*)(l_Lean_Parser_termParser_formatter___boxed), 6, 1);
lean_closure_set(v___x_18_, 0, v___x_17_);
return v___x_18_;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__8(void){
_start:
{
lean_object* v___x_20_; lean_object* v___x_21_; lean_object* v___x_22_;
v___x_20_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__7));
v___x_21_ = lean_obj_once(&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__6, &l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__6_once, _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__6);
v___x_22_ = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter___boxed), 7, 2);
lean_closure_set(v___x_22_, 0, v___x_21_);
lean_closure_set(v___x_22_, 1, v___x_20_);
return v___x_22_;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__9(void){
_start:
{
lean_object* v___x_23_; lean_object* v___x_24_; lean_object* v___x_25_; lean_object* v___x_26_;
v___x_23_ = lean_obj_once(&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__8, &l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__8_once, _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__8);
v___x_24_ = lean_unsigned_to_nat(1024u);
v___x_25_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4));
v___x_26_ = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(v___x_26_, 0, v___x_25_);
lean_closure_set(v___x_26_, 1, v___x_24_);
lean_closure_set(v___x_26_, 2, v___x_23_);
return v___x_26_;
}
}
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter(lean_object* v_a_27_, lean_object* v_a_28_, lean_object* v_a_29_, lean_object* v_a_30_){
_start:
{
lean_object* v___x_32_; lean_object* v___x_33_; lean_object* v___x_34_;
v___x_32_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__5));
v___x_33_ = lean_obj_once(&l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__9, &l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__9_once, _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__9);
v___x_34_ = l_Lean_PrettyPrinter_Formatter_orelse_formatter(v___x_32_, v___x_33_, v_a_27_, v_a_28_, v_a_29_, v_a_30_);
return v___x_34_;
}
}
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___boxed(lean_object* v_a_35_, lean_object* v_a_36_, lean_object* v_a_37_, lean_object* v_a_38_, lean_object* v_a_39_){
_start:
{
lean_object* v_res_40_;
v_res_40_ = l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter(v_a_35_, v_a_36_, v_a_37_, v_a_38_);
return v_res_40_;
}
}
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3(){
_start:
{
lean_object* v___x_49_; lean_object* v___x_50_; lean_object* v___x_51_; lean_object* v___x_52_; lean_object* v___x_53_;
v___x_49_ = l_Lean_PrettyPrinter_formatterAttribute;
v___x_50_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4));
v___x_51_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___closed__1));
v___x_52_ = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___boxed), 5, 0);
v___x_53_ = l_Lean_KeyedDeclsAttribute_addBuiltin___redArg(v___x_49_, v___x_50_, v___x_51_, v___x_52_);
return v___x_53_;
}
}
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3___boxed(lean_object* v_a_54_){
_start:
{
lean_object* v_res_55_;
v_res_55_ = l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3();
return v_res_55_;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__1(void){
_start:
{
lean_object* v___x_63_; lean_object* v___x_64_;
v___x_63_ = l_Lean_Parser_maxPrec;
v___x_64_ = lean_alloc_closure((void*)(l_Lean_Parser_termParser_parenthesizer___boxed), 6, 1);
lean_closure_set(v___x_64_, 0, v___x_63_);
return v___x_64_;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__3(void){
_start:
{
lean_object* v___x_66_; lean_object* v___x_67_; lean_object* v___x_68_;
v___x_66_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__2));
v___x_67_ = lean_obj_once(&l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__1, &l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__1_once, _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__1);
v___x_68_ = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer___boxed), 7, 2);
lean_closure_set(v___x_68_, 0, v___x_67_);
lean_closure_set(v___x_68_, 1, v___x_66_);
return v___x_68_;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__4(void){
_start:
{
lean_object* v___x_69_; lean_object* v___x_70_; lean_object* v___x_71_; lean_object* v___x_72_;
v___x_69_ = lean_obj_once(&l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__3, &l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__3_once, _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__3);
v___x_70_ = lean_unsigned_to_nat(1024u);
v___x_71_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4));
v___x_72_ = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(v___x_72_, 0, v___x_71_);
lean_closure_set(v___x_72_, 1, v___x_70_);
lean_closure_set(v___x_72_, 2, v___x_69_);
return v___x_72_;
}
}
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer(lean_object* v_a_73_, lean_object* v_a_74_, lean_object* v_a_75_, lean_object* v_a_76_){
_start:
{
lean_object* v___x_78_; lean_object* v___x_79_; lean_object* v___x_80_;
v___x_78_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__0));
v___x_79_ = lean_obj_once(&l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__4, &l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__4_once, _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___closed__4);
v___x_80_ = l_Lean_PrettyPrinter_Parenthesizer_withAntiquot_parenthesizer(v___x_78_, v___x_79_, v_a_73_, v_a_74_, v_a_75_, v_a_76_);
return v___x_80_;
}
}
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___boxed(lean_object* v_a_81_, lean_object* v_a_82_, lean_object* v_a_83_, lean_object* v_a_84_, lean_object* v_a_85_){
_start:
{
lean_object* v_res_86_;
v_res_86_ = l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer(v_a_81_, v_a_82_, v_a_83_, v_a_84_);
return v_res_86_;
}
}
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7(){
_start:
{
lean_object* v___x_95_; lean_object* v___x_96_; lean_object* v___x_97_; lean_object* v___x_98_; lean_object* v___x_99_;
v___x_95_ = l_Lean_PrettyPrinter_parenthesizerAttribute;
v___x_96_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4));
v___x_97_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___closed__1));
v___x_98_ = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer___boxed), 5, 0);
v___x_99_ = l_Lean_KeyedDeclsAttribute_addBuiltin___redArg(v___x_95_, v___x_96_, v___x_97_, v___x_98_);
return v___x_99_;
}
}
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7___boxed(lean_object* v_a_100_){
_start:
{
lean_object* v_res_101_;
v_res_101_ = l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7();
return v_res_101_;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__0(void){
_start:
{
uint8_t v___x_102_; uint8_t v___x_103_; lean_object* v___x_104_; lean_object* v___x_105_; lean_object* v___x_106_;
v___x_102_ = 0;
v___x_103_ = 1;
v___x_104_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4));
v___x_105_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__3));
v___x_106_ = l_Lean_Parser_mkAntiquot(v___x_105_, v___x_104_, v___x_103_, v___x_102_);
return v___x_106_;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__1(void){
_start:
{
lean_object* v___x_107_; lean_object* v___x_108_;
v___x_107_ = l_Lean_Parser_maxPrec;
v___x_108_ = l_Lean_Parser_termParser(v___x_107_);
return v___x_108_;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__2(void){
_start:
{
lean_object* v___x_109_; lean_object* v___x_110_; lean_object* v___x_111_;
v___x_109_ = l_Lean_Parser_Command_declSig;
v___x_110_ = lean_obj_once(&l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__1, &l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__1_once, _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__1);
v___x_111_ = l_Lean_Parser_andthen(v___x_110_, v___x_109_);
return v___x_111_;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__3(void){
_start:
{
lean_object* v___x_112_; lean_object* v___x_113_; lean_object* v___x_114_; lean_object* v___x_115_;
v___x_112_ = lean_obj_once(&l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__2, &l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__2_once, _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__2);
v___x_113_ = lean_unsigned_to_nat(1024u);
v___x_114_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4));
v___x_115_ = l_Lean_Parser_leadingNode(v___x_114_, v___x_113_, v___x_112_);
return v___x_115_;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__4(void){
_start:
{
lean_object* v___x_116_; lean_object* v___x_117_; lean_object* v___x_118_;
v___x_116_ = lean_obj_once(&l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__3, &l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__3_once, _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__3);
v___x_117_ = lean_obj_once(&l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__0, &l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__0_once, _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__0);
v___x_118_ = l_Lean_Parser_withAntiquot(v___x_117_, v___x_116_);
return v___x_118_;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__5(void){
_start:
{
lean_object* v___x_119_; lean_object* v___x_120_; lean_object* v___x_121_;
v___x_119_ = lean_obj_once(&l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__4, &l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__4_once, _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__4);
v___x_120_ = ((lean_object*)(l_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter___closed__4));
v___x_121_ = l_Lean_Parser_withCache(v___x_120_, v___x_119_);
return v___x_121_;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId(void){
_start:
{
lean_object* v___x_122_;
v___x_122_ = lean_obj_once(&l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__5, &l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__5_once, _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId___closed__5);
return v___x_122_;
}
}
lean_object* runtime_initialize_Lean_Parser_Types(uint8_t builtin);
lean_object* runtime_initialize_Lean_Parser_Command(uint8_t builtin);
static bool _G_runtime_initialized = false;
LEAN_EXPORT lean_object* runtime_initialize_Lean_PrettyPrinter_Delaborator_DeclWithSig(uint8_t builtin) {
lean_object * res;
if (_G_runtime_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_runtime_initialized = true;
res = runtime_initialize_Lean_Parser_Types(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_Parser_Command(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_formatter__3();
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = l_Lean_PrettyPrinter_Delaborator_declSigWithId___regBuiltin_Lean_PrettyPrinter_Delaborator_declSigWithId_parenthesizer__7();
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_PrettyPrinter_Delaborator_declSigWithId = _init_l_Lean_PrettyPrinter_Delaborator_declSigWithId();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_declSigWithId);
return lean_io_result_mk_ok(lean_box(0));
}
static bool _G_meta_initialized = false;
LEAN_EXPORT lean_object* meta_initialize_Lean_PrettyPrinter_Delaborator_DeclWithSig(uint8_t builtin) {
lean_object * res;
if (_G_meta_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_meta_initialized = true;
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* initialize_Lean_Parser_Types(uint8_t builtin);
lean_object* initialize_Lean_Parser_Command(uint8_t builtin);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_PrettyPrinter_Delaborator_DeclWithSig(uint8_t builtin) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Lean_Parser_Types(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Parser_Command(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_Lean_PrettyPrinter_Delaborator_DeclWithSig(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = meta_initialize_Lean_PrettyPrinter_Delaborator_DeclWithSig(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return initialize_Lean_PrettyPrinter_Delaborator_DeclWithSig(builtin);
}
#ifdef __cplusplus
}
#endif

734
stage0/stdlib/Lean/Server/Rpc/RequestHandling.c generated
View file

@ -93,7 +93,9 @@ lean_object* l_Lean_instantiateMVarsCore(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withoutErrToSorryImp___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_TermElabM_run___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_append(lean_object*, lean_object*);
lean_object* l_Lean_addAndCompile(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_addDecl(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_markMeta(lean_object*, lean_object*);
lean_object* l_Lean_compileDecl(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_MapDeclarationExtension_insert___redArg(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_MapDeclarationExtension_contains___redArg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
@ -394,18 +396,20 @@ static const lean_string_object l_Lean_Server_registerRpcProcedure___closed__13_
static const lean_object* l_Lean_Server_registerRpcProcedure___closed__13 = (const lean_object*)&l_Lean_Server_registerRpcProcedure___closed__13_value;
static const lean_ctor_object l_Lean_Server_registerRpcProcedure___closed__14_value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_ctor_object) + sizeof(void*)*2 + 8, .m_other = 2, .m_tag = 1}, .m_objs = {((lean_object*)(((size_t)(0) << 1) | 1)),((lean_object*)&l_Lean_Server_registerRpcProcedure___closed__13_value),LEAN_SCALAR_PTR_LITERAL(76, 241, 252, 252, 247, 5, 133, 205)}};
static const lean_object* l_Lean_Server_registerRpcProcedure___closed__14 = (const lean_object*)&l_Lean_Server_registerRpcProcedure___closed__14_value;
static const lean_string_object l_Lean_Server_registerRpcProcedure___closed__15_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 42, .m_capacity = 42, .m_length = 41, .m_data = "Failed to register RPC call handler for '"};
static const lean_object* l_Lean_Server_registerRpcProcedure___closed__15 = (const lean_object*)&l_Lean_Server_registerRpcProcedure___closed__15_value;
static lean_once_cell_t l_Lean_Server_registerRpcProcedure___closed__16_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_Server_registerRpcProcedure___closed__16;
static lean_once_cell_t l_Lean_Server_registerRpcProcedure___closed__15_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_Server_registerRpcProcedure___closed__15;
static const lean_string_object l_Lean_Server_registerRpcProcedure___closed__16_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 42, .m_capacity = 42, .m_length = 41, .m_data = "Failed to register RPC call handler for '"};
static const lean_object* l_Lean_Server_registerRpcProcedure___closed__16 = (const lean_object*)&l_Lean_Server_registerRpcProcedure___closed__16_value;
static lean_once_cell_t l_Lean_Server_registerRpcProcedure___closed__17_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_Server_registerRpcProcedure___closed__17;
static lean_once_cell_t l_Lean_Server_registerRpcProcedure___closed__18_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_Server_registerRpcProcedure___closed__18;
static const lean_string_object l_Lean_Server_registerRpcProcedure___closed__19_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 31, .m_capacity = 31, .m_length = 30, .m_data = ": already registered (builtin)"};
static const lean_object* l_Lean_Server_registerRpcProcedure___closed__19 = (const lean_object*)&l_Lean_Server_registerRpcProcedure___closed__19_value;
static lean_once_cell_t l_Lean_Server_registerRpcProcedure___closed__20_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_Server_registerRpcProcedure___closed__20;
static lean_once_cell_t l_Lean_Server_registerRpcProcedure___closed__19_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_Server_registerRpcProcedure___closed__19;
static const lean_string_object l_Lean_Server_registerRpcProcedure___closed__20_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 31, .m_capacity = 31, .m_length = 30, .m_data = ": already registered (builtin)"};
static const lean_object* l_Lean_Server_registerRpcProcedure___closed__20 = (const lean_object*)&l_Lean_Server_registerRpcProcedure___closed__20_value;
static lean_once_cell_t l_Lean_Server_registerRpcProcedure___closed__21_once = LEAN_ONCE_CELL_INITIALIZER;
static lean_object* l_Lean_Server_registerRpcProcedure___closed__21;
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcProcedure(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcProcedure___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
@ -4279,10 +4283,10 @@ return v___x_1408_;
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcProcedure___lam__1___boxed(lean_object* v___x_1411_, lean_object* v___x_1412_, lean_object* v___x_1413_, lean_object* v_method_1414_, lean_object* v___x_1415_, lean_object* v___x_1416_, lean_object* v___y_1417_, lean_object* v___y_1418_, lean_object* v___y_1419_, lean_object* v___y_1420_, lean_object* v___y_1421_, lean_object* v___y_1422_, lean_object* v___y_1423_){
_start:
{
uint8_t v___x_5388__boxed_1424_; uint8_t v___x_5392__boxed_1425_; lean_object* v_res_1426_;
v___x_5388__boxed_1424_ = lean_unbox(v___x_1411_);
v___x_5392__boxed_1425_ = lean_unbox(v___x_1416_);
v_res_1426_ = l_Lean_Server_registerRpcProcedure___lam__1(v___x_5388__boxed_1424_, v___x_1412_, v___x_1413_, v_method_1414_, v___x_1415_, v___x_5392__boxed_1425_, v___y_1417_, v___y_1418_, v___y_1419_, v___y_1420_, v___y_1421_, v___y_1422_);
uint8_t v___x_5837__boxed_1424_; uint8_t v___x_5841__boxed_1425_; lean_object* v_res_1426_;
v___x_5837__boxed_1424_ = lean_unbox(v___x_1411_);
v___x_5841__boxed_1425_ = lean_unbox(v___x_1416_);
v_res_1426_ = l_Lean_Server_registerRpcProcedure___lam__1(v___x_5837__boxed_1424_, v___x_1412_, v___x_1413_, v_method_1414_, v___x_1415_, v___x_5841__boxed_1425_, v___y_1417_, v___y_1418_, v___y_1419_, v___y_1420_, v___y_1421_, v___y_1422_);
return v_res_1426_;
}
}
@ -4597,20 +4601,22 @@ v___x_1525_ = l_Lean_mkConst(v___x_1524_, v___x_1523_);
return v___x_1525_;
}
}
static lean_object* _init_l_Lean_Server_registerRpcProcedure___closed__16(void){
static lean_object* _init_l_Lean_Server_registerRpcProcedure___closed__15(void){
_start:
{
lean_object* v___x_1533_; lean_object* v___x_1534_;
v___x_1533_ = ((lean_object*)(l_Lean_Server_registerRpcProcedure___closed__15));
v___x_1534_ = l_Lean_stringToMessageData(v___x_1533_);
return v___x_1534_;
lean_object* v___x_1532_; lean_object* v___x_1533_;
v___x_1532_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__4, &l_Lean_Server_registerRpcProcedure___closed__4_once, _init_l_Lean_Server_registerRpcProcedure___closed__4);
v___x_1533_ = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(v___x_1533_, 0, v___x_1532_);
lean_ctor_set(v___x_1533_, 1, v___x_1532_);
return v___x_1533_;
}
}
static lean_object* _init_l_Lean_Server_registerRpcProcedure___closed__17(void){
_start:
{
lean_object* v___x_1535_; lean_object* v___x_1536_;
v___x_1535_ = ((lean_object*)(l_Lean_Server_registerBuiltinRpcProcedure___redArg___closed__1));
v___x_1535_ = ((lean_object*)(l_Lean_Server_registerRpcProcedure___closed__16));
v___x_1536_ = l_Lean_stringToMessageData(v___x_1535_);
return v___x_1536_;
}
@ -4619,385 +4625,481 @@ static lean_object* _init_l_Lean_Server_registerRpcProcedure___closed__18(void){
_start:
{
lean_object* v___x_1537_; lean_object* v___x_1538_;
v___x_1537_ = ((lean_object*)(l_Lean_Server_registerBuiltinRpcProcedure___redArg___closed__5));
v___x_1537_ = ((lean_object*)(l_Lean_Server_registerBuiltinRpcProcedure___redArg___closed__1));
v___x_1538_ = l_Lean_stringToMessageData(v___x_1537_);
return v___x_1538_;
}
}
static lean_object* _init_l_Lean_Server_registerRpcProcedure___closed__20(void){
static lean_object* _init_l_Lean_Server_registerRpcProcedure___closed__19(void){
_start:
{
lean_object* v___x_1540_; lean_object* v___x_1541_;
v___x_1540_ = ((lean_object*)(l_Lean_Server_registerRpcProcedure___closed__19));
v___x_1541_ = l_Lean_stringToMessageData(v___x_1540_);
return v___x_1541_;
lean_object* v___x_1539_; lean_object* v___x_1540_;
v___x_1539_ = ((lean_object*)(l_Lean_Server_registerBuiltinRpcProcedure___redArg___closed__5));
v___x_1540_ = l_Lean_stringToMessageData(v___x_1539_);
return v___x_1540_;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcProcedure(lean_object* v_method_1542_, lean_object* v_a_1543_, lean_object* v_a_1544_){
static lean_object* _init_l_Lean_Server_registerRpcProcedure___closed__21(void){
_start:
{
lean_object* v___x_1546_; lean_object* v___x_1547_; lean_object* v___x_1548_; lean_object* v_env_1549_; lean_object* v___y_1551_; lean_object* v___y_1552_; lean_object* v___x_1601_; lean_object* v___x_1602_; lean_object* v___x_1603_; lean_object* v___x_1604_; lean_object* v___x_1605_; lean_object* v___x_1606_; lean_object* v___y_1608_; lean_object* v___y_1609_; uint8_t v___x_1615_;
v___x_1546_ = lean_st_ref_get(v_a_1544_);
v___x_1547_ = l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_builtinRpcProcedures;
v___x_1548_ = lean_st_ref_get(v___x_1547_);
v_env_1549_ = lean_ctor_get(v___x_1546_, 0);
lean_inc_ref(v_env_1549_);
lean_dec(v___x_1546_);
v___x_1601_ = lean_box(0);
v___x_1602_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__16, &l_Lean_Server_registerRpcProcedure___closed__16_once, _init_l_Lean_Server_registerRpcProcedure___closed__16);
lean_inc(v_method_1542_);
v___x_1603_ = l_Lean_MessageData_ofName(v_method_1542_);
v___x_1604_ = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(v___x_1604_, 0, v___x_1602_);
lean_ctor_set(v___x_1604_, 1, v___x_1603_);
v___x_1605_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__17, &l_Lean_Server_registerRpcProcedure___closed__17_once, _init_l_Lean_Server_registerRpcProcedure___closed__17);
v___x_1606_ = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(v___x_1606_, 0, v___x_1604_);
lean_ctor_set(v___x_1606_, 1, v___x_1605_);
v___x_1615_ = l_Lean_PersistentHashMap_contains___at___00Lean_Server_existsBuiltinRpcProcedure_spec__0___redArg(v___x_1548_, v_method_1542_);
if (v___x_1615_ == 0)
lean_object* v___x_1542_; lean_object* v___x_1543_;
v___x_1542_ = ((lean_object*)(l_Lean_Server_registerRpcProcedure___closed__20));
v___x_1543_ = l_Lean_stringToMessageData(v___x_1542_);
return v___x_1543_;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcProcedure(lean_object* v_method_1544_, lean_object* v_a_1545_, lean_object* v_a_1546_){
_start:
{
v___y_1608_ = v_a_1543_;
v___y_1609_ = v_a_1544_;
goto v___jp_1607_;
lean_object* v___x_1548_; lean_object* v___x_1549_; lean_object* v___x_1550_; lean_object* v_env_1551_; lean_object* v___y_1553_; lean_object* v___y_1554_; lean_object* v___x_1624_; lean_object* v___x_1625_; lean_object* v___x_1626_; lean_object* v___x_1627_; lean_object* v___x_1628_; lean_object* v___x_1629_; lean_object* v___y_1631_; lean_object* v___y_1632_; uint8_t v___x_1638_;
v___x_1548_ = lean_st_ref_get(v_a_1546_);
v___x_1549_ = l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_builtinRpcProcedures;
v___x_1550_ = lean_st_ref_get(v___x_1549_);
v_env_1551_ = lean_ctor_get(v___x_1548_, 0);
lean_inc_ref(v_env_1551_);
lean_dec(v___x_1548_);
v___x_1624_ = lean_box(0);
v___x_1625_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__17, &l_Lean_Server_registerRpcProcedure___closed__17_once, _init_l_Lean_Server_registerRpcProcedure___closed__17);
lean_inc(v_method_1544_);
v___x_1626_ = l_Lean_MessageData_ofName(v_method_1544_);
v___x_1627_ = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(v___x_1627_, 0, v___x_1625_);
lean_ctor_set(v___x_1627_, 1, v___x_1626_);
v___x_1628_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__18, &l_Lean_Server_registerRpcProcedure___closed__18_once, _init_l_Lean_Server_registerRpcProcedure___closed__18);
v___x_1629_ = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(v___x_1629_, 0, v___x_1627_);
lean_ctor_set(v___x_1629_, 1, v___x_1628_);
v___x_1638_ = l_Lean_PersistentHashMap_contains___at___00Lean_Server_existsBuiltinRpcProcedure_spec__0___redArg(v___x_1550_, v_method_1544_);
if (v___x_1638_ == 0)
{
v___y_1631_ = v_a_1545_;
v___y_1632_ = v_a_1546_;
goto v___jp_1630_;
}
else
{
lean_object* v___x_1616_; lean_object* v___x_1617_; lean_object* v___x_1618_;
lean_dec_ref(v_env_1549_);
lean_dec(v_method_1542_);
v___x_1616_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__20, &l_Lean_Server_registerRpcProcedure___closed__20_once, _init_l_Lean_Server_registerRpcProcedure___closed__20);
v___x_1617_ = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(v___x_1617_, 0, v___x_1606_);
lean_ctor_set(v___x_1617_, 1, v___x_1616_);
v___x_1618_ = l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3___redArg(v___x_1617_, v_a_1543_, v_a_1544_);
lean_dec(v_a_1544_);
lean_dec_ref(v_a_1543_);
return v___x_1618_;
lean_object* v___x_1639_; lean_object* v___x_1640_; lean_object* v___x_1641_;
lean_dec_ref(v_env_1551_);
lean_dec(v_method_1544_);
v___x_1639_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__21, &l_Lean_Server_registerRpcProcedure___closed__21_once, _init_l_Lean_Server_registerRpcProcedure___closed__21);
v___x_1640_ = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(v___x_1640_, 0, v___x_1629_);
lean_ctor_set(v___x_1640_, 1, v___x_1639_);
v___x_1641_ = l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3___redArg(v___x_1640_, v_a_1545_, v_a_1546_);
lean_dec(v_a_1546_);
lean_dec_ref(v_a_1545_);
return v___x_1641_;
}
v___jp_1550_:
v___jp_1552_:
{
lean_object* v___x_1553_; uint8_t v___x_1554_; uint8_t v___x_1555_; lean_object* v___x_1556_; lean_object* v___x_1557_; lean_object* v___x_1558_; lean_object* v___x_1559_; lean_object* v___x_1560_; lean_object* v___x_1561_; lean_object* v___x_1562_; lean_object* v___x_1563_; lean_object* v___x_1564_; lean_object* v___f_1565_; lean_object* v___x_1566_; lean_object* v___x_1567_; lean_object* v___x_1568_;
v___x_1553_ = lean_box(0);
v___x_1554_ = 1;
v___x_1555_ = 0;
v___x_1556_ = ((lean_object*)(l_Lean_Server_registerRpcProcedure___closed__2));
v___x_1557_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__6, &l_Lean_Server_registerRpcProcedure___closed__6_once, _init_l_Lean_Server_registerRpcProcedure___closed__6);
v___x_1558_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__10, &l_Lean_Server_registerRpcProcedure___closed__10_once, _init_l_Lean_Server_registerRpcProcedure___closed__10);
v___x_1559_ = lean_st_mk_ref(v___x_1558_);
v___x_1560_ = ((lean_object*)(l_Lean_Server_initFn___closed__1_00___x40_Lean_Server_Rpc_RequestHandling_2946836025____hygCtx___hyg_2_));
v___x_1561_ = ((lean_object*)(l_Lean_Server_initFn___closed__2_00___x40_Lean_Server_Rpc_RequestHandling_2946836025____hygCtx___hyg_2_));
v___x_1562_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__11, &l_Lean_Server_registerRpcProcedure___closed__11_once, _init_l_Lean_Server_registerRpcProcedure___closed__11);
v___x_1563_ = lean_box(v___x_1555_);
v___x_1564_ = lean_box(v___x_1554_);
lean_inc(v_method_1542_);
v___f_1565_ = lean_alloc_closure((void*)(l_Lean_Server_registerRpcProcedure___lam__1___boxed), 13, 6);
lean_closure_set(v___f_1565_, 0, v___x_1563_);
lean_closure_set(v___f_1565_, 1, v___x_1560_);
lean_closure_set(v___f_1565_, 2, v___x_1561_);
lean_closure_set(v___f_1565_, 3, v_method_1542_);
lean_closure_set(v___f_1565_, 4, v___x_1562_);
lean_closure_set(v___f_1565_, 5, v___x_1564_);
v___x_1566_ = lean_alloc_closure((void*)(l_Lean_Elab_Term_withoutErrToSorry___at___00Lean_Server_registerRpcProcedure_spec__1___boxed), 9, 2);
lean_closure_set(v___x_1566_, 0, lean_box(0));
lean_closure_set(v___x_1566_, 1, v___f_1565_);
v___x_1567_ = ((lean_object*)(l_Lean_Server_registerRpcProcedure___closed__12));
lean_inc(v___y_1552_);
lean_inc_ref(v___y_1551_);
lean_inc(v___x_1559_);
v___x_1568_ = l_Lean_Elab_Term_TermElabM_run___redArg(v___x_1566_, v___x_1556_, v___x_1567_, v___x_1557_, v___x_1559_, v___y_1551_, v___y_1552_);
if (lean_obj_tag(v___x_1568_) == 0)
lean_object* v___x_1555_; uint8_t v___x_1556_; uint8_t v___x_1557_; lean_object* v___x_1558_; lean_object* v___x_1559_; lean_object* v___x_1560_; lean_object* v___x_1561_; lean_object* v___x_1562_; lean_object* v___x_1563_; lean_object* v___x_1564_; lean_object* v___x_1565_; lean_object* v___x_1566_; lean_object* v___f_1567_; lean_object* v___x_1568_; lean_object* v___x_1569_; lean_object* v___x_1570_;
v___x_1555_ = lean_box(0);
v___x_1556_ = 1;
v___x_1557_ = 0;
v___x_1558_ = ((lean_object*)(l_Lean_Server_registerRpcProcedure___closed__2));
v___x_1559_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__6, &l_Lean_Server_registerRpcProcedure___closed__6_once, _init_l_Lean_Server_registerRpcProcedure___closed__6);
v___x_1560_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__10, &l_Lean_Server_registerRpcProcedure___closed__10_once, _init_l_Lean_Server_registerRpcProcedure___closed__10);
v___x_1561_ = lean_st_mk_ref(v___x_1560_);
v___x_1562_ = ((lean_object*)(l_Lean_Server_initFn___closed__1_00___x40_Lean_Server_Rpc_RequestHandling_2946836025____hygCtx___hyg_2_));
v___x_1563_ = ((lean_object*)(l_Lean_Server_initFn___closed__2_00___x40_Lean_Server_Rpc_RequestHandling_2946836025____hygCtx___hyg_2_));
v___x_1564_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__11, &l_Lean_Server_registerRpcProcedure___closed__11_once, _init_l_Lean_Server_registerRpcProcedure___closed__11);
v___x_1565_ = lean_box(v___x_1557_);
v___x_1566_ = lean_box(v___x_1556_);
lean_inc(v_method_1544_);
v___f_1567_ = lean_alloc_closure((void*)(l_Lean_Server_registerRpcProcedure___lam__1___boxed), 13, 6);
lean_closure_set(v___f_1567_, 0, v___x_1565_);
lean_closure_set(v___f_1567_, 1, v___x_1562_);
lean_closure_set(v___f_1567_, 2, v___x_1563_);
lean_closure_set(v___f_1567_, 3, v_method_1544_);
lean_closure_set(v___f_1567_, 4, v___x_1564_);
lean_closure_set(v___f_1567_, 5, v___x_1566_);
v___x_1568_ = lean_alloc_closure((void*)(l_Lean_Elab_Term_withoutErrToSorry___at___00Lean_Server_registerRpcProcedure_spec__1___boxed), 9, 2);
lean_closure_set(v___x_1568_, 0, lean_box(0));
lean_closure_set(v___x_1568_, 1, v___f_1567_);
v___x_1569_ = ((lean_object*)(l_Lean_Server_registerRpcProcedure___closed__12));
lean_inc(v___y_1554_);
lean_inc_ref(v___y_1553_);
lean_inc(v___x_1561_);
v___x_1570_ = l_Lean_Elab_Term_TermElabM_run___redArg(v___x_1568_, v___x_1558_, v___x_1569_, v___x_1559_, v___x_1561_, v___y_1553_, v___y_1554_);
if (lean_obj_tag(v___x_1570_) == 0)
{
lean_object* v_a_1569_; lean_object* v___x_1570_; lean_object* v_fst_1571_; lean_object* v___x_1573_; uint8_t v_isShared_1574_; uint8_t v_isSharedCheck_1591_;
v_a_1569_ = lean_ctor_get(v___x_1568_, 0);
lean_inc(v_a_1569_);
lean_dec_ref(v___x_1568_);
v___x_1570_ = lean_st_ref_get(v___x_1559_);
lean_dec(v___x_1559_);
lean_object* v_a_1571_; lean_object* v___x_1572_; lean_object* v_fst_1573_; lean_object* v___x_1575_; uint8_t v_isShared_1576_; uint8_t v_isSharedCheck_1614_;
v_a_1571_ = lean_ctor_get(v___x_1570_, 0);
lean_inc(v_a_1571_);
lean_dec_ref(v___x_1570_);
v___x_1572_ = lean_st_ref_get(v___x_1561_);
lean_dec(v___x_1561_);
lean_dec(v___x_1572_);
v_fst_1573_ = lean_ctor_get(v_a_1571_, 0);
v_isSharedCheck_1614_ = !lean_is_exclusive(v_a_1571_);
if (v_isSharedCheck_1614_ == 0)
{
lean_object* v_unused_1615_;
v_unused_1615_ = lean_ctor_get(v_a_1571_, 1);
lean_dec(v_unused_1615_);
v___x_1575_ = v_a_1571_;
v_isShared_1576_ = v_isSharedCheck_1614_;
goto v_resetjp_1574_;
}
else
{
lean_inc(v_fst_1573_);
lean_dec(v_a_1571_);
v___x_1575_ = lean_box(0);
v_isShared_1576_ = v_isSharedCheck_1614_;
goto v_resetjp_1574_;
}
v_resetjp_1574_:
{
lean_object* v___x_1577_; lean_object* v___x_1578_; lean_object* v___x_1579_; lean_object* v___x_1580_; uint8_t v___x_1581_; lean_object* v___x_1583_;
v___x_1577_ = ((lean_object*)(l_Lean_Server_registerRpcProcedure___closed__14));
lean_inc(v_method_1544_);
v___x_1578_ = l_Lean_Name_append(v_method_1544_, v___x_1577_);
lean_inc(v___x_1578_);
v___x_1579_ = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(v___x_1579_, 0, v___x_1578_);
lean_ctor_set(v___x_1579_, 1, v___x_1555_);
lean_ctor_set(v___x_1579_, 2, v___x_1564_);
v___x_1580_ = lean_box(0);
v___x_1581_ = 1;
lean_inc(v___x_1578_);
if (v_isShared_1576_ == 0)
{
lean_ctor_set_tag(v___x_1575_, 1);
lean_ctor_set(v___x_1575_, 1, v___x_1555_);
lean_ctor_set(v___x_1575_, 0, v___x_1578_);
v___x_1583_ = v___x_1575_;
goto v_reusejp_1582_;
}
else
{
lean_object* v_reuseFailAlloc_1613_;
v_reuseFailAlloc_1613_ = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(v_reuseFailAlloc_1613_, 0, v___x_1578_);
lean_ctor_set(v_reuseFailAlloc_1613_, 1, v___x_1555_);
v___x_1583_ = v_reuseFailAlloc_1613_;
goto v_reusejp_1582_;
}
v_reusejp_1582_:
{
lean_object* v___x_1584_; lean_object* v___x_1585_; lean_object* v___x_1586_;
v___x_1584_ = lean_alloc_ctor(0, 4, 1);
lean_ctor_set(v___x_1584_, 0, v___x_1579_);
lean_ctor_set(v___x_1584_, 1, v_fst_1573_);
lean_ctor_set(v___x_1584_, 2, v___x_1580_);
lean_ctor_set(v___x_1584_, 3, v___x_1583_);
lean_ctor_set_uint8(v___x_1584_, sizeof(void*)*4, v___x_1581_);
v___x_1585_ = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(v___x_1585_, 0, v___x_1584_);
lean_inc(v___y_1554_);
lean_inc_ref(v___y_1553_);
lean_inc_ref(v___x_1585_);
v___x_1586_ = l_Lean_addDecl(v___x_1585_, v___x_1557_, v___y_1553_, v___y_1554_);
if (lean_obj_tag(v___x_1586_) == 0)
{
lean_object* v___x_1587_; lean_object* v_env_1588_; lean_object* v_nextMacroScope_1589_; lean_object* v_ngen_1590_; lean_object* v_auxDeclNGen_1591_; lean_object* v_traceState_1592_; lean_object* v_messages_1593_; lean_object* v_infoState_1594_; lean_object* v_snapshotTasks_1595_; lean_object* v___x_1597_; uint8_t v_isShared_1598_; uint8_t v_isSharedCheck_1611_;
lean_dec_ref(v___x_1586_);
v___x_1587_ = lean_st_ref_take(v___y_1554_);
v_env_1588_ = lean_ctor_get(v___x_1587_, 0);
v_nextMacroScope_1589_ = lean_ctor_get(v___x_1587_, 1);
v_ngen_1590_ = lean_ctor_get(v___x_1587_, 2);
v_auxDeclNGen_1591_ = lean_ctor_get(v___x_1587_, 3);
v_traceState_1592_ = lean_ctor_get(v___x_1587_, 4);
v_messages_1593_ = lean_ctor_get(v___x_1587_, 6);
v_infoState_1594_ = lean_ctor_get(v___x_1587_, 7);
v_snapshotTasks_1595_ = lean_ctor_get(v___x_1587_, 8);
v_isSharedCheck_1611_ = !lean_is_exclusive(v___x_1587_);
if (v_isSharedCheck_1611_ == 0)
{
lean_object* v_unused_1612_;
v_unused_1612_ = lean_ctor_get(v___x_1587_, 5);
lean_dec(v_unused_1612_);
v___x_1597_ = v___x_1587_;
v_isShared_1598_ = v_isSharedCheck_1611_;
goto v_resetjp_1596_;
}
else
{
lean_inc(v_snapshotTasks_1595_);
lean_inc(v_infoState_1594_);
lean_inc(v_messages_1593_);
lean_inc(v_traceState_1592_);
lean_inc(v_auxDeclNGen_1591_);
lean_inc(v_ngen_1590_);
lean_inc(v_nextMacroScope_1589_);
lean_inc(v_env_1588_);
lean_dec(v___x_1587_);
v___x_1597_ = lean_box(0);
v_isShared_1598_ = v_isSharedCheck_1611_;
goto v_resetjp_1596_;
}
v_resetjp_1596_:
{
lean_object* v___x_1599_; lean_object* v___x_1600_; lean_object* v___x_1602_;
lean_inc(v___x_1578_);
v___x_1599_ = l_Lean_markMeta(v_env_1588_, v___x_1578_);
v___x_1600_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__15, &l_Lean_Server_registerRpcProcedure___closed__15_once, _init_l_Lean_Server_registerRpcProcedure___closed__15);
if (v_isShared_1598_ == 0)
{
lean_ctor_set(v___x_1597_, 5, v___x_1600_);
lean_ctor_set(v___x_1597_, 0, v___x_1599_);
v___x_1602_ = v___x_1597_;
goto v_reusejp_1601_;
}
else
{
lean_object* v_reuseFailAlloc_1610_;
v_reuseFailAlloc_1610_ = lean_alloc_ctor(0, 9, 0);
lean_ctor_set(v_reuseFailAlloc_1610_, 0, v___x_1599_);
lean_ctor_set(v_reuseFailAlloc_1610_, 1, v_nextMacroScope_1589_);
lean_ctor_set(v_reuseFailAlloc_1610_, 2, v_ngen_1590_);
lean_ctor_set(v_reuseFailAlloc_1610_, 3, v_auxDeclNGen_1591_);
lean_ctor_set(v_reuseFailAlloc_1610_, 4, v_traceState_1592_);
lean_ctor_set(v_reuseFailAlloc_1610_, 5, v___x_1600_);
lean_ctor_set(v_reuseFailAlloc_1610_, 6, v_messages_1593_);
lean_ctor_set(v_reuseFailAlloc_1610_, 7, v_infoState_1594_);
lean_ctor_set(v_reuseFailAlloc_1610_, 8, v_snapshotTasks_1595_);
v___x_1602_ = v_reuseFailAlloc_1610_;
goto v_reusejp_1601_;
}
v_reusejp_1601_:
{
lean_object* v___x_1603_; lean_object* v___x_1604_;
v___x_1603_ = lean_st_ref_set(v___y_1554_, v___x_1602_);
lean_inc(v___y_1554_);
v___x_1604_ = l_Lean_compileDecl(v___x_1585_, v___x_1556_, v___y_1553_, v___y_1554_);
if (lean_obj_tag(v___x_1604_) == 0)
{
lean_object* v___x_1605_; lean_object* v_env_1606_; lean_object* v___x_1607_; lean_object* v___x_1608_; lean_object* v___x_1609_;
lean_dec_ref(v___x_1604_);
v___x_1605_ = lean_st_ref_get(v___y_1554_);
v_env_1606_ = lean_ctor_get(v___x_1605_, 0);
lean_inc_ref(v_env_1606_);
lean_dec(v___x_1605_);
v___x_1607_ = l_Lean_Server_userRpcProcedures;
v___x_1608_ = l_Lean_MapDeclarationExtension_insert___redArg(v___x_1607_, v_env_1606_, v_method_1544_, v___x_1578_);
v___x_1609_ = l_Lean_setEnv___at___00Lean_Server_registerRpcProcedure_spec__2___redArg(v___x_1608_, v___y_1554_);
lean_dec(v___y_1554_);
return v___x_1609_;
}
else
{
lean_dec(v___x_1578_);
lean_dec(v___y_1554_);
lean_dec(v_method_1544_);
return v___x_1604_;
}
}
}
}
else
{
lean_dec_ref(v___x_1585_);
lean_dec(v___x_1578_);
lean_dec(v___y_1554_);
lean_dec_ref(v___y_1553_);
lean_dec(v_method_1544_);
return v___x_1586_;
}
}
}
}
else
{
lean_object* v_a_1616_; lean_object* v___x_1618_; uint8_t v_isShared_1619_; uint8_t v_isSharedCheck_1623_;
lean_dec(v___x_1561_);
lean_dec(v___y_1554_);
lean_dec_ref(v___y_1553_);
lean_dec(v_method_1544_);
v_a_1616_ = lean_ctor_get(v___x_1570_, 0);
v_isSharedCheck_1623_ = !lean_is_exclusive(v___x_1570_);
if (v_isSharedCheck_1623_ == 0)
{
v___x_1618_ = v___x_1570_;
v_isShared_1619_ = v_isSharedCheck_1623_;
goto v_resetjp_1617_;
}
else
{
lean_inc(v_a_1616_);
lean_dec(v___x_1570_);
v_fst_1571_ = lean_ctor_get(v_a_1569_, 0);
v_isSharedCheck_1591_ = !lean_is_exclusive(v_a_1569_);
if (v_isSharedCheck_1591_ == 0)
v___x_1618_ = lean_box(0);
v_isShared_1619_ = v_isSharedCheck_1623_;
goto v_resetjp_1617_;
}
v_resetjp_1617_:
{
lean_object* v_unused_1592_;
v_unused_1592_ = lean_ctor_get(v_a_1569_, 1);
lean_dec(v_unused_1592_);
v___x_1573_ = v_a_1569_;
v_isShared_1574_ = v_isSharedCheck_1591_;
goto v_resetjp_1572_;
lean_object* v___x_1621_;
if (v_isShared_1619_ == 0)
{
v___x_1621_ = v___x_1618_;
goto v_reusejp_1620_;
}
else
{
lean_inc(v_fst_1571_);
lean_dec(v_a_1569_);
v___x_1573_ = lean_box(0);
v_isShared_1574_ = v_isSharedCheck_1591_;
goto v_resetjp_1572_;
lean_object* v_reuseFailAlloc_1622_;
v_reuseFailAlloc_1622_ = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(v_reuseFailAlloc_1622_, 0, v_a_1616_);
v___x_1621_ = v_reuseFailAlloc_1622_;
goto v_reusejp_1620_;
}
v_resetjp_1572_:
v_reusejp_1620_:
{
lean_object* v___x_1575_; lean_object* v___x_1576_; lean_object* v___x_1577_; lean_object* v___x_1578_; uint8_t v___x_1579_; lean_object* v___x_1581_;
v___x_1575_ = ((lean_object*)(l_Lean_Server_registerRpcProcedure___closed__14));
lean_inc(v_method_1542_);
v___x_1576_ = l_Lean_Name_append(v_method_1542_, v___x_1575_);
lean_inc(v___x_1576_);
v___x_1577_ = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(v___x_1577_, 0, v___x_1576_);
lean_ctor_set(v___x_1577_, 1, v___x_1553_);
lean_ctor_set(v___x_1577_, 2, v___x_1562_);
v___x_1578_ = lean_box(0);
v___x_1579_ = 1;
lean_inc(v___x_1576_);
if (v_isShared_1574_ == 0)
return v___x_1621_;
}
}
}
}
v___jp_1630_:
{
lean_ctor_set_tag(v___x_1573_, 1);
lean_ctor_set(v___x_1573_, 1, v___x_1553_);
lean_ctor_set(v___x_1573_, 0, v___x_1576_);
v___x_1581_ = v___x_1573_;
goto v_reusejp_1580_;
lean_object* v___x_1633_; uint8_t v___x_1634_;
v___x_1633_ = l_Lean_Server_userRpcProcedures;
lean_inc(v_method_1544_);
v___x_1634_ = l_Lean_MapDeclarationExtension_contains___redArg(v___x_1624_, v___x_1633_, v_env_1551_, v_method_1544_);
if (v___x_1634_ == 0)
{
lean_dec_ref(v___x_1629_);
v___y_1553_ = v___y_1631_;
v___y_1554_ = v___y_1632_;
goto v___jp_1552_;
}
else
{
lean_object* v_reuseFailAlloc_1590_;
v_reuseFailAlloc_1590_ = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(v_reuseFailAlloc_1590_, 0, v___x_1576_);
lean_ctor_set(v_reuseFailAlloc_1590_, 1, v___x_1553_);
v___x_1581_ = v_reuseFailAlloc_1590_;
goto v_reusejp_1580_;
}
v_reusejp_1580_:
{
lean_object* v___x_1582_; lean_object* v___x_1583_; lean_object* v___x_1584_;
v___x_1582_ = lean_alloc_ctor(0, 4, 1);
lean_ctor_set(v___x_1582_, 0, v___x_1577_);
lean_ctor_set(v___x_1582_, 1, v_fst_1571_);
lean_ctor_set(v___x_1582_, 2, v___x_1578_);
lean_ctor_set(v___x_1582_, 3, v___x_1581_);
lean_ctor_set_uint8(v___x_1582_, sizeof(void*)*4, v___x_1579_);
v___x_1583_ = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(v___x_1583_, 0, v___x_1582_);
lean_inc(v___y_1552_);
v___x_1584_ = l_Lean_addAndCompile(v___x_1583_, v___x_1554_, v___y_1551_, v___y_1552_);
if (lean_obj_tag(v___x_1584_) == 0)
{
lean_object* v___x_1585_; lean_object* v_env_1586_; lean_object* v___x_1587_; lean_object* v___x_1588_; lean_object* v___x_1589_;
lean_dec_ref(v___x_1584_);
v___x_1585_ = lean_st_ref_get(v___y_1552_);
v_env_1586_ = lean_ctor_get(v___x_1585_, 0);
lean_inc_ref(v_env_1586_);
lean_dec(v___x_1585_);
v___x_1587_ = l_Lean_Server_userRpcProcedures;
v___x_1588_ = l_Lean_MapDeclarationExtension_insert___redArg(v___x_1587_, v_env_1586_, v_method_1542_, v___x_1576_);
v___x_1589_ = l_Lean_setEnv___at___00Lean_Server_registerRpcProcedure_spec__2___redArg(v___x_1588_, v___y_1552_);
lean_dec(v___y_1552_);
return v___x_1589_;
}
else
{
lean_dec(v___x_1576_);
lean_dec(v___y_1552_);
lean_dec(v_method_1542_);
return v___x_1584_;
lean_object* v___x_1635_; lean_object* v___x_1636_; lean_object* v___x_1637_;
lean_dec(v_method_1544_);
v___x_1635_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__19, &l_Lean_Server_registerRpcProcedure___closed__19_once, _init_l_Lean_Server_registerRpcProcedure___closed__19);
v___x_1636_ = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(v___x_1636_, 0, v___x_1629_);
lean_ctor_set(v___x_1636_, 1, v___x_1635_);
v___x_1637_ = l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3___redArg(v___x_1636_, v___y_1631_, v___y_1632_);
lean_dec(v___y_1632_);
lean_dec_ref(v___y_1631_);
return v___x_1637_;
}
}
}
}
else
{
lean_object* v_a_1593_; lean_object* v___x_1595_; uint8_t v_isShared_1596_; uint8_t v_isSharedCheck_1600_;
lean_dec(v___x_1559_);
lean_dec(v___y_1552_);
lean_dec_ref(v___y_1551_);
lean_dec(v_method_1542_);
v_a_1593_ = lean_ctor_get(v___x_1568_, 0);
v_isSharedCheck_1600_ = !lean_is_exclusive(v___x_1568_);
if (v_isSharedCheck_1600_ == 0)
{
v___x_1595_ = v___x_1568_;
v_isShared_1596_ = v_isSharedCheck_1600_;
goto v_resetjp_1594_;
}
else
{
lean_inc(v_a_1593_);
lean_dec(v___x_1568_);
v___x_1595_ = lean_box(0);
v_isShared_1596_ = v_isSharedCheck_1600_;
goto v_resetjp_1594_;
}
v_resetjp_1594_:
{
lean_object* v___x_1598_;
if (v_isShared_1596_ == 0)
{
v___x_1598_ = v___x_1595_;
goto v_reusejp_1597_;
}
else
{
lean_object* v_reuseFailAlloc_1599_;
v_reuseFailAlloc_1599_ = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(v_reuseFailAlloc_1599_, 0, v_a_1593_);
v___x_1598_ = v_reuseFailAlloc_1599_;
goto v_reusejp_1597_;
}
v_reusejp_1597_:
{
return v___x_1598_;
}
}
}
}
v___jp_1607_:
{
lean_object* v___x_1610_; uint8_t v___x_1611_;
v___x_1610_ = l_Lean_Server_userRpcProcedures;
lean_inc(v_method_1542_);
v___x_1611_ = l_Lean_MapDeclarationExtension_contains___redArg(v___x_1601_, v___x_1610_, v_env_1549_, v_method_1542_);
if (v___x_1611_ == 0)
{
lean_dec_ref(v___x_1606_);
v___y_1551_ = v___y_1608_;
v___y_1552_ = v___y_1609_;
goto v___jp_1550_;
}
else
{
lean_object* v___x_1612_; lean_object* v___x_1613_; lean_object* v___x_1614_;
lean_dec(v_method_1542_);
v___x_1612_ = lean_obj_once(&l_Lean_Server_registerRpcProcedure___closed__18, &l_Lean_Server_registerRpcProcedure___closed__18_once, _init_l_Lean_Server_registerRpcProcedure___closed__18);
v___x_1613_ = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(v___x_1613_, 0, v___x_1606_);
lean_ctor_set(v___x_1613_, 1, v___x_1612_);
v___x_1614_ = l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3___redArg(v___x_1613_, v___y_1608_, v___y_1609_);
lean_dec(v___y_1609_);
lean_dec_ref(v___y_1608_);
return v___x_1614_;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcProcedure___boxed(lean_object* v_method_1619_, lean_object* v_a_1620_, lean_object* v_a_1621_, lean_object* v_a_1622_){
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcProcedure___boxed(lean_object* v_method_1642_, lean_object* v_a_1643_, lean_object* v_a_1644_, lean_object* v_a_1645_){
_start:
{
lean_object* v_res_1623_;
v_res_1623_ = l_Lean_Server_registerRpcProcedure(v_method_1619_, v_a_1620_, v_a_1621_);
return v_res_1623_;
lean_object* v_res_1646_;
v_res_1646_ = l_Lean_Server_registerRpcProcedure(v_method_1642_, v_a_1643_, v_a_1644_);
return v_res_1646_;
}
}
LEAN_EXPORT lean_object* l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3(lean_object* v_00_u03b1_1624_, lean_object* v_msg_1625_, lean_object* v___y_1626_, lean_object* v___y_1627_){
LEAN_EXPORT lean_object* l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3(lean_object* v_00_u03b1_1647_, lean_object* v_msg_1648_, lean_object* v___y_1649_, lean_object* v___y_1650_){
_start:
{
lean_object* v___x_1629_;
v___x_1629_ = l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3___redArg(v_msg_1625_, v___y_1626_, v___y_1627_);
return v___x_1629_;
lean_object* v___x_1652_;
v___x_1652_ = l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3___redArg(v_msg_1648_, v___y_1649_, v___y_1650_);
return v___x_1652_;
}
}
LEAN_EXPORT lean_object* l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3___boxed(lean_object* v_00_u03b1_1630_, lean_object* v_msg_1631_, lean_object* v___y_1632_, lean_object* v___y_1633_, lean_object* v___y_1634_){
LEAN_EXPORT lean_object* l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3___boxed(lean_object* v_00_u03b1_1653_, lean_object* v_msg_1654_, lean_object* v___y_1655_, lean_object* v___y_1656_, lean_object* v___y_1657_){
_start:
{
lean_object* v_res_1635_;
v_res_1635_ = l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3(v_00_u03b1_1630_, v_msg_1631_, v___y_1632_, v___y_1633_);
lean_dec(v___y_1633_);
lean_dec_ref(v___y_1632_);
return v_res_1635_;
lean_object* v_res_1658_;
v_res_1658_ = l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3(v_00_u03b1_1653_, v_msg_1654_, v___y_1655_, v___y_1656_);
lean_dec(v___y_1656_);
lean_dec_ref(v___y_1655_);
return v_res_1658_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__0_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_(lean_object* v___x_1636_, lean_object* v_decl_1637_, lean_object* v_x_1638_, uint8_t v_attrKind_1639_, lean_object* v___y_1640_, lean_object* v___y_1641_){
LEAN_EXPORT lean_object* l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__0_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_(lean_object* v___x_1659_, lean_object* v_decl_1660_, lean_object* v_x_1661_, uint8_t v_attrKind_1662_, lean_object* v___y_1663_, lean_object* v___y_1664_){
_start:
{
lean_object* v___x_1643_;
lean_inc(v___y_1641_);
lean_inc_ref(v___y_1640_);
lean_inc(v_decl_1637_);
v___x_1643_ = l_Lean_ensureAttrDeclIsMeta(v___x_1636_, v_decl_1637_, v_attrKind_1639_, v___y_1640_, v___y_1641_);
if (lean_obj_tag(v___x_1643_) == 0)
lean_object* v___x_1666_;
lean_inc(v___y_1664_);
lean_inc_ref(v___y_1663_);
lean_inc(v_decl_1660_);
v___x_1666_ = l_Lean_ensureAttrDeclIsMeta(v___x_1659_, v_decl_1660_, v_attrKind_1662_, v___y_1663_, v___y_1664_);
if (lean_obj_tag(v___x_1666_) == 0)
{
lean_object* v___x_1644_;
lean_dec_ref(v___x_1643_);
v___x_1644_ = l_Lean_Server_registerRpcProcedure(v_decl_1637_, v___y_1640_, v___y_1641_);
return v___x_1644_;
lean_object* v___x_1667_;
lean_dec_ref(v___x_1666_);
v___x_1667_ = l_Lean_Server_registerRpcProcedure(v_decl_1660_, v___y_1663_, v___y_1664_);
return v___x_1667_;
}
else
{
lean_dec(v___y_1641_);
lean_dec_ref(v___y_1640_);
lean_dec(v_decl_1637_);
return v___x_1643_;
lean_dec(v___y_1664_);
lean_dec_ref(v___y_1663_);
lean_dec(v_decl_1660_);
return v___x_1666_;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__0_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2____boxed(lean_object* v___x_1645_, lean_object* v_decl_1646_, lean_object* v_x_1647_, lean_object* v_attrKind_1648_, lean_object* v___y_1649_, lean_object* v___y_1650_, lean_object* v___y_1651_){
LEAN_EXPORT lean_object* l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__0_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2____boxed(lean_object* v___x_1668_, lean_object* v_decl_1669_, lean_object* v_x_1670_, lean_object* v_attrKind_1671_, lean_object* v___y_1672_, lean_object* v___y_1673_, lean_object* v___y_1674_){
_start:
{
uint8_t v_attrKind_boxed_1652_; lean_object* v_res_1653_;
v_attrKind_boxed_1652_ = lean_unbox(v_attrKind_1648_);
v_res_1653_ = l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__0_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_(v___x_1645_, v_decl_1646_, v_x_1647_, v_attrKind_boxed_1652_, v___y_1649_, v___y_1650_);
lean_dec(v_x_1647_);
return v_res_1653_;
uint8_t v_attrKind_boxed_1675_; lean_object* v_res_1676_;
v_attrKind_boxed_1675_ = lean_unbox(v_attrKind_1671_);
v_res_1676_ = l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__0_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_(v___x_1668_, v_decl_1669_, v_x_1670_, v_attrKind_boxed_1675_, v___y_1672_, v___y_1673_);
lean_dec(v_x_1670_);
return v_res_1676_;
}
}
static lean_object* _init_l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__1_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_(void){
_start:
{
lean_object* v___x_1655_; lean_object* v___x_1656_;
v___x_1655_ = ((lean_object*)(l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__0_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_));
v___x_1656_ = l_Lean_stringToMessageData(v___x_1655_);
return v___x_1656_;
lean_object* v___x_1678_; lean_object* v___x_1679_;
v___x_1678_ = ((lean_object*)(l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__0_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_));
v___x_1679_ = l_Lean_stringToMessageData(v___x_1678_);
return v___x_1679_;
}
}
static lean_object* _init_l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__3_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_(void){
_start:
{
lean_object* v___x_1658_; lean_object* v___x_1659_;
v___x_1658_ = ((lean_object*)(l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__2_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_));
v___x_1659_ = l_Lean_stringToMessageData(v___x_1658_);
return v___x_1659_;
lean_object* v___x_1681_; lean_object* v___x_1682_;
v___x_1681_ = ((lean_object*)(l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__2_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_));
v___x_1682_ = l_Lean_stringToMessageData(v___x_1681_);
return v___x_1682_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_(lean_object* v___x_1660_, lean_object* v_decl_1661_, lean_object* v___y_1662_, lean_object* v___y_1663_){
LEAN_EXPORT lean_object* l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_(lean_object* v___x_1683_, lean_object* v_decl_1684_, lean_object* v___y_1685_, lean_object* v___y_1686_){
_start:
{
lean_object* v___x_1665_; lean_object* v___x_1666_; lean_object* v___x_1667_; lean_object* v___x_1668_; lean_object* v___x_1669_; lean_object* v___x_1670_;
v___x_1665_ = lean_obj_once(&l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__1_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_, &l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__1_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2__once, _init_l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__1_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_);
v___x_1666_ = l_Lean_MessageData_ofName(v___x_1660_);
v___x_1667_ = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(v___x_1667_, 0, v___x_1665_);
lean_ctor_set(v___x_1667_, 1, v___x_1666_);
v___x_1668_ = lean_obj_once(&l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__3_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_, &l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__3_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2__once, _init_l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__3_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_);
v___x_1669_ = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(v___x_1669_, 0, v___x_1667_);
lean_ctor_set(v___x_1669_, 1, v___x_1668_);
v___x_1670_ = l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3___redArg(v___x_1669_, v___y_1662_, v___y_1663_);
return v___x_1670_;
lean_object* v___x_1688_; lean_object* v___x_1689_; lean_object* v___x_1690_; lean_object* v___x_1691_; lean_object* v___x_1692_; lean_object* v___x_1693_;
v___x_1688_ = lean_obj_once(&l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__1_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_, &l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__1_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2__once, _init_l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__1_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_);
v___x_1689_ = l_Lean_MessageData_ofName(v___x_1683_);
v___x_1690_ = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(v___x_1690_, 0, v___x_1688_);
lean_ctor_set(v___x_1690_, 1, v___x_1689_);
v___x_1691_ = lean_obj_once(&l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__3_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_, &l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__3_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2__once, _init_l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1___closed__3_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_);
v___x_1692_ = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(v___x_1692_, 0, v___x_1690_);
lean_ctor_set(v___x_1692_, 1, v___x_1691_);
v___x_1693_ = l_Lean_throwError___at___00Lean_Server_registerRpcProcedure_spec__3___redArg(v___x_1692_, v___y_1685_, v___y_1686_);
return v___x_1693_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2____boxed(lean_object* v___x_1671_, lean_object* v_decl_1672_, lean_object* v___y_1673_, lean_object* v___y_1674_, lean_object* v___y_1675_){
LEAN_EXPORT lean_object* l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2____boxed(lean_object* v___x_1694_, lean_object* v_decl_1695_, lean_object* v___y_1696_, lean_object* v___y_1697_, lean_object* v___y_1698_){
_start:
{
lean_object* v_res_1676_;
v_res_1676_ = l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_(v___x_1671_, v_decl_1672_, v___y_1673_, v___y_1674_);
lean_dec(v___y_1674_);
lean_dec_ref(v___y_1673_);
lean_dec(v_decl_1672_);
return v_res_1676_;
lean_object* v_res_1699_;
v_res_1699_ = l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___lam__1_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_(v___x_1694_, v_decl_1695_, v___y_1696_, v___y_1697_);
lean_dec(v___y_1697_);
lean_dec_ref(v___y_1696_);
lean_dec(v_decl_1695_);
return v_res_1699_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_(){
_start:
{
lean_object* v___x_1756_; lean_object* v___x_1757_;
v___x_1756_ = ((lean_object*)(l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___closed__31_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_));
v___x_1757_ = l_Lean_registerBuiltinAttribute(v___x_1756_);
return v___x_1757_;
lean_object* v___x_1779_; lean_object* v___x_1780_;
v___x_1779_ = ((lean_object*)(l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn___closed__31_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_));
v___x_1780_ = l_Lean_registerBuiltinAttribute(v___x_1779_);
return v___x_1780_;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2____boxed(lean_object* v_a_1758_){
LEAN_EXPORT lean_object* l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2____boxed(lean_object* v_a_1781_){
_start:
{
lean_object* v_res_1759_;
v_res_1759_ = l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_();
return v_res_1759_;
lean_object* v_res_1782_;
v_res_1782_ = l___private_Lean_Server_Rpc_RequestHandling_0__Lean_Server_initFn_00___x40_Lean_Server_Rpc_RequestHandling_1988373275____hygCtx___hyg_2_();
return v_res_1782_;
}
}
lean_object* runtime_initialize_Lean_Server_Requests(uint8_t builtin);

6
stage0/stdlib/Lean/Shell.c generated
View file

@ -114,7 +114,7 @@ lean_object* l_Lean_getBuildDir();
lean_object* l_Lean_getLibDir(lean_object*);
lean_object* lean_decode_lossy_utf8(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Shell_0__Lean_decodeLossyUTF8___boxed(lean_object*);
uint32_t lean_run_main(lean_object*, lean_object*, lean_object*);
uint32_t lean_eval_main(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Shell_0__Lean_runMain___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_init_llvm();
LEAN_EXPORT lean_object* l___private_Lean_Shell_0__Lean_initLLVM___boxed(lean_object*);
@ -598,7 +598,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Shell_0__Lean_runMain___boxed(lean_obj
_start:
{
uint32_t v_res_12_; lean_object* v_r_13_;
v_res_12_ = lean_run_main(v_env_8_, v_opts_9_, v_args_10_);
v_res_12_ = lean_eval_main(v_env_8_, v_opts_9_, v_args_10_);
lean_dec(v_args_10_);
lean_dec_ref(v_opts_9_);
lean_dec_ref(v_env_8_);
@ -9601,7 +9601,7 @@ lean_dec(v_cFileName_x3f_2786_);
v_val_2889_ = lean_ctor_get(v_a_2829_, 0);
lean_inc(v_val_2889_);
lean_dec_ref(v_a_2829_);
v___x_2890_ = lean_run_main(v_val_2889_, v_leanOpts_2772_, v___y_2824_);
v___x_2890_ = lean_eval_main(v_val_2889_, v_leanOpts_2772_, v___y_2824_);
lean_dec(v___y_2824_);
lean_dec_ref(v_leanOpts_2772_);
lean_dec(v_val_2889_);