From 91d48c915099dabb407e953c43f8ca810f8a590e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 5 Jul 2022 14:29:45 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Lean/Elab/App.lean | 4 + stage0/src/Lean/Elab/Term.lean | 7 +- stage0/stdlib/Lean/Elab/App.c | 1113 +++++++++++++------------------- stage0/stdlib/Lean/Elab/Term.c | 267 +++++--- 4 files changed, 632 insertions(+), 759 deletions(-) diff --git a/stage0/src/Lean/Elab/App.lean b/stage0/src/Lean/Elab/App.lean index 23b3d3f9b1..708eece8bc 100644 --- a/stage0/src/Lean/Elab/App.lean +++ b/stage0/src/Lean/Elab/App.lean @@ -658,6 +658,10 @@ private partial def consumeImplicits (stx : Syntax) (e eType : Expr) (hasArgs : private partial def resolveLValLoop (lval : LVal) (e eType : Expr) (previousExceptions : Array Exception) (hasArgs : Bool) : TermElabM (Expr × LValResolution) := do let (e, eType) ← consumeImplicits lval.getRef e eType hasArgs tryPostponeIfMVar eType + /- If `eType` is still a metavariable application, we try to apply default instances to "unblock" it. -/ + if (← isMVarApp eType) then + synthesizeSyntheticMVarsUsingDefault + let eType ← instantiateMVars eType try let lvalRes ← resolveLValAux e eType lval return (e, lvalRes) diff --git a/stage0/src/Lean/Elab/Term.lean b/stage0/src/Lean/Elab/Term.lean index 6a5a2d5ce5..d8b57fba80 100644 --- a/stage0/src/Lean/Elab/Term.lean +++ b/stage0/src/Lean/Elab/Term.lean @@ -992,10 +992,13 @@ def tryPostpone : TermElabM Unit := do if (← read).mayPostpone then throwPostpone +/-- Return `true` if `e` reduces (by unfolding only `[reducible]` declarations) to `?m ...` -/ +def isMVarApp (e : Expr) : TermElabM Bool := + return (← whnfR e).getAppFn.isMVar + /-- If `mayPostpone == true` and `e`'s head is a metavariable, throw `Exception.postpone`. -/ def tryPostponeIfMVar (e : Expr) : TermElabM Unit := do - let e ← whnfR e - if e.getAppFn.isMVar then + if (← isMVarApp e) then tryPostpone /-- If `e? = some e`, then `tryPostponeIfMVar e`, otherwise it is just `tryPostpone`. -/ diff --git a/stage0/stdlib/Lean/Elab/App.c b/stage0/stdlib/Lean/Elab/App.c index e274392c48..5106a87e69 100644 --- a/stage0/stdlib/Lean/Elab/App.c +++ b/stage0/stdlib/Lean/Elab/App.c @@ -68,6 +68,7 @@ lean_object* l_Lean_LocalDecl_userName(lean_object*); static lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValAux___lambda__3___closed__8; LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitApp___at___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_anyNamedArgDependsOnCurrent___spec__21(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_findMethodAlias_x3f(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop___lambda__1(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* l_Lean_Meta_whnfForall(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppAux___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_App_0__Lean_Elab_Term_findMethod_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -149,6 +150,7 @@ uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_getForallBody___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabAppArgs___lambda__2(lean_object*, lean_object*, lean_object*, uint8_t, 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___regBuiltin_Lean_Elab_Term_elabApp___closed__1; +LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop___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_object*); LEAN_EXPORT lean_object* l_Std_PersistentArray_anyMAux___at___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_anyNamedArgDependsOnCurrent___spec__23___boxed(lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_propagateExpectedType___lambda__2___closed__2; lean_object* lean_st_ref_get(lean_object*, lean_object*); @@ -527,6 +529,7 @@ LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_v LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_elabNamedPattern_docString(lean_object*); static lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg___lambda__1___closed__2; static lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_tryCoeFun_x3f___closed__6; +lean_object* l_Lean_Elab_Term_isMVarApp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__18; static lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__15; static lean_object* l___regBuiltin_Lean_Elab_Term_elabIdent_declRange___closed__3; @@ -614,6 +617,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs LEAN_EXPORT lean_object* l_Std_PersistentArray_anyM___at___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_anyNamedArgDependsOnCurrent___spec__38___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Elab_App_0__Lean_Elab_Term_throwLValError___spec__1(lean_object*); static lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___lambda__3___closed__3; +lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVarsUsingDefault(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_synthesizePendingAndNormalizeFunType___closed__2; static lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__8; lean_object* l_Lean_Syntax_getPos_x3f(lean_object*, uint8_t); @@ -750,7 +754,7 @@ uint8_t l_Lean_Expr_isFVar(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_finalize___lambda__1(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_Elab_App_0__Lean_Elab_Term_ElabAppArgs_getForallBody___lambda__1___boxed(lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_mkProjAndCheck___closed__7; -LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_13928_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_14008_(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_5_(lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppAux(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -20186,357 +20190,363 @@ return x_24; } } } -LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t 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, lean_object* x_12) { +LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t 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, lean_object* x_12, lean_object* x_13) { _start: { -lean_object* x_13; lean_object* x_14; lean_object* x_18; lean_object* x_19; -x_18 = l_Lean_Elab_Term_LVal_getRef(x_1); -lean_inc(x_11); -lean_inc(x_10); -lean_inc(x_9); -lean_inc(x_8); -lean_inc(x_7); -lean_inc(x_6); -x_19 = l___private_Lean_Elab_App_0__Lean_Elab_Term_consumeImplicits(x_18, x_2, x_3, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); -if (lean_obj_tag(x_19) == 0) -{ -lean_object* x_20; lean_object* x_21; uint8_t x_22; +lean_object* x_14; lean_object* x_15; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; +x_19 = l_Lean_instantiateMVars___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__1(x_1, x_7, x_8, x_9, x_10, x_11, x_12, x_13); x_20 = lean_ctor_get(x_19, 0); lean_inc(x_20); x_21 = lean_ctor_get(x_19, 1); lean_inc(x_21); lean_dec(x_19); -x_22 = !lean_is_exclusive(x_20); -if (x_22 == 0) -{ -lean_object* x_23; lean_object* x_24; lean_object* x_25; -x_23 = lean_ctor_get(x_20, 0); -x_24 = lean_ctor_get(x_20, 1); -lean_inc(x_11); -lean_inc(x_10); -lean_inc(x_9); -lean_inc(x_8); -lean_inc(x_6); -lean_inc(x_24); -x_25 = l_Lean_Elab_Term_tryPostponeIfMVar(x_24, x_6, x_7, x_8, x_9, x_10, x_11, x_21); -if (lean_obj_tag(x_25) == 0) -{ -lean_object* x_26; lean_object* x_27; -x_26 = lean_ctor_get(x_25, 1); -lean_inc(x_26); -lean_dec(x_25); +lean_inc(x_12); lean_inc(x_11); lean_inc(x_10); lean_inc(x_9); lean_inc(x_8); lean_inc(x_7); -lean_inc(x_6); -lean_inc(x_1); -lean_inc(x_24); -lean_inc(x_23); -x_27 = l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValAux(x_23, x_24, x_1, x_6, x_7, x_8, x_9, x_10, x_11, x_26); -if (lean_obj_tag(x_27) == 0) +lean_inc(x_3); +lean_inc(x_20); +lean_inc(x_2); +x_22 = l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValAux(x_2, x_20, x_3, x_7, x_8, x_9, x_10, x_11, x_12, x_21); +if (lean_obj_tag(x_22) == 0) { -lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; -lean_dec(x_24); +lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; +lean_dec(x_20); +lean_dec(x_12); lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); lean_dec(x_7); -lean_dec(x_6); lean_dec(x_4); -lean_dec(x_1); -x_28 = lean_ctor_get(x_27, 0); -lean_inc(x_28); -x_29 = lean_ctor_get(x_27, 1); -lean_inc(x_29); -lean_dec(x_27); -lean_ctor_set(x_20, 1, x_28); -x_30 = lean_box(0); -x_31 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_31, 0, x_20); -lean_ctor_set(x_31, 1, x_30); -x_13 = x_31; -x_14 = x_29; -goto block_17; +lean_dec(x_3); +x_23 = lean_ctor_get(x_22, 0); +lean_inc(x_23); +x_24 = lean_ctor_get(x_22, 1); +lean_inc(x_24); +lean_dec(x_22); +x_25 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_25, 0, x_2); +lean_ctor_set(x_25, 1, x_23); +x_26 = lean_box(0); +x_27 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_27, 0, x_25); +lean_ctor_set(x_27, 1, x_26); +x_14 = x_27; +x_15 = x_24; +goto block_18; } else { -lean_object* x_32; lean_object* x_33; lean_object* x_34; -lean_free_object(x_20); -x_32 = lean_ctor_get(x_27, 0); -lean_inc(x_32); -x_33 = lean_ctor_get(x_27, 1); -lean_inc(x_33); -lean_dec(x_27); +lean_object* x_28; lean_object* x_29; lean_object* x_30; +x_28 = lean_ctor_get(x_22, 0); +lean_inc(x_28); +x_29 = lean_ctor_get(x_22, 1); +lean_inc(x_29); +lean_dec(x_22); +lean_inc(x_12); lean_inc(x_11); lean_inc(x_10); lean_inc(x_9); -lean_inc(x_8); -x_34 = l_Lean_Meta_unfoldDefinition_x3f(x_24, x_8, x_9, x_10, x_11, x_33); -if (lean_obj_tag(x_34) == 0) +x_30 = l_Lean_Meta_unfoldDefinition_x3f(x_20, x_9, x_10, x_11, x_12, x_29); +if (lean_obj_tag(x_30) == 0) { -lean_object* x_35; -x_35 = lean_ctor_get(x_34, 0); -lean_inc(x_35); -if (lean_obj_tag(x_35) == 0) +lean_object* x_31; +x_31 = lean_ctor_get(x_30, 0); +lean_inc(x_31); +if (lean_obj_tag(x_31) == 0) { -uint8_t x_36; -lean_dec(x_23); -lean_dec(x_1); -x_36 = !lean_is_exclusive(x_34); -if (x_36 == 0) +uint8_t x_32; +lean_dec(x_3); +lean_dec(x_2); +x_32 = !lean_is_exclusive(x_30); +if (x_32 == 0) { -lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; uint8_t x_41; -x_37 = lean_ctor_get(x_34, 1); -x_38 = lean_ctor_get(x_34, 0); -lean_dec(x_38); -x_39 = lean_array_get_size(x_4); -x_40 = lean_unsigned_to_nat(0u); -x_41 = lean_nat_dec_lt(x_40, x_39); -if (x_41 == 0) +lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; uint8_t x_37; +x_33 = lean_ctor_get(x_30, 1); +x_34 = lean_ctor_get(x_30, 0); +lean_dec(x_34); +x_35 = lean_array_get_size(x_4); +x_36 = lean_unsigned_to_nat(0u); +x_37 = lean_nat_dec_lt(x_36, x_35); +if (x_37 == 0) { -lean_dec(x_39); +lean_dec(x_35); +lean_dec(x_12); lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); lean_dec(x_7); -lean_dec(x_6); lean_dec(x_4); -lean_ctor_set_tag(x_34, 1); -lean_ctor_set(x_34, 0, x_32); -return x_34; +lean_ctor_set_tag(x_30, 1); +lean_ctor_set(x_30, 0, x_28); +return x_30; } else { -uint8_t x_42; -x_42 = lean_nat_dec_le(x_39, x_39); -if (x_42 == 0) +uint8_t x_38; +x_38 = lean_nat_dec_le(x_35, x_35); +if (x_38 == 0) { -lean_dec(x_39); +lean_dec(x_35); +lean_dec(x_12); lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); lean_dec(x_7); -lean_dec(x_6); lean_dec(x_4); -lean_ctor_set_tag(x_34, 1); -lean_ctor_set(x_34, 0, x_32); -return x_34; +lean_ctor_set_tag(x_30, 1); +lean_ctor_set(x_30, 0, x_28); +return x_30; } else { -size_t x_43; size_t x_44; lean_object* x_45; lean_object* x_46; -lean_free_object(x_34); -x_43 = 0; -x_44 = lean_usize_of_nat(x_39); -lean_dec(x_39); -x_45 = lean_box(0); -x_46 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop___spec__1(x_4, x_43, x_44, x_45, x_6, x_7, x_8, x_9, x_10, x_11, x_37); +size_t x_39; size_t x_40; lean_object* x_41; lean_object* x_42; +lean_free_object(x_30); +x_39 = 0; +x_40 = lean_usize_of_nat(x_35); +lean_dec(x_35); +x_41 = lean_box(0); +x_42 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop___spec__1(x_4, x_39, x_40, x_41, x_7, x_8, x_9, x_10, x_11, x_12, x_33); lean_dec(x_4); -if (lean_obj_tag(x_46) == 0) +if (lean_obj_tag(x_42) == 0) { -uint8_t x_47; -x_47 = !lean_is_exclusive(x_46); -if (x_47 == 0) +uint8_t x_43; +x_43 = !lean_is_exclusive(x_42); +if (x_43 == 0) { -lean_object* x_48; -x_48 = lean_ctor_get(x_46, 0); -lean_dec(x_48); -lean_ctor_set_tag(x_46, 1); -lean_ctor_set(x_46, 0, x_32); +lean_object* x_44; +x_44 = lean_ctor_get(x_42, 0); +lean_dec(x_44); +lean_ctor_set_tag(x_42, 1); +lean_ctor_set(x_42, 0, x_28); +return x_42; +} +else +{ +lean_object* x_45; lean_object* x_46; +x_45 = lean_ctor_get(x_42, 1); +lean_inc(x_45); +lean_dec(x_42); +x_46 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_46, 0, x_28); +lean_ctor_set(x_46, 1, x_45); return x_46; } +} else { -lean_object* x_49; lean_object* x_50; -x_49 = lean_ctor_get(x_46, 1); +uint8_t x_47; +lean_dec(x_28); +x_47 = !lean_is_exclusive(x_42); +if (x_47 == 0) +{ +return x_42; +} +else +{ +lean_object* x_48; lean_object* x_49; lean_object* x_50; +x_48 = lean_ctor_get(x_42, 0); +x_49 = lean_ctor_get(x_42, 1); lean_inc(x_49); -lean_dec(x_46); +lean_inc(x_48); +lean_dec(x_42); x_50 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_50, 0, x_32); +lean_ctor_set(x_50, 0, x_48); lean_ctor_set(x_50, 1, x_49); return x_50; } } -else -{ -uint8_t x_51; -lean_dec(x_32); -x_51 = !lean_is_exclusive(x_46); -if (x_51 == 0) -{ -return x_46; -} -else -{ -lean_object* x_52; lean_object* x_53; lean_object* x_54; -x_52 = lean_ctor_get(x_46, 0); -x_53 = lean_ctor_get(x_46, 1); -lean_inc(x_53); -lean_inc(x_52); -lean_dec(x_46); -x_54 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_54, 0, x_52); -lean_ctor_set(x_54, 1, x_53); -return x_54; -} -} } } } else { -lean_object* x_55; lean_object* x_56; lean_object* x_57; uint8_t x_58; -x_55 = lean_ctor_get(x_34, 1); -lean_inc(x_55); -lean_dec(x_34); -x_56 = lean_array_get_size(x_4); -x_57 = lean_unsigned_to_nat(0u); -x_58 = lean_nat_dec_lt(x_57, x_56); -if (x_58 == 0) +lean_object* x_51; lean_object* x_52; lean_object* x_53; uint8_t x_54; +x_51 = lean_ctor_get(x_30, 1); +lean_inc(x_51); +lean_dec(x_30); +x_52 = lean_array_get_size(x_4); +x_53 = lean_unsigned_to_nat(0u); +x_54 = lean_nat_dec_lt(x_53, x_52); +if (x_54 == 0) { -lean_object* x_59; -lean_dec(x_56); +lean_object* x_55; +lean_dec(x_52); +lean_dec(x_12); lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); lean_dec(x_7); -lean_dec(x_6); lean_dec(x_4); -x_59 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_59, 0, x_32); -lean_ctor_set(x_59, 1, x_55); -return x_59; +x_55 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_55, 0, x_28); +lean_ctor_set(x_55, 1, x_51); +return x_55; } else { -uint8_t x_60; -x_60 = lean_nat_dec_le(x_56, x_56); -if (x_60 == 0) +uint8_t x_56; +x_56 = lean_nat_dec_le(x_52, x_52); +if (x_56 == 0) { -lean_object* x_61; -lean_dec(x_56); +lean_object* x_57; +lean_dec(x_52); +lean_dec(x_12); lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); lean_dec(x_7); -lean_dec(x_6); lean_dec(x_4); -x_61 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_61, 0, x_32); -lean_ctor_set(x_61, 1, x_55); -return x_61; +x_57 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_57, 0, x_28); +lean_ctor_set(x_57, 1, x_51); +return x_57; } else { -size_t x_62; size_t x_63; lean_object* x_64; lean_object* x_65; -x_62 = 0; -x_63 = lean_usize_of_nat(x_56); -lean_dec(x_56); -x_64 = lean_box(0); -x_65 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop___spec__1(x_4, x_62, x_63, x_64, x_6, x_7, x_8, x_9, x_10, x_11, x_55); +size_t x_58; size_t x_59; lean_object* x_60; lean_object* x_61; +x_58 = 0; +x_59 = lean_usize_of_nat(x_52); +lean_dec(x_52); +x_60 = lean_box(0); +x_61 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop___spec__1(x_4, x_58, x_59, x_60, x_7, x_8, x_9, x_10, x_11, x_12, x_51); lean_dec(x_4); -if (lean_obj_tag(x_65) == 0) +if (lean_obj_tag(x_61) == 0) { -lean_object* x_66; lean_object* x_67; lean_object* x_68; -x_66 = lean_ctor_get(x_65, 1); -lean_inc(x_66); -if (lean_is_exclusive(x_65)) { - lean_ctor_release(x_65, 0); - lean_ctor_release(x_65, 1); - x_67 = x_65; +lean_object* x_62; lean_object* x_63; lean_object* x_64; +x_62 = lean_ctor_get(x_61, 1); +lean_inc(x_62); +if (lean_is_exclusive(x_61)) { + lean_ctor_release(x_61, 0); + lean_ctor_release(x_61, 1); + x_63 = x_61; } else { - lean_dec_ref(x_65); + lean_dec_ref(x_61); + x_63 = lean_box(0); +} +if (lean_is_scalar(x_63)) { + x_64 = lean_alloc_ctor(1, 2, 0); +} else { + x_64 = x_63; + lean_ctor_set_tag(x_64, 1); +} +lean_ctor_set(x_64, 0, x_28); +lean_ctor_set(x_64, 1, x_62); +return x_64; +} +else +{ +lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; +lean_dec(x_28); +x_65 = lean_ctor_get(x_61, 0); +lean_inc(x_65); +x_66 = lean_ctor_get(x_61, 1); +lean_inc(x_66); +if (lean_is_exclusive(x_61)) { + lean_ctor_release(x_61, 0); + lean_ctor_release(x_61, 1); + x_67 = x_61; +} else { + lean_dec_ref(x_61); x_67 = lean_box(0); } if (lean_is_scalar(x_67)) { x_68 = lean_alloc_ctor(1, 2, 0); } else { x_68 = x_67; - lean_ctor_set_tag(x_68, 1); } -lean_ctor_set(x_68, 0, x_32); +lean_ctor_set(x_68, 0, x_65); lean_ctor_set(x_68, 1, x_66); return x_68; } +} +} +} +} else { lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; -lean_dec(x_32); -x_69 = lean_ctor_get(x_65, 0); +x_69 = lean_ctor_get(x_30, 1); lean_inc(x_69); -x_70 = lean_ctor_get(x_65, 1); +lean_dec(x_30); +x_70 = lean_ctor_get(x_31, 0); lean_inc(x_70); -if (lean_is_exclusive(x_65)) { - lean_ctor_release(x_65, 0); - lean_ctor_release(x_65, 1); - x_71 = x_65; -} else { - lean_dec_ref(x_65); - x_71 = lean_box(0); -} -if (lean_is_scalar(x_71)) { - x_72 = lean_alloc_ctor(1, 2, 0); -} else { - x_72 = x_71; -} -lean_ctor_set(x_72, 0, x_69); -lean_ctor_set(x_72, 1, x_70); -return x_72; -} -} -} -} +lean_dec(x_31); +x_71 = lean_array_push(x_4, x_28); +x_72 = l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop(x_3, x_2, x_70, x_71, x_5, x_7, x_8, x_9, x_10, x_11, x_12, x_69); +if (lean_obj_tag(x_72) == 0) +{ +lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; +x_73 = lean_ctor_get(x_72, 0); +lean_inc(x_73); +x_74 = lean_ctor_get(x_72, 1); +lean_inc(x_74); +lean_dec(x_72); +x_75 = lean_box(0); +x_76 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_76, 0, x_73); +lean_ctor_set(x_76, 1, x_75); +x_14 = x_76; +x_15 = x_74; +goto block_18; } else { -lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; -x_73 = lean_ctor_get(x_34, 1); -lean_inc(x_73); -lean_dec(x_34); -x_74 = lean_ctor_get(x_35, 0); -lean_inc(x_74); -lean_dec(x_35); -x_75 = lean_array_push(x_4, x_32); -x_76 = l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop(x_1, x_23, x_74, x_75, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_73); -if (lean_obj_tag(x_76) == 0) +uint8_t x_77; +x_77 = !lean_is_exclusive(x_72); +if (x_77 == 0) { -lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; -x_77 = lean_ctor_get(x_76, 0); -lean_inc(x_77); -x_78 = lean_ctor_get(x_76, 1); +return x_72; +} +else +{ +lean_object* x_78; lean_object* x_79; lean_object* x_80; +x_78 = lean_ctor_get(x_72, 0); +x_79 = lean_ctor_get(x_72, 1); +lean_inc(x_79); lean_inc(x_78); -lean_dec(x_76); -x_79 = lean_box(0); -x_80 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_80, 0, x_77); +lean_dec(x_72); +x_80 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_80, 0, x_78); lean_ctor_set(x_80, 1, x_79); -x_13 = x_80; -x_14 = x_78; -goto block_17; +return x_80; +} +} +} } else { uint8_t x_81; -x_81 = !lean_is_exclusive(x_76); +lean_dec(x_28); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +x_81 = !lean_is_exclusive(x_30); if (x_81 == 0) { -return x_76; +return x_30; } else { lean_object* x_82; lean_object* x_83; lean_object* x_84; -x_82 = lean_ctor_get(x_76, 0); -x_83 = lean_ctor_get(x_76, 1); +x_82 = lean_ctor_get(x_30, 0); +x_83 = lean_ctor_get(x_30, 1); lean_inc(x_83); lean_inc(x_82); -lean_dec(x_76); +lean_dec(x_30); x_84 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_84, 0, x_82); lean_ctor_set(x_84, 1, x_83); @@ -20544,335 +20554,110 @@ return x_84; } } } -} -else +block_18: { -uint8_t x_85; -lean_dec(x_32); -lean_dec(x_23); -lean_dec(x_11); -lean_dec(x_10); -lean_dec(x_9); -lean_dec(x_8); -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_4); -lean_dec(x_1); -x_85 = !lean_is_exclusive(x_34); -if (x_85 == 0) +lean_object* x_16; lean_object* x_17; +x_16 = lean_ctor_get(x_14, 0); +lean_inc(x_16); +lean_dec(x_14); +x_17 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_17, 0, x_16); +lean_ctor_set(x_17, 1, x_15); +return x_17; +} +} +} +LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t 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, lean_object* x_12) { +_start: { -return x_34; -} -else -{ -lean_object* x_86; lean_object* x_87; lean_object* x_88; -x_86 = lean_ctor_get(x_34, 0); -x_87 = lean_ctor_get(x_34, 1); -lean_inc(x_87); -lean_inc(x_86); -lean_dec(x_34); -x_88 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_88, 0, x_86); -lean_ctor_set(x_88, 1, x_87); -return x_88; -} -} -} -} -else -{ -uint8_t x_89; -lean_free_object(x_20); -lean_dec(x_24); -lean_dec(x_23); -lean_dec(x_11); -lean_dec(x_10); -lean_dec(x_9); -lean_dec(x_8); -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_4); -lean_dec(x_1); -x_89 = !lean_is_exclusive(x_25); -if (x_89 == 0) -{ -return x_25; -} -else -{ -lean_object* x_90; lean_object* x_91; lean_object* x_92; -x_90 = lean_ctor_get(x_25, 0); -x_91 = lean_ctor_get(x_25, 1); -lean_inc(x_91); -lean_inc(x_90); -lean_dec(x_25); -x_92 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_92, 0, x_90); -lean_ctor_set(x_92, 1, x_91); -return x_92; -} -} -} -else -{ -lean_object* x_93; lean_object* x_94; lean_object* x_95; -x_93 = lean_ctor_get(x_20, 0); -x_94 = lean_ctor_get(x_20, 1); -lean_inc(x_94); -lean_inc(x_93); -lean_dec(x_20); -lean_inc(x_11); -lean_inc(x_10); -lean_inc(x_9); -lean_inc(x_8); -lean_inc(x_6); -lean_inc(x_94); -x_95 = l_Lean_Elab_Term_tryPostponeIfMVar(x_94, x_6, x_7, x_8, x_9, x_10, x_11, x_21); -if (lean_obj_tag(x_95) == 0) -{ -lean_object* x_96; lean_object* x_97; -x_96 = lean_ctor_get(x_95, 1); -lean_inc(x_96); -lean_dec(x_95); +lean_object* x_13; lean_object* x_14; +x_13 = l_Lean_Elab_Term_LVal_getRef(x_1); lean_inc(x_11); lean_inc(x_10); lean_inc(x_9); lean_inc(x_8); lean_inc(x_7); lean_inc(x_6); -lean_inc(x_1); -lean_inc(x_94); -lean_inc(x_93); -x_97 = l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValAux(x_93, x_94, x_1, x_6, x_7, x_8, x_9, x_10, x_11, x_96); -if (lean_obj_tag(x_97) == 0) +x_14 = l___private_Lean_Elab_App_0__Lean_Elab_Term_consumeImplicits(x_13, x_2, x_3, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); +if (lean_obj_tag(x_14) == 0) { -lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; -lean_dec(x_94); -lean_dec(x_11); -lean_dec(x_10); -lean_dec(x_9); -lean_dec(x_8); -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_4); -lean_dec(x_1); -x_98 = lean_ctor_get(x_97, 0); -lean_inc(x_98); -x_99 = lean_ctor_get(x_97, 1); -lean_inc(x_99); -lean_dec(x_97); -x_100 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_100, 0, x_93); -lean_ctor_set(x_100, 1, x_98); -x_101 = lean_box(0); -x_102 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_102, 0, x_100); -lean_ctor_set(x_102, 1, x_101); -x_13 = x_102; -x_14 = x_99; -goto block_17; -} -else -{ -lean_object* x_103; lean_object* x_104; lean_object* x_105; -x_103 = lean_ctor_get(x_97, 0); -lean_inc(x_103); -x_104 = lean_ctor_get(x_97, 1); -lean_inc(x_104); -lean_dec(x_97); +lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; +x_15 = lean_ctor_get(x_14, 0); +lean_inc(x_15); +x_16 = lean_ctor_get(x_14, 1); +lean_inc(x_16); +lean_dec(x_14); +x_17 = lean_ctor_get(x_15, 0); +lean_inc(x_17); +x_18 = lean_ctor_get(x_15, 1); +lean_inc(x_18); +lean_dec(x_15); lean_inc(x_11); lean_inc(x_10); lean_inc(x_9); lean_inc(x_8); -x_105 = l_Lean_Meta_unfoldDefinition_x3f(x_94, x_8, x_9, x_10, x_11, x_104); -if (lean_obj_tag(x_105) == 0) +lean_inc(x_6); +lean_inc(x_18); +x_19 = l_Lean_Elab_Term_tryPostponeIfMVar(x_18, x_6, x_7, x_8, x_9, x_10, x_11, x_16); +if (lean_obj_tag(x_19) == 0) { -lean_object* x_106; -x_106 = lean_ctor_get(x_105, 0); -lean_inc(x_106); -if (lean_obj_tag(x_106) == 0) +lean_object* x_20; lean_object* x_21; +x_20 = lean_ctor_get(x_19, 1); +lean_inc(x_20); +lean_dec(x_19); +lean_inc(x_11); +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_18); +x_21 = l_Lean_Elab_Term_isMVarApp(x_18, x_6, x_7, x_8, x_9, x_10, x_11, x_20); +if (lean_obj_tag(x_21) == 0) { -lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; uint8_t x_111; -lean_dec(x_93); -lean_dec(x_1); -x_107 = lean_ctor_get(x_105, 1); -lean_inc(x_107); -if (lean_is_exclusive(x_105)) { - lean_ctor_release(x_105, 0); - lean_ctor_release(x_105, 1); - x_108 = x_105; -} else { - lean_dec_ref(x_105); - x_108 = lean_box(0); -} -x_109 = lean_array_get_size(x_4); -x_110 = lean_unsigned_to_nat(0u); -x_111 = lean_nat_dec_lt(x_110, x_109); -if (x_111 == 0) +lean_object* x_22; uint8_t x_23; +x_22 = lean_ctor_get(x_21, 0); +lean_inc(x_22); +x_23 = lean_unbox(x_22); +lean_dec(x_22); +if (x_23 == 0) { -lean_object* x_112; -lean_dec(x_109); -lean_dec(x_11); -lean_dec(x_10); -lean_dec(x_9); -lean_dec(x_8); -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_4); -if (lean_is_scalar(x_108)) { - x_112 = lean_alloc_ctor(1, 2, 0); -} else { - x_112 = x_108; - lean_ctor_set_tag(x_112, 1); -} -lean_ctor_set(x_112, 0, x_103); -lean_ctor_set(x_112, 1, x_107); -return x_112; +lean_object* x_24; lean_object* x_25; lean_object* x_26; +x_24 = lean_ctor_get(x_21, 1); +lean_inc(x_24); +lean_dec(x_21); +x_25 = lean_box(0); +x_26 = l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop___lambda__1(x_18, x_17, x_1, x_4, x_5, x_25, x_6, x_7, x_8, x_9, x_10, x_11, x_24); +return x_26; } else { -uint8_t x_113; -x_113 = lean_nat_dec_le(x_109, x_109); -if (x_113 == 0) +lean_object* x_27; lean_object* x_28; +x_27 = lean_ctor_get(x_21, 1); +lean_inc(x_27); +lean_dec(x_21); +lean_inc(x_11); +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +lean_inc(x_6); +x_28 = l_Lean_Elab_Term_synthesizeSyntheticMVarsUsingDefault(x_6, x_7, x_8, x_9, x_10, x_11, x_27); +if (lean_obj_tag(x_28) == 0) { -lean_object* x_114; -lean_dec(x_109); -lean_dec(x_11); -lean_dec(x_10); -lean_dec(x_9); -lean_dec(x_8); -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_4); -if (lean_is_scalar(x_108)) { - x_114 = lean_alloc_ctor(1, 2, 0); -} else { - x_114 = x_108; - lean_ctor_set_tag(x_114, 1); -} -lean_ctor_set(x_114, 0, x_103); -lean_ctor_set(x_114, 1, x_107); -return x_114; +lean_object* x_29; lean_object* x_30; lean_object* x_31; +x_29 = lean_ctor_get(x_28, 0); +lean_inc(x_29); +x_30 = lean_ctor_get(x_28, 1); +lean_inc(x_30); +lean_dec(x_28); +x_31 = l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop___lambda__1(x_18, x_17, x_1, x_4, x_5, x_29, x_6, x_7, x_8, x_9, x_10, x_11, x_30); +lean_dec(x_29); +return x_31; } else { -size_t x_115; size_t x_116; lean_object* x_117; lean_object* x_118; -lean_dec(x_108); -x_115 = 0; -x_116 = lean_usize_of_nat(x_109); -lean_dec(x_109); -x_117 = lean_box(0); -x_118 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop___spec__1(x_4, x_115, x_116, x_117, x_6, x_7, x_8, x_9, x_10, x_11, x_107); -lean_dec(x_4); -if (lean_obj_tag(x_118) == 0) -{ -lean_object* x_119; lean_object* x_120; lean_object* x_121; -x_119 = lean_ctor_get(x_118, 1); -lean_inc(x_119); -if (lean_is_exclusive(x_118)) { - lean_ctor_release(x_118, 0); - lean_ctor_release(x_118, 1); - x_120 = x_118; -} else { - lean_dec_ref(x_118); - x_120 = lean_box(0); -} -if (lean_is_scalar(x_120)) { - x_121 = lean_alloc_ctor(1, 2, 0); -} else { - x_121 = x_120; - lean_ctor_set_tag(x_121, 1); -} -lean_ctor_set(x_121, 0, x_103); -lean_ctor_set(x_121, 1, x_119); -return x_121; -} -else -{ -lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; -lean_dec(x_103); -x_122 = lean_ctor_get(x_118, 0); -lean_inc(x_122); -x_123 = lean_ctor_get(x_118, 1); -lean_inc(x_123); -if (lean_is_exclusive(x_118)) { - lean_ctor_release(x_118, 0); - lean_ctor_release(x_118, 1); - x_124 = x_118; -} else { - lean_dec_ref(x_118); - x_124 = lean_box(0); -} -if (lean_is_scalar(x_124)) { - x_125 = lean_alloc_ctor(1, 2, 0); -} else { - x_125 = x_124; -} -lean_ctor_set(x_125, 0, x_122); -lean_ctor_set(x_125, 1, x_123); -return x_125; -} -} -} -} -else -{ -lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; -x_126 = lean_ctor_get(x_105, 1); -lean_inc(x_126); -lean_dec(x_105); -x_127 = lean_ctor_get(x_106, 0); -lean_inc(x_127); -lean_dec(x_106); -x_128 = lean_array_push(x_4, x_103); -x_129 = l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop(x_1, x_93, x_127, x_128, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_126); -if (lean_obj_tag(x_129) == 0) -{ -lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; -x_130 = lean_ctor_get(x_129, 0); -lean_inc(x_130); -x_131 = lean_ctor_get(x_129, 1); -lean_inc(x_131); -lean_dec(x_129); -x_132 = lean_box(0); -x_133 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_133, 0, x_130); -lean_ctor_set(x_133, 1, x_132); -x_13 = x_133; -x_14 = x_131; -goto block_17; -} -else -{ -lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; -x_134 = lean_ctor_get(x_129, 0); -lean_inc(x_134); -x_135 = lean_ctor_get(x_129, 1); -lean_inc(x_135); -if (lean_is_exclusive(x_129)) { - lean_ctor_release(x_129, 0); - lean_ctor_release(x_129, 1); - x_136 = x_129; -} else { - lean_dec_ref(x_129); - x_136 = lean_box(0); -} -if (lean_is_scalar(x_136)) { - x_137 = lean_alloc_ctor(1, 2, 0); -} else { - x_137 = x_136; -} -lean_ctor_set(x_137, 0, x_134); -lean_ctor_set(x_137, 1, x_135); -return x_137; -} -} -} -else -{ -lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; -lean_dec(x_103); -lean_dec(x_93); +uint8_t x_32; +lean_dec(x_18); +lean_dec(x_17); lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); @@ -20881,34 +20666,32 @@ lean_dec(x_7); lean_dec(x_6); lean_dec(x_4); lean_dec(x_1); -x_138 = lean_ctor_get(x_105, 0); -lean_inc(x_138); -x_139 = lean_ctor_get(x_105, 1); -lean_inc(x_139); -if (lean_is_exclusive(x_105)) { - lean_ctor_release(x_105, 0); - lean_ctor_release(x_105, 1); - x_140 = x_105; -} else { - lean_dec_ref(x_105); - x_140 = lean_box(0); +x_32 = !lean_is_exclusive(x_28); +if (x_32 == 0) +{ +return x_28; } -if (lean_is_scalar(x_140)) { - x_141 = lean_alloc_ctor(1, 2, 0); -} else { - x_141 = x_140; +else +{ +lean_object* x_33; lean_object* x_34; lean_object* x_35; +x_33 = lean_ctor_get(x_28, 0); +x_34 = lean_ctor_get(x_28, 1); +lean_inc(x_34); +lean_inc(x_33); +lean_dec(x_28); +x_35 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_35, 0, x_33); +lean_ctor_set(x_35, 1, x_34); +return x_35; } -lean_ctor_set(x_141, 0, x_138); -lean_ctor_set(x_141, 1, x_139); -return x_141; } } } else { -lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; -lean_dec(x_94); -lean_dec(x_93); +uint8_t x_36; +lean_dec(x_18); +lean_dec(x_17); lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); @@ -20917,32 +20700,31 @@ lean_dec(x_7); lean_dec(x_6); lean_dec(x_4); lean_dec(x_1); -x_142 = lean_ctor_get(x_95, 0); -lean_inc(x_142); -x_143 = lean_ctor_get(x_95, 1); -lean_inc(x_143); -if (lean_is_exclusive(x_95)) { - lean_ctor_release(x_95, 0); - lean_ctor_release(x_95, 1); - x_144 = x_95; -} else { - lean_dec_ref(x_95); - x_144 = lean_box(0); +x_36 = !lean_is_exclusive(x_21); +if (x_36 == 0) +{ +return x_21; } -if (lean_is_scalar(x_144)) { - x_145 = lean_alloc_ctor(1, 2, 0); -} else { - x_145 = x_144; -} -lean_ctor_set(x_145, 0, x_142); -lean_ctor_set(x_145, 1, x_143); -return x_145; +else +{ +lean_object* x_37; lean_object* x_38; lean_object* x_39; +x_37 = lean_ctor_get(x_21, 0); +x_38 = lean_ctor_get(x_21, 1); +lean_inc(x_38); +lean_inc(x_37); +lean_dec(x_21); +x_39 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_39, 0, x_37); +lean_ctor_set(x_39, 1, x_38); +return x_39; } } } else { -uint8_t x_146; +uint8_t x_40; +lean_dec(x_18); +lean_dec(x_17); lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); @@ -20951,35 +20733,55 @@ lean_dec(x_7); lean_dec(x_6); lean_dec(x_4); lean_dec(x_1); -x_146 = !lean_is_exclusive(x_19); -if (x_146 == 0) +x_40 = !lean_is_exclusive(x_19); +if (x_40 == 0) { return x_19; } else { -lean_object* x_147; lean_object* x_148; lean_object* x_149; -x_147 = lean_ctor_get(x_19, 0); -x_148 = lean_ctor_get(x_19, 1); -lean_inc(x_148); -lean_inc(x_147); +lean_object* x_41; lean_object* x_42; lean_object* x_43; +x_41 = lean_ctor_get(x_19, 0); +x_42 = lean_ctor_get(x_19, 1); +lean_inc(x_42); +lean_inc(x_41); lean_dec(x_19); -x_149 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_149, 0, x_147); -lean_ctor_set(x_149, 1, x_148); -return x_149; +x_43 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_43, 0, x_41); +lean_ctor_set(x_43, 1, x_42); +return x_43; } } -block_17: +} +else { -lean_object* x_15; lean_object* x_16; -x_15 = lean_ctor_get(x_13, 0); -lean_inc(x_15); -lean_dec(x_13); -x_16 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_16, 0, x_15); -lean_ctor_set(x_16, 1, x_14); -return x_16; +uint8_t x_44; +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_4); +lean_dec(x_1); +x_44 = !lean_is_exclusive(x_14); +if (x_44 == 0) +{ +return x_14; +} +else +{ +lean_object* x_45; lean_object* x_46; lean_object* x_47; +x_45 = lean_ctor_get(x_14, 0); +x_46 = lean_ctor_get(x_14, 1); +lean_inc(x_46); +lean_inc(x_45); +lean_dec(x_14); +x_47 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_47, 0, x_45); +lean_ctor_set(x_47, 1, x_46); +return x_47; +} } } } @@ -20996,6 +20798,17 @@ lean_dec(x_1); return x_14; } } +LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) { +_start: +{ +uint8_t x_14; lean_object* x_15; +x_14 = lean_unbox(x_5); +lean_dec(x_5); +x_15 = l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop___lambda__1(x_1, x_2, x_3, x_4, x_14, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13); +lean_dec(x_6); +return x_15; +} +} LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValLoop___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) { _start: { @@ -23643,7 +23456,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___lambda__3___closed__1; x_2 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___lambda__3___closed__2; -x_3 = lean_unsigned_to_nat(765u); +x_3 = lean_unsigned_to_nat(769u); x_4 = lean_unsigned_to_nat(8u); x_5 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___lambda__3___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -33163,7 +32976,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___lambda__3___closed__1; x_2 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_App_0__Lean_Elab_Term_mergeFailures___spec__2___closed__1; -x_3 = lean_unsigned_to_nat(972u); +x_3 = lean_unsigned_to_nat(976u); x_4 = lean_unsigned_to_nat(57u); x_5 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___lambda__3___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -33999,7 +33812,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___lambda__3___closed__1; x_2 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppAux___spec__4___closed__1; -x_3 = lean_unsigned_to_nat(987u); +x_3 = lean_unsigned_to_nat(991u); x_4 = lean_unsigned_to_nat(35u); x_5 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___lambda__3___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -34956,7 +34769,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabApp_declRange___clos _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1001u); +x_1 = lean_unsigned_to_nat(1005u); x_2 = lean_unsigned_to_nat(23u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -34968,7 +34781,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabApp_declRange___clos _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1004u); +x_1 = lean_unsigned_to_nat(1008u); x_2 = lean_unsigned_to_nat(90u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -34996,7 +34809,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabApp_declRange___clos _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1001u); +x_1 = lean_unsigned_to_nat(1005u); x_2 = lean_unsigned_to_nat(27u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35008,7 +34821,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabApp_declRange___clos _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1001u); +x_1 = lean_unsigned_to_nat(1005u); x_2 = lean_unsigned_to_nat(34u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35165,7 +34978,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabIdent_declRange___cl _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1009u); +x_1 = lean_unsigned_to_nat(1013u); x_2 = lean_unsigned_to_nat(25u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35177,7 +34990,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabIdent_declRange___cl _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1009u); +x_1 = lean_unsigned_to_nat(1013u); x_2 = lean_unsigned_to_nat(61u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35205,7 +35018,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabIdent_declRange___cl _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1009u); +x_1 = lean_unsigned_to_nat(1013u); x_2 = lean_unsigned_to_nat(29u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35217,7 +35030,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabIdent_declRange___cl _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1009u); +x_1 = lean_unsigned_to_nat(1013u); x_2 = lean_unsigned_to_nat(38u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35341,7 +35154,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern_declRan _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1011u); +x_1 = lean_unsigned_to_nat(1015u); x_2 = lean_unsigned_to_nat(32u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35353,7 +35166,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern_declRan _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1011u); +x_1 = lean_unsigned_to_nat(1015u); x_2 = lean_unsigned_to_nat(75u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35381,7 +35194,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern_declRan _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1011u); +x_1 = lean_unsigned_to_nat(1015u); x_2 = lean_unsigned_to_nat(36u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35393,7 +35206,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNamedPattern_declRan _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1011u); +x_1 = lean_unsigned_to_nat(1015u); x_2 = lean_unsigned_to_nat(52u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35489,7 +35302,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabDotIdent_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1012u); +x_1 = lean_unsigned_to_nat(1016u); x_2 = lean_unsigned_to_nat(28u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35501,7 +35314,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabDotIdent_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1012u); +x_1 = lean_unsigned_to_nat(1016u); x_2 = lean_unsigned_to_nat(67u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35529,7 +35342,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabDotIdent_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1012u); +x_1 = lean_unsigned_to_nat(1016u); x_2 = lean_unsigned_to_nat(32u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35541,7 +35354,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabDotIdent_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1012u); +x_1 = lean_unsigned_to_nat(1016u); x_2 = lean_unsigned_to_nat(44u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35655,7 +35468,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicitUniv_declRan _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1014u); +x_1 = lean_unsigned_to_nat(1018u); x_2 = lean_unsigned_to_nat(32u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35667,7 +35480,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicitUniv_declRan _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1014u); +x_1 = lean_unsigned_to_nat(1018u); x_2 = lean_unsigned_to_nat(75u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35695,7 +35508,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicitUniv_declRan _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1014u); +x_1 = lean_unsigned_to_nat(1018u); x_2 = lean_unsigned_to_nat(36u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35707,7 +35520,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicitUniv_declRan _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1014u); +x_1 = lean_unsigned_to_nat(1018u); x_2 = lean_unsigned_to_nat(52u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -35990,7 +35803,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabPipeProj_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1016u); +x_1 = lean_unsigned_to_nat(1020u); x_2 = lean_unsigned_to_nat(28u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36002,7 +35815,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabPipeProj_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1021u); +x_1 = lean_unsigned_to_nat(1025u); x_2 = lean_unsigned_to_nat(34u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36030,7 +35843,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabPipeProj_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1016u); +x_1 = lean_unsigned_to_nat(1020u); x_2 = lean_unsigned_to_nat(32u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36042,7 +35855,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabPipeProj_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1016u); +x_1 = lean_unsigned_to_nat(1020u); x_2 = lean_unsigned_to_nat(44u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36295,7 +36108,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicit_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1026u); +x_1 = lean_unsigned_to_nat(1030u); x_2 = lean_unsigned_to_nat(28u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36307,7 +36120,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicit_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1032u); +x_1 = lean_unsigned_to_nat(1036u); x_2 = lean_unsigned_to_nat(50u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36335,7 +36148,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicit_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1026u); +x_1 = lean_unsigned_to_nat(1030u); x_2 = lean_unsigned_to_nat(32u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36347,7 +36160,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabExplicit_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1026u); +x_1 = lean_unsigned_to_nat(1030u); x_2 = lean_unsigned_to_nat(44u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36443,7 +36256,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabChoice_declRange___c _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1034u); +x_1 = lean_unsigned_to_nat(1038u); x_2 = lean_unsigned_to_nat(26u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36455,7 +36268,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabChoice_declRange___c _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1034u); +x_1 = lean_unsigned_to_nat(1038u); x_2 = lean_unsigned_to_nat(63u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36483,7 +36296,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabChoice_declRange___c _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1034u); +x_1 = lean_unsigned_to_nat(1038u); x_2 = lean_unsigned_to_nat(30u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36495,7 +36308,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabChoice_declRange___c _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1034u); +x_1 = lean_unsigned_to_nat(1038u); x_2 = lean_unsigned_to_nat(40u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36591,7 +36404,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabProj_declRange___clo _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1035u); +x_1 = lean_unsigned_to_nat(1039u); x_2 = lean_unsigned_to_nat(24u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36603,7 +36416,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabProj_declRange___clo _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1035u); +x_1 = lean_unsigned_to_nat(1039u); x_2 = lean_unsigned_to_nat(59u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36631,7 +36444,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabProj_declRange___clo _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1035u); +x_1 = lean_unsigned_to_nat(1039u); x_2 = lean_unsigned_to_nat(28u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36643,7 +36456,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabProj_declRange___clo _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1035u); +x_1 = lean_unsigned_to_nat(1039u); x_2 = lean_unsigned_to_nat(36u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36739,7 +36552,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabArrayRef_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1036u); +x_1 = lean_unsigned_to_nat(1040u); x_2 = lean_unsigned_to_nat(28u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36751,7 +36564,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabArrayRef_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1036u); +x_1 = lean_unsigned_to_nat(1040u); x_2 = lean_unsigned_to_nat(67u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36779,7 +36592,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabArrayRef_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1036u); +x_1 = lean_unsigned_to_nat(1040u); x_2 = lean_unsigned_to_nat(32u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36791,7 +36604,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabArrayRef_declRange__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1036u); +x_1 = lean_unsigned_to_nat(1040u); x_2 = lean_unsigned_to_nat(44u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36887,7 +36700,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabArrayRefOpt_declRang _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1037u); +x_1 = lean_unsigned_to_nat(1041u); x_2 = lean_unsigned_to_nat(31u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36899,7 +36712,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabArrayRefOpt_declRang _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1037u); +x_1 = lean_unsigned_to_nat(1041u); x_2 = lean_unsigned_to_nat(73u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36927,7 +36740,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabArrayRefOpt_declRang _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1037u); +x_1 = lean_unsigned_to_nat(1041u); x_2 = lean_unsigned_to_nat(35u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -36939,7 +36752,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabArrayRefOpt_declRang _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1037u); +x_1 = lean_unsigned_to_nat(1041u); x_2 = lean_unsigned_to_nat(50u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -37035,7 +36848,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabArrayRefPanic_declRa _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1038u); +x_1 = lean_unsigned_to_nat(1042u); x_2 = lean_unsigned_to_nat(33u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -37047,7 +36860,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabArrayRefPanic_declRa _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1038u); +x_1 = lean_unsigned_to_nat(1042u); x_2 = lean_unsigned_to_nat(77u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -37075,7 +36888,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabArrayRefPanic_declRa _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1038u); +x_1 = lean_unsigned_to_nat(1042u); x_2 = lean_unsigned_to_nat(37u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -37087,7 +36900,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabArrayRefPanic_declRa _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(1038u); +x_1 = lean_unsigned_to_nat(1042u); x_2 = lean_unsigned_to_nat(54u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -37133,7 +36946,7 @@ x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1); return x_4; } } -LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_13928_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_14008_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -37978,7 +37791,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabArrayRefPanic_declRange__ res = l___regBuiltin_Lean_Elab_Term_elabArrayRefPanic_declRange(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_App___hyg_13928_(lean_io_mk_world()); +res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_14008_(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)); diff --git a/stage0/stdlib/Lean/Elab/Term.c b/stage0/stdlib/Lean/Elab/Term.c index 21f2cf6880..367053fd5c 100644 --- a/stage0/stdlib/Lean/Elab/Term.c +++ b/stage0/stdlib/Lean/Elab/Term.c @@ -195,7 +195,6 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean LEAN_EXPORT lean_object* l_Lean_Elab_Term_instInhabitedTermElabResult___rarg(lean_object*); static lean_object* l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__1; static lean_object* l_Lean_Elab_Term_instMonadTermElabM___closed__5; -static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__2; static lean_object* l_Lean_Elab_Term_mkCoe___closed__4; LEAN_EXPORT lean_object* l_Lean_Elab_Term_isMonadApp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTerm___at_Lean_Elab_Term_throwMVarError___spec__2___rarg(lean_object*); @@ -310,6 +309,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_getSyntheticMVarDecl_x3f___lambda__1__ lean_object* l_Std_RBNode_findCore___at___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elimApp___spec__5(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Term_exprToSyntax___closed__4; LEAN_EXPORT lean_object* l_Lean_Elab_Term_ensureType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__2; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_withoutModifyingElabMetaStateWithInfo___spec__14___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_MessageData_ofList(lean_object*); LEAN_EXPORT lean_object* l_Lean_getDelayedMVarAssignment_x3f___at_Lean_Elab_Term_ContainsPendingMVar_visit___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -513,6 +513,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_withMacroExpansionInfo___at_Lean_Elab_Term_ LEAN_EXPORT lean_object* l_Lean_Elab_Term_instInhabitedTermElabM___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__11; lean_object* l_Lean_MessageData_toString(lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301____closed__1; static lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoeSort___lambda__1___closed__5; LEAN_EXPORT lean_object* l_Lean_Elab_Term_observing(lean_object*); uint8_t l_Lean_Syntax_matchesNull(lean_object*, lean_object*); @@ -566,6 +567,7 @@ static lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Term_mkTypeMismatchError___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___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambdaAux___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_logAt___at_Lean_Elab_Term_traceAtCmdPos___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301____closed__2; static lean_object* l_Lean_Elab_throwAbortTerm___at_Lean_Elab_Term_throwMVarError___spec__2___rarg___closed__2; LEAN_EXPORT lean_object* l_Lean_Elab_withMacroExpansionInfo___at_Lean_Elab_Term_withMacroExpansion___spec__1___rarg___lambda__1(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_Std_PersistentArray_mapM___at_Lean_Elab_Term_withoutModifyingElabMetaStateWithInfo___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -646,7 +648,6 @@ static lean_object* l_Lean_Elab_Term_mkTypeMismatchError___closed__6; LEAN_EXPORT lean_object* l_Lean_Elab_Term_blockImplicitLambda___boxed(lean_object*); static lean_object* l_Lean_Elab_Term_GetOpKind_noConfusion___rarg___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Term_GetOpKind_opName___boxed(lean_object*); -static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__1; static lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__7; static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits_go___spec__50___closed__1; LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitMain___at_Lean_Elab_Term_addAutoBoundImplicits_go___spec__3(lean_object*, lean_object*, lean_object*); @@ -686,7 +687,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_commitIfDidNotPostpone(lean_object*); lean_object* lean_st_mk_ref(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5983_(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5960_(lean_object*); -LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301_(lean_object*); LEAN_EXPORT lean_object* l_Lean_mkAuxName___at_Lean_Elab_Term_mkAuxName___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_setElabConfig(lean_object*); static lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__14; @@ -727,6 +728,7 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_collectUn LEAN_EXPORT lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError_appendExtra(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_isLetRecAuxMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__1; LEAN_EXPORT uint8_t l_Lean_Elab_Term_Context_errToSorry___default; LEAN_EXPORT lean_object* l_Lean_getDelayedMVarRoot___at_Lean_Elab_Term_isLetRecAuxMVar___spec__1___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_instInhabitedTermElabResult(lean_object*); @@ -755,7 +757,6 @@ static lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoeSort___la LEAN_EXPORT lean_object* l_Lean_Elab_Term_getSyntheticMVarDecl_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint64_t lean_uint64_of_nat(lean_object*); static lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isHole___closed__4; -static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270____closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Term_resolveId_x3f(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_isExprMVarAssigned___at_Lean_Elab_Term_synthesizeInstMVarCore___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_mkDeclName___at_Lean_Elab_Term_expandDeclId___spec__2___closed__1; @@ -803,6 +804,7 @@ static lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___closed__3; static lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoeSort___closed__3; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Term_0__Lean_Elab_Term_withoutModifyingStateWithInfoAndMessagesImpl___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*); uint8_t l_Lean_MessageData_hasSyntheticSorry(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Elab_Term_isMVarApp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_registerMVarErrorHoleInfo___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_Term_0__Lean_Elab_Term_tryCoeSort___lambda__1___closed__4; static lean_object* l_Lean_Elab_mkDeclName___at_Lean_Elab_Term_expandDeclId___spec__2___closed__2; @@ -822,6 +824,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabTermEnsuringType___boxed(lean_obje lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_Elab_Term_addAutoBoundImplicits_go___spec__9(lean_object*, lean_object*, size_t, size_t); LEAN_EXPORT lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___lambda__1___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_isMVarApp___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Lean_Elab_Term_Context_isNoncomputableSection___default; static lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__6; LEAN_EXPORT lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -869,7 +872,6 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_withoutModif LEAN_EXPORT lean_object* l_Lean_Elab_Term_mkConst(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_Term_0__Lean_Elab_Term_dropTermParens___closed__2; lean_object* l_Lean_LocalDecl_fvarId(lean_object*); -static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270____closed__2; lean_object* l___private_Lean_Util_Trace_0__Lean_addTraceOptions(lean_object*); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Term_resolveName___closed__4; @@ -1247,7 +1249,7 @@ static lean_object* l_Lean_Elab_Tactic_instInhabitedSnapshot___closed__17; LEAN_EXPORT lean_object* l_ReaderT_pure___at_Lean_Elab_Term_addTermInfo___spec__1___rarg___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_throwErrorIfErrors(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_getDelayedMVarAssignment_x3f___at_Lean_Elab_Term_isLetRecAuxMVar___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517_(lean_object*); LEAN_EXPORT lean_object* l_Std_PersistentArray_mapM___at_Lean_Elab_Term_withoutModifyingElabMetaStateWithInfo___spec__10___boxed(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_addAutoBoundImplicits(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Term_addAutoBoundImplicits_go___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -1291,7 +1293,6 @@ lean_object* l_Lean_MetavarContext_getDecl(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError_addArgName___closed__2; uint8_t l_Std_PersistentArray_anyM___at_Lean_MessageLog_hasErrors___spec__1(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__2___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__3; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__2___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_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits_go___spec__50(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_object* l_Lean_Core_resetMessageLog(lean_object*, lean_object*, lean_object*); @@ -1404,6 +1405,7 @@ static lean_object* l_Lean_Elab_Term_instInhabitedLetRecToLift___closed__4; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_withoutModifyingElabMetaStateWithInfo___spec__12___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_Option_set___at_Lean_Meta_withPPInaccessibleNamesImp___spec__2(lean_object*, lean_object*, uint8_t); LEAN_EXPORT lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkSyntheticSorryFor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__3; LEAN_EXPORT lean_object* l_Lean_Elab_Term_mkTermInfo(lean_object*, 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_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Term_synthesizeInstMVarCore___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___closed__8; @@ -28210,6 +28212,80 @@ lean_dec(x_2); return x_8; } } +LEAN_EXPORT lean_object* l_Lean_Elab_Term_isMVarApp(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +_start: +{ +lean_object* x_9; +x_9 = l_Lean_Meta_whnfR(x_1, x_4, x_5, x_6, x_7, x_8); +if (lean_obj_tag(x_9) == 0) +{ +uint8_t x_10; +x_10 = !lean_is_exclusive(x_9); +if (x_10 == 0) +{ +lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14; +x_11 = lean_ctor_get(x_9, 0); +x_12 = l_Lean_Expr_getAppFn(x_11); +lean_dec(x_11); +x_13 = l_Lean_Expr_isMVar(x_12); +lean_dec(x_12); +x_14 = lean_box(x_13); +lean_ctor_set(x_9, 0, x_14); +return x_9; +} +else +{ +lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19; lean_object* x_20; +x_15 = lean_ctor_get(x_9, 0); +x_16 = lean_ctor_get(x_9, 1); +lean_inc(x_16); +lean_inc(x_15); +lean_dec(x_9); +x_17 = l_Lean_Expr_getAppFn(x_15); +lean_dec(x_15); +x_18 = l_Lean_Expr_isMVar(x_17); +lean_dec(x_17); +x_19 = lean_box(x_18); +x_20 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_20, 0, x_19); +lean_ctor_set(x_20, 1, x_16); +return x_20; +} +} +else +{ +uint8_t x_21; +x_21 = !lean_is_exclusive(x_9); +if (x_21 == 0) +{ +return x_9; +} +else +{ +lean_object* x_22; lean_object* x_23; lean_object* x_24; +x_22 = lean_ctor_get(x_9, 0); +x_23 = lean_ctor_get(x_9, 1); +lean_inc(x_23); +lean_inc(x_22); +lean_dec(x_9); +x_24 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_24, 0, x_22); +lean_ctor_set(x_24, 1, x_23); +return x_24; +} +} +} +} +LEAN_EXPORT lean_object* l_Lean_Elab_Term_isMVarApp___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +_start: +{ +lean_object* x_9; +x_9 = l_Lean_Elab_Term_isMVarApp(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); +lean_dec(x_3); +lean_dec(x_2); +return x_9; +} +} LEAN_EXPORT lean_object* l_Lean_Elab_Term_tryPostponeIfMVar(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { _start: { @@ -28218,107 +28294,84 @@ lean_inc(x_7); lean_inc(x_6); lean_inc(x_5); lean_inc(x_4); -x_9 = l_Lean_Meta_whnfR(x_1, x_4, x_5, x_6, x_7, x_8); +x_9 = l_Lean_Elab_Term_isMVarApp(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); if (lean_obj_tag(x_9) == 0) { -uint8_t x_10; -x_10 = !lean_is_exclusive(x_9); -if (x_10 == 0) +lean_object* x_10; uint8_t x_11; +x_10 = lean_ctor_get(x_9, 0); +lean_inc(x_10); +x_11 = lean_unbox(x_10); +lean_dec(x_10); +if (x_11 == 0) { -lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; -x_11 = lean_ctor_get(x_9, 0); -x_12 = lean_ctor_get(x_9, 1); -x_13 = l_Lean_Expr_getAppFn(x_11); -lean_dec(x_11); -x_14 = l_Lean_Expr_isMVar(x_13); -lean_dec(x_13); -if (x_14 == 0) -{ -lean_object* x_15; +uint8_t x_12; lean_dec(x_7); lean_dec(x_6); lean_dec(x_5); lean_dec(x_4); lean_dec(x_2); -x_15 = lean_box(0); -lean_ctor_set(x_9, 0, x_15); +x_12 = !lean_is_exclusive(x_9); +if (x_12 == 0) +{ +lean_object* x_13; lean_object* x_14; +x_13 = lean_ctor_get(x_9, 0); +lean_dec(x_13); +x_14 = lean_box(0); +lean_ctor_set(x_9, 0, x_14); return x_9; } else { -lean_object* x_16; -lean_free_object(x_9); -x_16 = l_Lean_Elab_Term_tryPostpone(x_2, x_3, x_4, x_5, x_6, x_7, x_12); -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_5); -lean_dec(x_4); -return x_16; +lean_object* x_15; lean_object* x_16; lean_object* x_17; +x_15 = lean_ctor_get(x_9, 1); +lean_inc(x_15); +lean_dec(x_9); +x_16 = lean_box(0); +x_17 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_17, 0, x_16); +lean_ctor_set(x_17, 1, x_15); +return x_17; } } else { -lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; -x_17 = lean_ctor_get(x_9, 0); +lean_object* x_18; lean_object* x_19; x_18 = lean_ctor_get(x_9, 1); lean_inc(x_18); -lean_inc(x_17); lean_dec(x_9); -x_19 = l_Lean_Expr_getAppFn(x_17); -lean_dec(x_17); -x_20 = l_Lean_Expr_isMVar(x_19); -lean_dec(x_19); +x_19 = l_Lean_Elab_Term_tryPostpone(x_2, x_3, x_4, x_5, x_6, x_7, x_18); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +return x_19; +} +} +else +{ +uint8_t x_20; +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_2); +x_20 = !lean_is_exclusive(x_9); if (x_20 == 0) { -lean_object* x_21; lean_object* x_22; -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_5); -lean_dec(x_4); -lean_dec(x_2); -x_21 = lean_box(0); -x_22 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_22, 0, x_21); -lean_ctor_set(x_22, 1, x_18); -return x_22; -} -else -{ -lean_object* x_23; -x_23 = l_Lean_Elab_Term_tryPostpone(x_2, x_3, x_4, x_5, x_6, x_7, x_18); -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_5); -lean_dec(x_4); -return x_23; -} -} -} -else -{ -uint8_t x_24; -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_5); -lean_dec(x_4); -lean_dec(x_2); -x_24 = !lean_is_exclusive(x_9); -if (x_24 == 0) -{ return x_9; } else { -lean_object* x_25; lean_object* x_26; lean_object* x_27; -x_25 = lean_ctor_get(x_9, 0); -x_26 = lean_ctor_get(x_9, 1); -lean_inc(x_26); -lean_inc(x_25); +lean_object* x_21; lean_object* x_22; lean_object* x_23; +x_21 = lean_ctor_get(x_9, 0); +x_22 = lean_ctor_get(x_9, 1); +lean_inc(x_22); +lean_inc(x_21); lean_dec(x_9); -x_27 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_27, 0, x_25); -lean_ctor_set(x_27, 1, x_26); -return x_27; +x_23 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_23, 0, x_21); +lean_ctor_set(x_23, 1, x_22); +return x_23; } } } @@ -48805,7 +48858,7 @@ lean_dec(x_3); return x_10; } } -static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270____closed__1() { +static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301____closed__1() { _start: { lean_object* x_1; @@ -48813,21 +48866,21 @@ x_1 = lean_mk_string_from_bytes("letrec", 6); return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270____closed__2() { +static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Elab_Term_MVarErrorInfo_logError___closed__11; -x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270____closed__1; +x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270____closed__2; +x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301____closed__2; x_3 = l_Lean_registerTraceClass(x_2, x_1); return x_3; } @@ -49326,7 +49379,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_isLetRecAuxMVar(lean_object* x_1, lean _start: { lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_38; lean_object* x_39; lean_object* x_40; uint8_t x_41; -x_9 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270____closed__2; +x_9 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301____closed__2; x_38 = lean_st_ref_get(x_7, x_8); x_39 = lean_ctor_get(x_38, 0); lean_inc(x_39); @@ -57962,7 +58015,7 @@ x_3 = lean_alloc_closure((void*)(l_Lean_Elab_withoutModifyingStateWithInfoAndMes return x_3; } } -static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__1() { +static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -57972,7 +58025,7 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__2() { +static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__2() { _start: { lean_object* x_1; @@ -57980,17 +58033,17 @@ x_1 = lean_mk_string_from_bytes("debug", 5); return x_1; } } -static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__3() { +static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Elab_Term_MVarErrorInfo_logError___closed__11; -x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__2; +x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__2; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -58002,7 +58055,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; x_4 = lean_ctor_get(x_3, 1); lean_inc(x_4); lean_dec(x_3); -x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__1; +x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__1; x_6 = l_Lean_registerTraceClass(x_5, x_4); if (lean_obj_tag(x_6) == 0) { @@ -58010,7 +58063,7 @@ lean_object* x_7; lean_object* x_8; lean_object* x_9; x_7 = lean_ctor_get(x_6, 1); lean_inc(x_7); lean_dec(x_6); -x_8 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__3; +x_8 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__3; x_9 = l_Lean_registerTraceClass(x_8, x_7); return x_9; } @@ -58859,11 +58912,11 @@ l_Lean_Elab_Term_mkAuxName___closed__1 = _init_l_Lean_Elab_Term_mkAuxName___clos lean_mark_persistent(l_Lean_Elab_Term_mkAuxName___closed__1); l_Lean_Elab_Term_mkAuxName___closed__2 = _init_l_Lean_Elab_Term_mkAuxName___closed__2(); lean_mark_persistent(l_Lean_Elab_Term_mkAuxName___closed__2); -l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270____closed__1(); -lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270____closed__1); -l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270____closed__2(); -lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270____closed__2); -res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13270_(lean_io_mk_world()); +l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301____closed__1(); +lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301____closed__1); +l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301____closed__2(); +lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301____closed__2); +res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_13301_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l_Lean_Elab_Term_isLetRecAuxMVar___lambda__2___closed__1 = _init_l_Lean_Elab_Term_isLetRecAuxMVar___lambda__2___closed__1(); @@ -59022,13 +59075,13 @@ l_Lean_Elab_Term_exprToSyntax___closed__3 = _init_l_Lean_Elab_Term_exprToSyntax_ lean_mark_persistent(l_Lean_Elab_Term_exprToSyntax___closed__3); l_Lean_Elab_Term_exprToSyntax___closed__4 = _init_l_Lean_Elab_Term_exprToSyntax___closed__4(); lean_mark_persistent(l_Lean_Elab_Term_exprToSyntax___closed__4); -l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__1(); -lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__1); -l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__2(); -lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__2); -l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__3 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__3(); -lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486____closed__3); -res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15486_(lean_io_mk_world()); +l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__1(); +lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__1); +l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__2(); +lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__2); +l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__3 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__3(); +lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517____closed__3); +res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15517_(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));