From e20a07bd6dd030cd94d42c240dd97310fa409c4f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 1 May 2021 16:23:32 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/kernel/inductive.cpp | 3 +- stage0/stdlib/Lean/Elab/Match.c | 98 +++++++++++++------------- stage0/stdlib/Lean/Elab/Tactic/Match.c | 4 +- stage0/stdlib/Lean/Meta/IndPredBelow.c | 6 +- 4 files changed, 56 insertions(+), 55 deletions(-) diff --git a/stage0/src/kernel/inductive.cpp b/stage0/src/kernel/inductive.cpp index d4daf5cc27..3d1a47659b 100644 --- a/stage0/src/kernel/inductive.cpp +++ b/stage0/src/kernel/inductive.cpp @@ -593,7 +593,8 @@ public: expr u_app = mk_app(u_i, xs); C_app = mk_app(C_app, u_app); expr v_i_ty = mk_pi(xs, C_app); - expr v_i = mk_local_decl(name("v").append_after(i), v_i_ty, binder_info()); + local_decl u_i_decl = m_lctx.get_local_decl(fvar_name(u_i)); + expr v_i = mk_local_decl(u_i_decl.get_user_name().append_after("_ih"), v_i_ty, binder_info()); v.push_back(v_i); } expr minor_ty = mk_pi(b_u, mk_pi(v, C_app)); diff --git a/stage0/stdlib/Lean/Elab/Match.c b/stage0/stdlib/Lean/Elab/Match.c index 609541164e..1e689fc161 100644 --- a/stage0/stdlib/Lean/Elab/Match.c +++ b/stage0/stdlib/Lean/Elab/Match.c @@ -154,6 +154,7 @@ lean_object* lean_environment_find(lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_15342____closed__8; lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__3___lambda__1___closed__2; lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Quotation_precheckIdent___spec__1___rarg(lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__2; lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_throwEx___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isMatchUnit_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -165,6 +166,7 @@ lean_object* lean_st_ref_get(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_precheckMatch_match__3___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_generalize_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___closed__17; +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1; extern lean_object* l_Lean_instInhabitedParserDescr___closed__1; extern lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__1; uint8_t lean_name_eq(lean_object*, lean_object*); @@ -218,6 +220,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_pr extern lean_object* l_Array_getEvenElems___rarg___closed__1; lean_object* l_Lean_MessageData_ofList(lean_object*); lean_object* l_Lean_Meta_isTypeCorrect(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__4; lean_object* l_Array_sequenceMap___at_Lean_Elab_Term_precheckMatch___spec__1(lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_generalize_match__2(lean_object*); lean_object* l_Lean_Elab_Term_ToDepElimPattern_main___closed__1; @@ -258,14 +261,12 @@ lean_object* l_Lean_Expr_replaceFVars(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_foldrMUnsafe_fold___at___private_Lean_Elab_Match_0__Lean_Elab_Term_generalize___spec__4___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*); lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltView___closed__3; -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1; lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_finalizePatternDecls___spec__1___closed__4; lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processCtorAppCore___lambda__2(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_getMainModule___rarg(lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_1481____closed__8; uint8_t l_USize_decLt(size_t, size_t); -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__2; lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processId_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_rootNamespace___closed__2; @@ -288,7 +289,6 @@ lean_object* l_Lean_Elab_Term_instToStringPatternVar_match__1(lean_object*); lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*); lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltView___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Match_0__Lean_Elab_Term_generalize___spec__1(lean_object*, size_t, size_t, lean_object*); -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__5; lean_object* l_Lean_Elab_Term_precheckMatch___lambda__1(lean_object*, lean_object*); lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkEqRefl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -345,7 +345,6 @@ extern lean_object* l___private_Lean_Util_Trace_0__Lean_addNode___rarg___lambda_ uint8_t l_Lean_Name_hasMacroScopes(lean_object*); lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_withPatternVars_loop_match__1(lean_object*); -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__4; lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_getMVarSyntaxMVarId(lean_object*); lean_object* l_Lean_Elab_throwIllFormedSyntax___at___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_quotedNameToPattern___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabTermEnsuringType(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -389,6 +388,7 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_getPatternVarNames___ extern lean_object* l_List_forIn_loop___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_checkNextPatternTypes___spec__1___closed__1; lean_object* l___regBuiltin_Lean_Elab_Term_elabMatch(lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__5; lean_object* l_Lean_Meta_Match_Pattern_toExpr_visit(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_precheckMatch___spec__5___closed__1; lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_Match_0__Lean_Elab_Term_getIndicesToInclude___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -453,6 +453,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscr lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___closed__12; lean_object* l_Lean_throwError___at_Lean_Elab_Term_CollectPatternVars_collect_processCtorAppCore___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_instantiateLocalDeclMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__3; lean_object* l_Lean_Elab_Term_mkMatcher(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Elab_Term_Quotation_precheckAttribute; lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isMatchUnit_x3f_match__2(lean_object*); @@ -478,7 +479,6 @@ uint8_t l_Lean_Option_get___at_Lean_ppExpr___spec__1(lean_object*, lean_object*) lean_object* l_Lean_Elab_Term_elabMatch_elabMatchDefault___closed__1; lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processCtorAppContext_match__2(lean_object*); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__3; uint8_t l_Lean_LocalDecl_binderInfo(lean_object*); lean_object* l_Lean_Elab_Term_expandMacrosInPatterns(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux_match__2(lean_object*); @@ -513,6 +513,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs lean_object* l_Lean_throwError___at_Lean_Elab_Term_CollectPatternVars_collect_processCtorAppCore___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2; lean_object* l_Lean_Elab_Term_finalizePatternDecls_match__2(lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__1; lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processCtor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabPatterns___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_loop___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*); @@ -536,7 +537,6 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_getPatternVarNames___ extern lean_object* l___private_Init_Meta_0__Lean_quoteName___closed__2; lean_object* l_ReaderT_pure___at_Lean_Elab_liftMacroM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___spec__1___lambda__2___closed__3; -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__1; lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__1(size_t, size_t, lean_object*); lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_mkMVarSyntax___rarg(lean_object*, lean_object*); lean_object* l_Lean_Syntax_mkStrLit(lean_object*, lean_object*); @@ -640,6 +640,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_mkUserNameFor___boxed lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_tryPostponeIfDiscrTypeIsMVar___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_nullKind___closed__2; lean_object* l_Lean_Elab_Term_CollectPatternVars_collect(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2; lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_tryPostponeIfDiscrTypeIsMVar___spec__1___closed__1; extern lean_object* l_Lean_Elab_Term_termElabAttribute; lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processId_match__2___rarg(lean_object*, lean_object*, lean_object*); @@ -648,7 +649,6 @@ extern lean_object* l_Lean_Elab_throwIllFormedSyntax___rarg___closed__2; lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_processCtorAppContext(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_instToStringPatternVar(lean_object*); lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*); -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2; lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_waitExpectedType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Syntax_isNodeOf(lean_object*, lean_object*, lean_object*); @@ -988,9 +988,9 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux_match__3 lean_object* l_Lean_Elab_Term_isLocalIdent_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__4___lambda__1___closed__1; lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Closure_mkBinding___spec__1(size_t, size_t, lean_object*); -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327_(lean_object*); -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12038_(lean_object*); -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275_(lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329_(lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12040_(lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277_(lean_object*); lean_object* l_Lean_mkConst(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_reportMatcherResultErrors___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkSimpleThunk(lean_object*); @@ -4490,7 +4490,7 @@ return x_11; } } } -static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__1() { +static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__1() { _start: { lean_object* x_1; @@ -4498,21 +4498,21 @@ x_1 = lean_mk_string("MVarWithIdKind"); return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2() { +static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__1; +x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275_(lean_object* x_1) { +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2; +x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2; x_3 = l_Lean_Parser_registerBuiltinNodeKind(x_2, x_1); return x_3; } @@ -4533,7 +4533,7 @@ lean_ctor_set(x_7, 0, x_5); lean_ctor_set(x_7, 1, x_6); x_8 = l_Lean_mkOptionalNode___closed__2; x_9 = lean_array_push(x_8, x_7); -x_10 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2; +x_10 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2; x_11 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_11, 0, x_10); lean_ctor_set(x_11, 1, x_9); @@ -4554,7 +4554,7 @@ lean_ctor_set(x_15, 0, x_12); lean_ctor_set(x_15, 1, x_14); x_16 = l_Lean_mkOptionalNode___closed__2; x_17 = lean_array_push(x_16, x_15); -x_18 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2; +x_18 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2; x_19 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_19, 0, x_18); lean_ctor_set(x_19, 1, x_17); @@ -4656,7 +4656,7 @@ _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_2 = l_Lean_Elab_Term_termElabAttribute; -x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2; +x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2; x_4 = l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind___closed__1; x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; @@ -31775,7 +31775,7 @@ lean_dec(x_5); return x_12; } } -static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1() { +static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -31785,7 +31785,7 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__2() { +static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__2() { _start: { lean_object* x_1; @@ -31793,17 +31793,17 @@ x_1 = lean_mk_string("ignoreUnusedAlts"); return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__3() { +static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1; -x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__2; +x_1 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1; +x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__2; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__4() { +static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__4() { _start: { lean_object* x_1; @@ -31811,13 +31811,13 @@ x_1 = lean_mk_string("if true, do not generate error if an alternative is not us return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__5() { +static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__5() { _start: { uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_1 = 0; x_2 = l_Lean_instInhabitedParserDescr___closed__1; -x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__4; +x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__4; x_4 = lean_box(x_1); x_5 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_5, 0, x_4); @@ -31826,12 +31826,12 @@ lean_ctor_set(x_5, 2, x_3); return x_5; } } -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327_(lean_object* x_1) { +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__3; -x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__5; +x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__3; +x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__5; x_4 = l_Lean_Option_register___at_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_4____spec__1(x_2, x_3, x_1); return x_4; } @@ -36083,7 +36083,7 @@ x_31 = lean_ctor_get(x_29, 1); lean_inc(x_31); lean_dec(x_29); x_32 = lean_array_get_size(x_25); -x_33 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1; +x_33 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1; lean_inc(x_7); x_34 = l_Lean_Elab_Term_mkAuxName(x_33, x_7, x_8, x_9, x_10, x_11, x_12, x_31); if (lean_obj_tag(x_34) == 0) @@ -36489,7 +36489,7 @@ x_109 = lean_ctor_get(x_21, 1); lean_inc(x_109); lean_dec(x_21); x_110 = lean_array_get_size(x_106); -x_111 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1; +x_111 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1; lean_inc(x_7); x_112 = l_Lean_Elab_Term_mkAuxName(x_111, x_7, x_8, x_9, x_10, x_11, x_12, x_105); if (lean_obj_tag(x_112) == 0) @@ -40220,7 +40220,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12038_(lean_object* x_1) { +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12040_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -40529,11 +40529,11 @@ l_Lean_Elab_Term_expandMacrosInPatterns___boxed__const__1 = _init_l_Lean_Elab_Te lean_mark_persistent(l_Lean_Elab_Term_expandMacrosInPatterns___boxed__const__1); l_Lean_Elab_Term_instToStringPatternVar___closed__1 = _init_l_Lean_Elab_Term_instToStringPatternVar___closed__1(); lean_mark_persistent(l_Lean_Elab_Term_instToStringPatternVar___closed__1); -l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__1(); -lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__1); -l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2(); -lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275____closed__2); -res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2275_(lean_io_mk_world()); +l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__1(); +lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__1); +l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2(); +lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277____closed__2); +res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2277_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind___closed__1(); @@ -40749,17 +40749,17 @@ l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_collectDeps___cl lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_collectDeps___closed__1); l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___boxed__const__1 = _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___boxed__const__1(); lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___boxed__const__1); -l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1(); -lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1); -l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__2(); -lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__2); -l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__3(); -lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__3); -l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__4(); -lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__4); -l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__5 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__5(); -lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__5); -res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327_(lean_io_mk_world()); +l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1(); +lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1); +l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__2(); +lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__2); +l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__3(); +lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__3); +l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__4(); +lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__4); +l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__5 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__5(); +lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__5); +res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_Elab_Term_match_ignoreUnusedAlts = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Elab_Term_match_ignoreUnusedAlts); @@ -40835,7 +40835,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabMatch___closed__1); res = l___regBuiltin_Lean_Elab_Term_elabMatch(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12038_(lean_io_mk_world()); +res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12040_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l_Lean_Elab_Term_elabNoMatch___closed__1 = _init_l_Lean_Elab_Term_elabNoMatch___closed__1(); diff --git a/stage0/stdlib/Lean/Elab/Tactic/Match.c b/stage0/stdlib/Lean/Elab/Tactic/Match.c index 298a2f2c69..9bb2c541ff 100644 --- a/stage0/stdlib/Lean/Elab/Tactic/Match.c +++ b/stage0/stdlib/Lean/Elab/Tactic/Match.c @@ -42,6 +42,7 @@ size_t l_USize_sub(size_t, size_t); extern lean_object* l_Array_empty___closed__1; extern lean_object* l_myMacro____x40_Init_Notation___hyg_15342____closed__8; lean_object* lean_st_ref_get(lean_object*, lean_object*); +extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1; lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTerm_match__1(lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_15342____closed__2; @@ -56,7 +57,6 @@ lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Match_0__Lea size_t l_USize_shiftRight(size_t, size_t); lean_object* lean_string_utf8_byte_size(lean_object*); lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTermAux___spec__1___boxed(lean_object*, lean_object*, lean_object*); -extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1; lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Tactic_evalMatch___spec__1___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* l_Lean_Elab_Term_getMainModule___rarg(lean_object*, lean_object*); @@ -1593,7 +1593,7 @@ lean_dec(x_277); x_316 = lean_ctor_get(x_6, 0); lean_inc(x_316); lean_dec(x_6); -x_317 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9327____closed__1; +x_317 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9329____closed__1; x_318 = l_Lean_Name_appendIndexAfter(x_317, x_316); x_319 = l_Lean_Name_append(x_1, x_318); x_320 = l_Lean_mkIdentFrom(x_30, x_319); diff --git a/stage0/stdlib/Lean/Meta/IndPredBelow.c b/stage0/stdlib/Lean/Meta/IndPredBelow.c index a752ea9d74..202fb35da7 100644 --- a/stage0/stdlib/Lean/Meta/IndPredBelow.c +++ b/stage0/stdlib/Lean/Meta/IndPredBelow.c @@ -299,7 +299,7 @@ lean_object* l_Lean_Meta_transform_visit_visitLambda___at_Lean_Meta_IndPredBelow lean_object* l_Lean_Meta_IndPredBelow_proveBrecOn_closeGoal___rarg___closed__6; lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_processPostponedStep___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_4_(lean_object*); -lean_object* l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_2916_(lean_object*); +lean_object* l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_2924_(lean_object*); lean_object* l_Lean_Meta_forallTelescope___at_Lean_Meta_IndPredBelow_mkContext_mkHeader___spec__3(lean_object*); lean_object* l_Lean_Meta_getLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_IndPredBelow_mkCtorType_checkCount___spec__8___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -13308,7 +13308,7 @@ lean_dec(x_1); return x_12; } } -lean_object* l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_2916_(lean_object* x_1) { +lean_object* l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_2924_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -13449,7 +13449,7 @@ l_Lean_Meta_IndPredBelow_mkBelow___closed__6 = _init_l_Lean_Meta_IndPredBelow_mk lean_mark_persistent(l_Lean_Meta_IndPredBelow_mkBelow___closed__6); l_Lean_Meta_IndPredBelow_mkBelow___closed__7 = _init_l_Lean_Meta_IndPredBelow_mkBelow___closed__7(); lean_mark_persistent(l_Lean_Meta_IndPredBelow_mkBelow___closed__7); -res = l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_2916_(lean_io_mk_world()); +res = l_Lean_Meta_IndPredBelow_initFn____x40_Lean_Meta_IndPredBelow___hyg_2924_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); return lean_io_result_mk_ok(lean_box(0));