From 77de817960c252cc9a2f1ca79911fcfe3cba7014 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Feb 2024 12:19:04 -0800 Subject: [PATCH] chore: update stage0 --- stage0/stdlib/Lean/Elab/ComputedFields.c | 2 +- stage0/stdlib/Lean/Elab/MutualDef.c | 10 +-- stage0/stdlib/Lean/Meta/Basic.c | 74 +++++++++++----------- stage0/stdlib/Lean/Meta/Closure.c | 10 +-- stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c | 2 +- stage0/stdlib/Lean/Meta/WHNF.c | 8 +-- 6 files changed, 53 insertions(+), 53 deletions(-) diff --git a/stage0/stdlib/Lean/Elab/ComputedFields.c b/stage0/stdlib/Lean/Elab/ComputedFields.c index 61e74686bc..b414003703 100644 --- a/stage0/stdlib/Lean/Elab/ComputedFields.c +++ b/stage0/stdlib/Lean/Elab/ComputedFields.c @@ -999,7 +999,7 @@ return x_17; else { uint8_t x_18; -x_18 = lean_ctor_get_uint8(x_3, 3); +x_18 = lean_ctor_get_uint8(x_3, 4); if (x_18 == 0) { uint8_t x_19; diff --git a/stage0/stdlib/Lean/Elab/MutualDef.c b/stage0/stdlib/Lean/Elab/MutualDef.c index 908ee7de5e..8be10eef29 100644 --- a/stage0/stdlib/Lean/Elab/MutualDef.c +++ b/stage0/stdlib/Lean/Elab/MutualDef.c @@ -247,7 +247,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_checkForHid lean_object* l_Lean_stringToMessageData(lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkLetRecClosures___spec__11(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabMutualDef(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_resetZetaFVarIds___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_MutualClosure_main___spec__6(lean_object*, size_t, size_t, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_checkForHiddenUnivLevels_visit___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_checkForHiddenUnivLevels___spec__2___closed__2; @@ -360,6 +359,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualD static lean_object* l_Lean_Elab_Term_checkForHiddenUnivLevels_visitLevel___closed__8; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_elabMutualDef___spec__12___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_List_forM___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_checkLetRecsToLiftTypes___spec__1___closed__1; +lean_object* l_Lean_Meta_resetZetaDeltaFVarIds___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_elabMutualDef___spec__11___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_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereStructInst___spec__5___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_removeUnusedVars___closed__2; @@ -467,7 +467,6 @@ lean_object* l_Lean_RBNode_findCore___at_Lean_Elab_Structural_findRecArg_go___sp lean_object* l_Lean_Expr_forallE___override(lean_object*, lean_object*, lean_object*, uint8_t); static lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Term_elabMutualDef_processDeriving___spec__5___closed__4; LEAN_EXPORT lean_object* l_Lean_Elab_elabAttrs___at_Lean_Elab_Command_elabMutualDef___spec__3(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_getZetaFVarIds___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkInitialUsedFVarsMap___spec__5___rarg___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_Array_indexOfAux___at_Lean_LocalContext_erase___spec__3(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_elabModifiers___at_Lean_Elab_Command_elabMutualDef___spec__1___lambda__3___closed__4; @@ -635,6 +634,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_Mutua lean_object* l_Lean_Elab_Term_withAutoBoundImplicitForbiddenPred___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Std_Format_defWidth; static lean_object* l_Lean_Elab_instInhabitedDefViewElabHeader___closed__2; +lean_object* l_Lean_Meta_getZetaDeltaFVarIds___rarg(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_getPendindMVarErrorMessage___closed__1; LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Term_MutualClosure_getModifiersForLetRecs___spec__2___boxed(lean_object*, lean_object*, lean_object*); static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__6___lambda__5___closed__6; @@ -15531,7 +15531,7 @@ x_34 = lean_ctor_get(x_14, 1); lean_dec(x_34); x_35 = lean_ctor_get(x_14, 0); lean_dec(x_35); -x_36 = l_Lean_Meta_getZetaFVarIds___rarg(x_8, x_9, x_10, x_28); +x_36 = l_Lean_Meta_getZetaDeltaFVarIds___rarg(x_8, x_9, x_10, x_28); x_37 = lean_ctor_get(x_36, 0); lean_inc(x_37); x_38 = lean_ctor_get(x_36, 1); @@ -15801,7 +15801,7 @@ lean_inc(x_111); lean_inc(x_110); lean_inc(x_109); lean_dec(x_14); -x_113 = l_Lean_Meta_getZetaFVarIds___rarg(x_8, x_9, x_10, x_28); +x_113 = l_Lean_Meta_getZetaDeltaFVarIds___rarg(x_8, x_9, x_10, x_28); x_114 = lean_ctor_get(x_113, 0); lean_inc(x_114); x_115 = lean_ctor_get(x_113, 1); @@ -22359,7 +22359,7 @@ lean_inc(x_15); x_22 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkFreeVarMap___spec__1(x_21, x_18, x_15); lean_inc(x_19); x_23 = l_Array_append___rarg(x_22, x_19); -x_24 = l_Lean_Meta_resetZetaFVarIds___rarg(x_9, x_10, x_11, x_12); +x_24 = l_Lean_Meta_resetZetaDeltaFVarIds___rarg(x_9, x_10, x_11, x_12); x_25 = lean_ctor_get(x_8, 0); lean_inc(x_25); x_26 = lean_ctor_get(x_24, 1); diff --git a/stage0/stdlib/Lean/Meta/Basic.c b/stage0/stdlib/Lean/Meta/Basic.c index c4ce5d7b99..4f706e2248 100644 --- a/stage0/stdlib/Lean/Meta/Basic.c +++ b/stage0/stdlib/Lean/Meta/Basic.c @@ -34,6 +34,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_ppExpr(lean_object*, lean_object*, lean_obj LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_savingCacheImpl___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_5_(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_withLocalInstances___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_getZetaDeltaFVarIds___boxed(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_isInductivePredicate___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___rarg___lambda__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*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withExistingLocalDeclsImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -139,7 +140,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_processPostponed___boxed(lean_object*, lean static lean_object* l_Lean_Meta_getLocalDeclFromUserName___closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_approxDefEq(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_instantiateForallAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_getZetaFVarIds(lean_object*); lean_object* l_Lean_Level_succ___override(lean_object*); double l_Lean_trace_profiler_threshold_getSecs(lean_object*); LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_withLocalInstancesImp___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -147,7 +147,6 @@ LEAN_EXPORT lean_object* l_Lean_instantiateLevelMVars___at_Lean_Meta_normalizeLe LEAN_EXPORT uint8_t l_Lean_Meta_ParamInfo_isProp___default; LEAN_EXPORT lean_object* l_Lean_Meta_instMonadLCtxMetaM(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_sort___override(lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaFVarIds___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_LMVarId_getLevel___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_processPostponed_loop___closed__3; lean_object* l_Lean_PersistentArray_push___rarg(lean_object*, lean_object*); @@ -176,6 +175,7 @@ uint8_t lean_usize_dec_eq(size_t, size_t); static lean_object* l_Lean_Meta_instMonadMetaM___closed__5; LEAN_EXPORT lean_object* l_Lean_FVarId_isLetVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_modifyCache___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_withTrackingZetaDelta___rarg(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_checkpointDefEq___closed__1; LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarCore(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -209,7 +209,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_DefEqCache_instances___default; LEAN_EXPORT lean_object* l_Lean_Meta_withLocalInstances___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_instMonadEnvMetaM___closed__3; LEAN_EXPORT lean_object* l_Lean_Meta_withNewBinderInfos___at_Lean_Meta_withInstImplicitAsImplict___spec__3(lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaFVarIds___boxed(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_State_zetaDeltaFVarIds___default; static lean_object* l_Lean_Meta_State_postponed___default___closed__3; LEAN_EXPORT lean_object* l___private_Lean_Util_Trace_0__Lean_addTraceNode___at_Lean_Meta_processPostponed___spec__4___boxed(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_Meta_isDefEqNoConstantApprox(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -237,7 +237,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withNewLocalIn static lean_object* l_Lean_Meta_instInhabitedCache___closed__2; LEAN_EXPORT lean_object* l_Lean_PersistentArray_forInAux___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_MVarId_setKind(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_withTrackingZeta___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_savingCacheImpl(lean_object*); LEAN_EXPORT lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_withConfig___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -274,7 +273,6 @@ lean_object* l_Lean_stringToMessageData(lean_object*); static lean_object* l_Lean_Meta_mkLevelErrorMessage___closed__1; static lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_instantiateLambdaAux___closed__1; lean_object* l_Lean_Expr_mvar___override(lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaFVarIds___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescopeReducing___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Meta_mkFreshExprMVarAt___spec__2(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_ParamInfo_backDeps___default; @@ -324,6 +322,7 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_MVarId_getDecl___spec__1___ static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_5____closed__1; static lean_object* l_Lean_Meta_mkLevelStuckErrorMessage___closed__1; static lean_object* l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__4___closed__1; +LEAN_EXPORT lean_object* l_Lean_Meta_getZetaDeltaFVarIds(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_getLocalInstances___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_instHashableArray___rarg___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_mkFreshExprMVarWithId___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -365,6 +364,7 @@ LEAN_EXPORT uint8_t l___private_Lean_Meta_Basic_0__Lean_Meta_mkLeveErrorMessageC LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp___rarg(lean_object*, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__3___closed__5; LEAN_EXPORT uint8_t l___private_Init_Data_Option_Basic_0__Option_beqOption____x40_Init_Data_Option_Basic___hyg_158____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaDeltaFVarIds___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_getFVarFromUserName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_RBNode_findCore___at___private_Lean_Meta_Basic_0__Lean_Meta_mkLeveErrorMessageCore___spec__1___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_mkFreshLevelMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -473,9 +473,9 @@ LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Meta_withIncRecDept LEAN_EXPORT lean_object* l_Lean_Meta_setMVarUserName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___rarg___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_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassExpensive_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_getZetaFVarIds___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_liftMetaM(lean_object*, lean_object*); static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__5___closed__2; +LEAN_EXPORT lean_object* l_Lean_Meta_withTrackingZetaDelta(lean_object*); static lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_instantiateForallAux___closed__1; LEAN_EXPORT lean_object* l_Lean_Meta_isLevelDefEqAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkLeveErrorMessageCore___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -521,6 +521,7 @@ extern lean_object* l_Lean_Expr_instHashableExpr; static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1614____closed__14; LEAN_EXPORT lean_object* l_Lean_Meta_inferType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassApp_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_withTrackingZetaDelta___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_levelZero; LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withNewMCtxDepthImp___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_lambdaMetaTelescope_process(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -530,7 +531,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_fullApproxDefEq___rarg___lambda__1(lean_obj lean_object* lean_io_mono_nanos_now(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_getTransparency(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp_process(lean_object*); -LEAN_EXPORT uint8_t l_Lean_Meta_Config_trackZeta___default; static lean_object* l_Lean_Meta_instAlternativeMetaM___closed__2; LEAN_EXPORT lean_object* l_Lean_MVarId_setType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Level_hasMVar(lean_object*); @@ -590,6 +590,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_getResetPostponed(lean_object*, lean_object LEAN_EXPORT lean_object* l_Lean_Meta_withConfig___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_simpLevelIMax_x27(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_State_mctx___default; +LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaDeltaFVarIds___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_FVarId_getBinderInfo___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_LocalDecl_isLet(lean_object*); lean_object* l_Lean_MetavarContext_mkBinding(uint8_t, lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*); @@ -634,6 +635,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_withLCtx___rarg(lean_object*, lean_object*, static lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassExpensive_x3f___closed__1; LEAN_EXPORT lean_object* l_Lean_Meta_instMonadBacktrackSavedStateMetaM; static lean_object* l_Lean_Meta_DefEqCache_reducible___default___closed__1; +LEAN_EXPORT lean_object* l_Lean_Meta_getZetaDeltaFVarIds___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withNewFVar___boxed(lean_object*, lean_object*); static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1614____closed__16; LEAN_EXPORT lean_object* l_Lean_Meta_approxDefEq___rarg(lean_object*, lean_object*, lean_object*, lean_object*); @@ -643,7 +645,6 @@ size_t lean_usize_mod(size_t, size_t); LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__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*, lean_object*); LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_LMVarId_getLevel___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_instInhabitedMetaM___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_getZetaFVarIds___boxed(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_getMVarDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_initFn____x40_Lean_Meta_Basic___hyg_14916____closed__4; static lean_object* l_Lean_Meta_instInhabitedMetaM___rarg___closed__2; @@ -701,6 +702,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_throwIsDefEqStuck___boxed(lean_object*, lea LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Meta_mkFreshExprMVarAt___spec__2___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_instantiateLambdaAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_instMonadMetaM___closed__2; +LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaDeltaFVarIds(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_withLCtx___at___private_Lean_Meta_Basic_0__Lean_Meta_mkLeveErrorMessageCore___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp_process___rarg(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_Cache_inferType___default___closed__1; @@ -708,7 +710,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_withLetDecl___rarg___boxed(lean_object*, le LEAN_EXPORT lean_object* l_Lean_Meta_mkFunUnit___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_withNewLocalInstances(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_checkpointDefEq(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_withTrackingZeta___rarg(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_processPostponed_loop___closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_shouldReduceReducibleOnly___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -747,11 +748,9 @@ static lean_object* l_Lean_Meta_instMonadMCtxMetaM___closed__3; LEAN_EXPORT lean_object* l_Lean_Meta_mkFreshLevelMVarsFor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_withLetDecl(lean_object*); LEAN_EXPORT lean_object* l_Lean_MVarId_getDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_getZetaFVarIds___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_getFVarLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_fullApproxDefEq(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_mkFreshExprMVarWithId(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_State_zetaFVarIds___default; uint8_t lean_nat_dec_lt(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_Meta_sortFVarIds___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -847,7 +846,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey___box LEAN_EXPORT lean_object* l_Lean_Meta_map2MetaM___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_shouldReduceAll___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_elimMVarDeps(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_withTrackingZeta(lean_object*); LEAN_EXPORT lean_object* l_Lean_addTrace___at_Lean_Meta_processPostponed_loop___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_withAtLeastTransparency___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_mkFreshLMVarId___at_Lean_Meta_mkFreshLevelMVar___spec__1(lean_object*, lean_object*, lean_object*); @@ -877,6 +875,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_forallBoundedTelescope(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_fullApproxDefEqImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_instantiateMVarsCore(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_FVarId_findDecl_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaDeltaFVarIds___boxed(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_instInhabitedMetaM___rarg(lean_object*); static lean_object* l_Lean_Meta_instMonadMetaM___closed__6; uint8_t l_Lean_Name_quickCmp(lean_object*, lean_object*); @@ -963,7 +962,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassImp_x3f static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1614____closed__4; LEAN_EXPORT lean_object* l_Lean_Meta_useEtaStruct___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_findMVarDecl_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaFVarIds(lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_withLocalDeclsD___spec__1___rarg(size_t, size_t, lean_object*); static lean_object* l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__5___closed__1; LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_liftMkBindingM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1011,6 +1009,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Util_Trace_0__Lean_getResetTraces___at LEAN_EXPORT lean_object* l_Lean_Meta_withNewBinderInfos___at_Lean_Meta_withInstImplicitAsImplict___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_instBEqArray___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Basic_0__Lean_Meta_withNewBinderInfosImp___spec__1(lean_object*, size_t, size_t, lean_object*); +LEAN_EXPORT uint8_t l_Lean_Meta_Config_trackZetaDelta___default; LEAN_EXPORT lean_object* l_Lean_MVarId_isReadOnly___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_checkpointDefEq___at_Lean_Meta_isLevelDefEq___spec__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_fullApproxDefEqImp(lean_object*); @@ -1043,6 +1042,7 @@ LEAN_EXPORT uint8_t l_Lean_Meta_ParamInfo_isExplicit(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Cache_defEqTrans___default; LEAN_EXPORT lean_object* l_Lean_Meta_ppExprWithInfos(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_instInhabitedInfoCacheKey___closed__1; +LEAN_EXPORT lean_object* l_Lean_Meta_getZetaDeltaFVarIds___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_array_uset(lean_object*, size_t, lean_object*); lean_object* l_Lean_Expr_ReplaceImpl_Cache_store(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_MessageData_ofName(lean_object*); @@ -1193,7 +1193,7 @@ x_1 = 1; return x_1; } } -static uint8_t _init_l_Lean_Meta_Config_trackZeta___default() { +static uint8_t _init_l_Lean_Meta_Config_trackZetaDelta___default() { _start: { uint8_t x_1; @@ -2003,7 +2003,7 @@ x_1 = l_Lean_Meta_instInhabitedCache___closed__4; return x_1; } } -static lean_object* _init_l_Lean_Meta_State_zetaFVarIds___default() { +static lean_object* _init_l_Lean_Meta_State_zetaDeltaFVarIds___default() { _start: { lean_object* x_1; @@ -5513,7 +5513,7 @@ lean_dec(x_1); return x_6; } } -LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaFVarIds___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaDeltaFVarIds___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; @@ -5594,35 +5594,35 @@ return x_27; } } } -LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaFVarIds(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaDeltaFVarIds(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_Lean_Meta_resetZetaFVarIds___rarg___boxed), 4, 0); +x_2 = lean_alloc_closure((void*)(l_Lean_Meta_resetZetaDeltaFVarIds___rarg___boxed), 4, 0); return x_2; } } -LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaFVarIds___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaDeltaFVarIds___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; -x_5 = l_Lean_Meta_resetZetaFVarIds___rarg(x_1, x_2, x_3, x_4); +x_5 = l_Lean_Meta_resetZetaDeltaFVarIds___rarg(x_1, x_2, x_3, x_4); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); return x_5; } } -LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaFVarIds___boxed(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaDeltaFVarIds___boxed(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l_Lean_Meta_resetZetaFVarIds(x_1); +x_2 = l_Lean_Meta_resetZetaDeltaFVarIds(x_1); lean_dec(x_1); return x_2; } } -LEAN_EXPORT lean_object* l_Lean_Meta_getZetaFVarIds___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +LEAN_EXPORT lean_object* l_Lean_Meta_getZetaDeltaFVarIds___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; uint8_t x_6; @@ -5656,30 +5656,30 @@ return x_12; } } } -LEAN_EXPORT lean_object* l_Lean_Meta_getZetaFVarIds(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_getZetaDeltaFVarIds(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_Lean_Meta_getZetaFVarIds___rarg___boxed), 4, 0); +x_2 = lean_alloc_closure((void*)(l_Lean_Meta_getZetaDeltaFVarIds___rarg___boxed), 4, 0); return x_2; } } -LEAN_EXPORT lean_object* l_Lean_Meta_getZetaFVarIds___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +LEAN_EXPORT lean_object* l_Lean_Meta_getZetaDeltaFVarIds___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; -x_5 = l_Lean_Meta_getZetaFVarIds___rarg(x_1, x_2, x_3, x_4); +x_5 = l_Lean_Meta_getZetaDeltaFVarIds___rarg(x_1, x_2, x_3, x_4); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); return x_5; } } -LEAN_EXPORT lean_object* l_Lean_Meta_getZetaFVarIds___boxed(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_getZetaDeltaFVarIds___boxed(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l_Lean_Meta_getZetaFVarIds(x_1); +x_2 = l_Lean_Meta_getZetaDeltaFVarIds(x_1); lean_dec(x_1); return x_2; } @@ -12916,7 +12916,7 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Meta_withConfig___rarg), 5, 0); return x_2; } } -LEAN_EXPORT lean_object* l_Lean_Meta_withTrackingZeta___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +LEAN_EXPORT lean_object* l_Lean_Meta_withTrackingZetaDelta___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { _start: { uint8_t x_8; @@ -13031,14 +13031,14 @@ return x_48; } } } -LEAN_EXPORT lean_object* l_Lean_Meta_withTrackingZeta___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +LEAN_EXPORT lean_object* l_Lean_Meta_withTrackingZetaDelta___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; x_5 = lean_ctor_get(x_2, 1); lean_inc(x_5); lean_dec(x_2); -x_6 = lean_alloc_closure((void*)(l_Lean_Meta_withTrackingZeta___rarg___lambda__1), 7, 1); +x_6 = lean_alloc_closure((void*)(l_Lean_Meta_withTrackingZetaDelta___rarg___lambda__1), 7, 1); lean_closure_set(x_6, 0, x_4); x_7 = lean_ctor_get(x_1, 0); lean_inc(x_7); @@ -13051,11 +13051,11 @@ x_11 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_8, x_10); return x_11; } } -LEAN_EXPORT lean_object* l_Lean_Meta_withTrackingZeta(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_withTrackingZetaDelta(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_Lean_Meta_withTrackingZeta___rarg), 4, 0); +x_2 = lean_alloc_closure((void*)(l_Lean_Meta_withTrackingZetaDelta___rarg), 4, 0); return x_2; } } @@ -39414,7 +39414,7 @@ l_Lean_Meta_Config_proofIrrelevance___default = _init_l_Lean_Meta_Config_proofIr l_Lean_Meta_Config_assignSyntheticOpaque___default = _init_l_Lean_Meta_Config_assignSyntheticOpaque___default(); l_Lean_Meta_Config_offsetCnstrs___default = _init_l_Lean_Meta_Config_offsetCnstrs___default(); l_Lean_Meta_Config_transparency___default = _init_l_Lean_Meta_Config_transparency___default(); -l_Lean_Meta_Config_trackZeta___default = _init_l_Lean_Meta_Config_trackZeta___default(); +l_Lean_Meta_Config_trackZetaDelta___default = _init_l_Lean_Meta_Config_trackZetaDelta___default(); l_Lean_Meta_Config_etaStruct___default = _init_l_Lean_Meta_Config_etaStruct___default(); l_Lean_Meta_ParamInfo_binderInfo___default = _init_l_Lean_Meta_ParamInfo_binderInfo___default(); l_Lean_Meta_ParamInfo_hasFwdDeps___default = _init_l_Lean_Meta_ParamInfo_hasFwdDeps___default(); @@ -39526,8 +39526,8 @@ l_Lean_Meta_State_mctx___default = _init_l_Lean_Meta_State_mctx___default(); lean_mark_persistent(l_Lean_Meta_State_mctx___default); l_Lean_Meta_State_cache___default = _init_l_Lean_Meta_State_cache___default(); lean_mark_persistent(l_Lean_Meta_State_cache___default); -l_Lean_Meta_State_zetaFVarIds___default = _init_l_Lean_Meta_State_zetaFVarIds___default(); -lean_mark_persistent(l_Lean_Meta_State_zetaFVarIds___default); +l_Lean_Meta_State_zetaDeltaFVarIds___default = _init_l_Lean_Meta_State_zetaDeltaFVarIds___default(); +lean_mark_persistent(l_Lean_Meta_State_zetaDeltaFVarIds___default); l_Lean_Meta_State_postponed___default___closed__1 = _init_l_Lean_Meta_State_postponed___default___closed__1(); lean_mark_persistent(l_Lean_Meta_State_postponed___default___closed__1); l_Lean_Meta_State_postponed___default___closed__2 = _init_l_Lean_Meta_State_postponed___default___closed__2(); diff --git a/stage0/stdlib/Lean/Meta/Closure.c b/stage0/stdlib/Lean/Meta/Closure.c index 49a4324f20..01a9444ece 100644 --- a/stage0/stdlib/Lean/Meta/Closure.c +++ b/stage0/stdlib/Lean/Meta/Closure.c @@ -60,7 +60,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_mkAuxDefinition___lambda__1___boxed(lean_ob LEAN_EXPORT lean_object* l_Lean_AssocList_foldlM___at_Lean_Meta_Closure_visitLevel___spec__7(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_mkFreshFVarId___at_Lean_Meta_Closure_collectExprAux___spec__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Closure_pushFVarArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_resetZetaFVarIds___rarg(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_Closure_collectLevelAux___closed__10; LEAN_EXPORT lean_object* l_Lean_Meta_Closure_pushToProcess(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_Closure_collectLevelAux___closed__6; @@ -81,6 +80,7 @@ size_t lean_usize_of_nat(lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Closure_process___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Closure_State_visitedExpr___default; lean_object* lean_expr_abstract(lean_object*, lean_object*); +lean_object* l_Lean_Meta_resetZetaDeltaFVarIds___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_reverse___rarg(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Closure_pickNextToProcess_x3f___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_Closure_instInhabitedToProcessElement___closed__1; @@ -102,7 +102,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Closure_mkNextUserName___rarg(lean_object*, lean_object* l_Lean_FVarId_getDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Closure_mkBinding___spec__1(size_t, size_t, lean_object*); lean_object* l_Lean_Expr_forallE___override(lean_object*, lean_object*, lean_object*, uint8_t); -lean_object* l_Lean_Meta_getZetaFVarIds___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_st_ref_get(lean_object*, lean_object*); lean_object* lean_array_pop(lean_object*); LEAN_EXPORT lean_object* l_Lean_RBNode_findCore___at_Lean_Meta_Closure_process___spec__1(lean_object*, lean_object*); @@ -135,6 +134,7 @@ lean_object* l_Lean_HashMap_insert___at_Lean_instantiateExprMVars___spec__3(lean LEAN_EXPORT lean_object* l_Lean_Meta_Closure_preprocess(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Closure_pickNextToProcess_x3f___boxed(lean_object*); uint8_t l_Lean_Environment_hasUnsafe(lean_object*, lean_object*); +lean_object* l_Lean_Meta_getZetaDeltaFVarIds___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_AssocList_find_x3f___at_Lean_Meta_Closure_visitLevel___spec__2(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Nat_foldRev___at_Lean_Meta_Closure_mkBinding___spec__2(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Closure_mkLambda(lean_object*, lean_object*); @@ -9104,7 +9104,7 @@ x_41 = lean_ctor_get(x_21, 1); lean_dec(x_41); x_42 = lean_ctor_get(x_21, 0); lean_dec(x_42); -x_43 = l_Lean_Meta_getZetaFVarIds___rarg(x_4, x_5, x_6, x_36); +x_43 = l_Lean_Meta_getZetaDeltaFVarIds___rarg(x_4, x_5, x_6, x_36); x_44 = lean_ctor_get(x_43, 0); lean_inc(x_44); x_45 = lean_ctor_get(x_43, 1); @@ -9513,7 +9513,7 @@ lean_inc(x_160); lean_inc(x_159); lean_inc(x_158); lean_dec(x_21); -x_161 = l_Lean_Meta_getZetaFVarIds___rarg(x_4, x_5, x_6, x_36); +x_161 = l_Lean_Meta_getZetaDeltaFVarIds___rarg(x_4, x_5, x_6, x_36); x_162 = lean_ctor_get(x_161, 0); lean_inc(x_162); x_163 = lean_ctor_get(x_161, 1); @@ -10481,7 +10481,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Closure_mkValueTypeClosureAux(lean_object* _start: { lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; -x_10 = l_Lean_Meta_resetZetaFVarIds___rarg(x_6, x_7, x_8, x_9); +x_10 = l_Lean_Meta_resetZetaDeltaFVarIds___rarg(x_6, x_7, x_8, x_9); x_11 = lean_ctor_get(x_5, 0); lean_inc(x_11); x_12 = lean_ctor_get(x_10, 1); diff --git a/stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c b/stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c index c43fcd97ed..d06aba28da 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c @@ -2841,7 +2841,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Sim _start: { uint8_t x_9; -x_9 = lean_ctor_get_uint8(x_1, sizeof(void*)*2 + 3); +x_9 = lean_ctor_get_uint8(x_1, sizeof(void*)*2 + 16); if (x_9 == 0) { lean_object* x_10; uint8_t x_11; diff --git a/stage0/stdlib/Lean/Meta/WHNF.c b/stage0/stdlib/Lean/Meta/WHNF.c index 2dd7d79230..6e5b3fdca8 100644 --- a/stage0/stdlib/Lean/Meta/WHNF.c +++ b/stage0/stdlib/Lean/Meta/WHNF.c @@ -14379,7 +14379,7 @@ return x_19; else { uint8_t x_20; -x_20 = lean_ctor_get_uint8(x_3, 3); +x_20 = lean_ctor_get_uint8(x_3, 4); if (x_20 == 0) { uint8_t x_21; @@ -19547,7 +19547,7 @@ return x_17; else { uint8_t x_18; -x_18 = lean_ctor_get_uint8(x_3, 3); +x_18 = lean_ctor_get_uint8(x_3, 4); if (x_18 == 0) { uint8_t x_19; @@ -24780,7 +24780,7 @@ return x_17; else { uint8_t x_18; -x_18 = lean_ctor_get_uint8(x_3, 3); +x_18 = lean_ctor_get_uint8(x_3, 4); if (x_18 == 0) { uint8_t x_19; @@ -33898,7 +33898,7 @@ return x_16; else { uint8_t x_17; -x_17 = lean_ctor_get_uint8(x_2, 3); +x_17 = lean_ctor_get_uint8(x_2, 4); if (x_17 == 0) { uint8_t x_18;