From d0ccb73fc9987f4d28abd0a00678fa8c76eb5476 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 Apr 2022 05:11:19 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Lean/Elab/Tactic/Simp.lean | 5 +- stage0/src/Lean/Meta/Tactic/Simp/Main.lean | 33 +- stage0/stdlib/Lean/Elab/Tactic/Simp.c | 1092 +++++++------ stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c | 1674 +++++++++++++++++--- 4 files changed, 2065 insertions(+), 739 deletions(-) diff --git a/stage0/src/Lean/Elab/Tactic/Simp.lean b/stage0/src/Lean/Elab/Tactic/Simp.lean index 619ff02fb0..1de98f92b5 100644 --- a/stage0/src/Lean/Elab/Tactic/Simp.lean +++ b/stage0/src/Lean/Elab/Tactic/Simp.lean @@ -141,7 +141,10 @@ private def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) thms := thms.eraseCore arg[1].getId else let declName ← resolveGlobalConstNoOverloadWithInfo arg[1] - thms ← thms.erase declName + if ctx.config.autoUnfold then + thms := thms.eraseCore declName + else + thms ← thms.erase declName else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then let post := if arg[0].isNone then diff --git a/stage0/src/Lean/Meta/Tactic/Simp/Main.lean b/stage0/src/Lean/Meta/Tactic/Simp/Main.lean index 5c739616bd..aa26563a84 100644 --- a/stage0/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/stage0/src/Lean/Meta/Tactic/Simp/Main.lean @@ -94,6 +94,25 @@ private def reduceFVar (cfg : Config) (e : Expr) : MetaM Expr := do else return e +/-- + Return true if `declName` is the name of a definition of the form + ``` + def declName ... := + match ... with + | ... + ``` +-/ +private partial def isMatchDef (declName : Name) : CoreM Bool := do + let .defnInfo info ← getConstInfo declName | return false + return go (← getEnv) info.value +where + go (env : Environment) (e : Expr) : Bool := + if e.isLambda then + go env e.bindingBody! + else + let f := e.getAppFn + f.isConst && isMatcherCore env f.constName! + private def unfold? (e : Expr) : SimpM (Option Expr) := do let f := e.getAppFn if !f.isConst then @@ -101,7 +120,19 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do let fName := f.constName! if (← isProjectionFn fName) then return none -- should be reduced by `reduceProjFn?` - if (← read).isDeclToUnfold e.getAppFn.constName! then + let ctx ← read + if ctx.config.autoUnfold then + if ctx.simpTheorems.isErased fName then + return none + else if hasSmartUnfoldingDecl (← getEnv) fName then + withDefault <| unfoldDefinition? e + else if (← isMatchDef fName) then + let some value ← withDefault <| unfoldDefinition? e | return none + let .reduced value ← reduceMatcher? value | return none + return some value + else + return none + else if ctx.isDeclToUnfold fName then withDefault <| unfoldDefinition? e else return none diff --git a/stage0/stdlib/Lean/Elab/Tactic/Simp.c b/stage0/stdlib/Lean/Elab/Tactic/Simp.c index 830fc793ba..cb68f6f5ed 100644 --- a/stage0/stdlib/Lean/Elab/Tactic/Simp.c +++ b/stage0/stdlib/Lean/Elab/Tactic/Simp.c @@ -18,7 +18,7 @@ LEAN_EXPORT lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Tactic_ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSimp_declRange___closed__5; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalSimp___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_object* lean_array_set(lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___lambda__1(uint8_t, lean_object*, size_t, size_t, 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_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___lambda__1(lean_object*, uint8_t, lean_object*, size_t, size_t, 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_withoutModifyingState___at_Lean_Elab_Tactic_elabSimpConfigCore___spec__12___at_Lean_Elab_Tactic_elabSimpConfigCore___spec__13___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Std_PersistentHashMap_empty___at_Lean_KeyedDeclsAttribute_ExtensionState_declNames___default___spec__1; size_t lean_usize_add(size_t, size_t); @@ -101,7 +101,7 @@ static lean_object* l_Lean_Meta_SimpTheorems_erase___at___private_Lean_Elab_Tact LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_tacticToDischarge___lambda__3___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_Meta_SimpTheorems_addDeclToUnfold(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_tacticToDischarge___closed__4; -LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18(uint8_t, lean_object*, size_t, size_t, 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___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18(lean_object*, uint8_t, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSimp_declRange(lean_object*); lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -299,7 +299,7 @@ lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMe LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_erase___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__17___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*); uint8_t l_Lean_Syntax_isNone(lean_object*); lean_object* l_Lean_Elab_Term_evalExpr___rarg(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_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18___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_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18___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_object* l_Lean_Elab_Tactic_getFVarIds(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_Tactic_tacticToDischarge___closed__13; LEAN_EXPORT lean_object* l_Lean_mkConstWithLevelParams___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__12(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -6285,14 +6285,15 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18(uint8_t x_1, lean_object* x_2, size_t x_3, size_t 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, lean_object* x_14) { +LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18(lean_object* x_1, uint8_t x_2, lean_object* x_3, size_t x_4, size_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, lean_object* x_14, lean_object* x_15) { _start: { -uint8_t x_15; -x_15 = lean_usize_dec_lt(x_4, x_3); -if (x_15 == 0) +uint8_t x_16; +x_16 = lean_usize_dec_lt(x_5, x_4); +if (x_16 == 0) { -lean_object* x_16; +lean_object* x_17; +lean_dec(x_14); lean_dec(x_13); lean_dec(x_12); lean_dec(x_11); @@ -6300,64 +6301,64 @@ lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); lean_dec(x_7); -lean_dec(x_6); -x_16 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_16, 0, x_5); -lean_ctor_set(x_16, 1, x_14); -return x_16; +x_17 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_17, 0, x_6); +lean_ctor_set(x_17, 1, x_15); +return x_17; } else { -lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33; -x_17 = lean_array_uget(x_2, x_4); -x_25 = lean_ctor_get(x_5, 1); -lean_inc(x_25); -x_26 = lean_ctor_get(x_5, 0); +lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34; +x_18 = lean_array_uget(x_3, x_5); +x_26 = lean_ctor_get(x_6, 1); lean_inc(x_26); -if (lean_is_exclusive(x_5)) { - lean_ctor_release(x_5, 0); - lean_ctor_release(x_5, 1); - x_27 = x_5; +x_27 = lean_ctor_get(x_6, 0); +lean_inc(x_27); +if (lean_is_exclusive(x_6)) { + lean_ctor_release(x_6, 0); + lean_ctor_release(x_6, 1); + x_28 = x_6; } else { - lean_dec_ref(x_5); - x_27 = lean_box(0); + lean_dec_ref(x_6); + x_28 = lean_box(0); } -x_28 = lean_ctor_get(x_25, 0); -lean_inc(x_28); -x_29 = lean_ctor_get(x_25, 1); +x_29 = lean_ctor_get(x_26, 0); lean_inc(x_29); -if (lean_is_exclusive(x_25)) { - lean_ctor_release(x_25, 0); - lean_ctor_release(x_25, 1); - x_30 = x_25; +x_30 = lean_ctor_get(x_26, 1); +lean_inc(x_30); +if (lean_is_exclusive(x_26)) { + lean_ctor_release(x_26, 0); + lean_ctor_release(x_26, 1); + x_31 = x_26; } else { - lean_dec_ref(x_25); - x_30 = lean_box(0); + lean_dec_ref(x_26); + x_31 = lean_box(0); } -lean_inc(x_17); -x_31 = l_Lean_Syntax_getKind(x_17); -x_32 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18___closed__2; -x_33 = lean_name_eq(x_31, x_32); -if (x_33 == 0) +lean_inc(x_18); +x_32 = l_Lean_Syntax_getKind(x_18); +x_33 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18___closed__2; +x_34 = lean_name_eq(x_32, x_33); +if (x_34 == 0) { -lean_object* x_34; uint8_t x_35; -x_34 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18___closed__4; -x_35 = lean_name_eq(x_31, x_34); -if (x_35 == 0) +lean_object* x_35; uint8_t x_36; +x_35 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18___closed__4; +x_36 = lean_name_eq(x_32, x_35); +if (x_36 == 0) { -lean_object* x_36; uint8_t x_37; -lean_dec(x_28); -lean_dec(x_17); -x_36 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18___closed__6; -x_37 = lean_name_eq(x_31, x_36); -lean_dec(x_31); -if (x_37 == 0) -{ -lean_object* x_38; uint8_t x_39; -lean_dec(x_30); +lean_object* x_37; uint8_t x_38; lean_dec(x_29); +lean_dec(x_18); +x_37 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18___closed__6; +x_38 = lean_name_eq(x_32, x_37); +lean_dec(x_32); +if (x_38 == 0) +{ +lean_object* x_39; uint8_t x_40; +lean_dec(x_31); +lean_dec(x_30); +lean_dec(x_28); lean_dec(x_27); -lean_dec(x_26); +lean_dec(x_14); lean_dec(x_13); lean_dec(x_12); lean_dec(x_11); @@ -6365,169 +6366,169 @@ lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); lean_dec(x_7); -lean_dec(x_6); -x_38 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__1___rarg(x_14); -x_39 = !lean_is_exclusive(x_38); -if (x_39 == 0) +x_39 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__1___rarg(x_15); +x_40 = !lean_is_exclusive(x_39); +if (x_40 == 0) { -return x_38; +return x_39; } else { -lean_object* x_40; lean_object* x_41; lean_object* x_42; -x_40 = lean_ctor_get(x_38, 0); -x_41 = lean_ctor_get(x_38, 1); +lean_object* x_41; lean_object* x_42; lean_object* x_43; +x_41 = lean_ctor_get(x_39, 0); +x_42 = lean_ctor_get(x_39, 1); +lean_inc(x_42); lean_inc(x_41); -lean_inc(x_40); -lean_dec(x_38); -x_42 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_42, 0, x_40); -lean_ctor_set(x_42, 1, x_41); -return x_42; +lean_dec(x_39); +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; } } else { -uint8_t x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; -x_43 = 1; -x_44 = lean_box(x_43); -if (lean_is_scalar(x_30)) { - x_45 = lean_alloc_ctor(0, 2, 0); -} else { - x_45 = x_30; -} -lean_ctor_set(x_45, 0, x_44); -lean_ctor_set(x_45, 1, x_29); -if (lean_is_scalar(x_27)) { +uint8_t x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; +x_44 = 1; +x_45 = lean_box(x_44); +if (lean_is_scalar(x_31)) { x_46 = lean_alloc_ctor(0, 2, 0); } else { - x_46 = x_27; + x_46 = x_31; } -lean_ctor_set(x_46, 0, x_26); -lean_ctor_set(x_46, 1, x_45); -x_47 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_47, 0, x_46); -x_18 = x_47; -x_19 = x_14; -goto block_24; +lean_ctor_set(x_46, 0, x_45); +lean_ctor_set(x_46, 1, x_30); +if (lean_is_scalar(x_28)) { + x_47 = lean_alloc_ctor(0, 2, 0); +} else { + x_47 = x_28; +} +lean_ctor_set(x_47, 0, x_27); +lean_ctor_set(x_47, 1, x_46); +x_48 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_48, 0, x_47); +x_19 = x_48; +x_20 = x_15; +goto block_25; } } else { -lean_object* x_48; lean_object* x_49; uint8_t x_50; lean_object* x_51; lean_object* x_52; uint8_t x_53; lean_object* x_54; lean_object* x_55; uint8_t x_56; -lean_dec(x_31); -x_48 = lean_unsigned_to_nat(0u); -x_49 = l_Lean_Syntax_getArg(x_17, x_48); -x_50 = l_Lean_Syntax_isNone(x_49); -x_51 = lean_unsigned_to_nat(1u); -x_52 = l_Lean_Syntax_getArg(x_17, x_51); -x_53 = l_Lean_Syntax_isNone(x_52); -lean_dec(x_52); -x_54 = lean_unsigned_to_nat(2u); -x_55 = l_Lean_Syntax_getArg(x_17, x_54); -lean_dec(x_17); -if (x_50 == 0) +lean_object* x_49; lean_object* x_50; uint8_t x_51; lean_object* x_52; lean_object* x_53; uint8_t x_54; lean_object* x_55; lean_object* x_56; uint8_t x_57; +lean_dec(x_32); +x_49 = lean_unsigned_to_nat(0u); +x_50 = l_Lean_Syntax_getArg(x_18, x_49); +x_51 = l_Lean_Syntax_isNone(x_50); +x_52 = lean_unsigned_to_nat(1u); +x_53 = l_Lean_Syntax_getArg(x_18, x_52); +x_54 = l_Lean_Syntax_isNone(x_53); +lean_dec(x_53); +x_55 = lean_unsigned_to_nat(2u); +x_56 = l_Lean_Syntax_getArg(x_18, x_55); +lean_dec(x_18); +if (x_51 == 0) { -lean_object* x_100; lean_object* x_101; lean_object* x_102; uint8_t x_103; -x_100 = l_Lean_Syntax_getArg(x_49, x_48); -lean_dec(x_49); -x_101 = l_Lean_Syntax_getKind(x_100); -x_102 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18___closed__8; -x_103 = lean_name_eq(x_101, x_102); -lean_dec(x_101); -x_56 = x_103; -goto block_99; +lean_object* x_101; lean_object* x_102; lean_object* x_103; uint8_t x_104; +x_101 = l_Lean_Syntax_getArg(x_50, x_49); +lean_dec(x_50); +x_102 = l_Lean_Syntax_getKind(x_101); +x_103 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18___closed__8; +x_104 = lean_name_eq(x_102, x_103); +lean_dec(x_102); +x_57 = x_104; +goto block_100; } else { -uint8_t x_104; -lean_dec(x_49); -x_104 = 1; -x_56 = x_104; -goto block_99; +uint8_t x_105; +lean_dec(x_50); +x_105 = 1; +x_57 = x_105; +goto block_100; } -block_99: +block_100: { -uint8_t x_57; -if (x_53 == 0) -{ -uint8_t x_97; -x_97 = 1; -x_57 = x_97; -goto block_96; -} -else +uint8_t x_58; +if (x_54 == 0) { uint8_t x_98; -x_98 = 0; -x_57 = x_98; -goto block_96; -} -block_96: -{ -lean_object* x_58; -lean_inc(x_13); -lean_inc(x_12); -lean_inc(x_11); -lean_inc(x_10); -lean_inc(x_9); -lean_inc(x_8); -lean_inc(x_55); -x_58 = l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs_resolveSimpIdTheorem_x3f(x_55, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); -if (lean_obj_tag(x_58) == 0) -{ -lean_object* x_59; -x_59 = lean_ctor_get(x_58, 0); -lean_inc(x_59); -switch (lean_obj_tag(x_59)) { -case 0: -{ -lean_object* x_60; lean_object* x_61; -x_60 = lean_ctor_get(x_58, 1); -lean_inc(x_60); -lean_dec(x_58); -lean_inc(x_13); -lean_inc(x_12); -lean_inc(x_11); -lean_inc(x_10); -lean_inc(x_9); -lean_inc(x_8); -x_61 = l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_addSimpTheorem(x_29, x_55, x_56, x_57, x_8, x_9, x_10, x_11, x_12, x_13, x_60); -if (lean_obj_tag(x_61) == 0) -{ -lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; -x_62 = lean_ctor_get(x_61, 0); -lean_inc(x_62); -x_63 = lean_ctor_get(x_61, 1); -lean_inc(x_63); -lean_dec(x_61); -if (lean_is_scalar(x_30)) { - x_64 = lean_alloc_ctor(0, 2, 0); -} else { - x_64 = x_30; -} -lean_ctor_set(x_64, 0, x_28); -lean_ctor_set(x_64, 1, x_62); -if (lean_is_scalar(x_27)) { - x_65 = lean_alloc_ctor(0, 2, 0); -} else { - x_65 = x_27; -} -lean_ctor_set(x_65, 0, x_26); -lean_ctor_set(x_65, 1, x_64); -x_66 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_66, 0, x_65); -x_18 = x_66; -x_19 = x_63; -goto block_24; +x_98 = 1; +x_58 = x_98; +goto block_97; } else { -uint8_t x_67; -lean_dec(x_30); +uint8_t x_99; +x_99 = 0; +x_58 = x_99; +goto block_97; +} +block_97: +{ +lean_object* x_59; +lean_inc(x_14); +lean_inc(x_13); +lean_inc(x_12); +lean_inc(x_11); +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_56); +x_59 = l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs_resolveSimpIdTheorem_x3f(x_56, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15); +if (lean_obj_tag(x_59) == 0) +{ +lean_object* x_60; +x_60 = lean_ctor_get(x_59, 0); +lean_inc(x_60); +switch (lean_obj_tag(x_60)) { +case 0: +{ +lean_object* x_61; lean_object* x_62; +x_61 = lean_ctor_get(x_59, 1); +lean_inc(x_61); +lean_dec(x_59); +lean_inc(x_14); +lean_inc(x_13); +lean_inc(x_12); +lean_inc(x_11); +lean_inc(x_10); +lean_inc(x_9); +x_62 = l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_addSimpTheorem(x_30, x_56, x_57, x_58, x_9, x_10, x_11, x_12, x_13, x_14, x_61); +if (lean_obj_tag(x_62) == 0) +{ +lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; +x_63 = lean_ctor_get(x_62, 0); +lean_inc(x_63); +x_64 = lean_ctor_get(x_62, 1); +lean_inc(x_64); +lean_dec(x_62); +if (lean_is_scalar(x_31)) { + x_65 = lean_alloc_ctor(0, 2, 0); +} else { + x_65 = x_31; +} +lean_ctor_set(x_65, 0, x_29); +lean_ctor_set(x_65, 1, x_63); +if (lean_is_scalar(x_28)) { + x_66 = lean_alloc_ctor(0, 2, 0); +} else { + x_66 = x_28; +} +lean_ctor_set(x_66, 0, x_27); +lean_ctor_set(x_66, 1, x_65); +x_67 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_67, 0, x_66); +x_19 = x_67; +x_20 = x_64; +goto block_25; +} +else +{ +uint8_t x_68; +lean_dec(x_31); +lean_dec(x_29); lean_dec(x_28); lean_dec(x_27); -lean_dec(x_26); +lean_dec(x_14); lean_dec(x_13); lean_dec(x_12); lean_dec(x_11); @@ -6535,77 +6536,77 @@ lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); lean_dec(x_7); -lean_dec(x_6); -x_67 = !lean_is_exclusive(x_61); -if (x_67 == 0) +x_68 = !lean_is_exclusive(x_62); +if (x_68 == 0) { -return x_61; +return x_62; } else { -lean_object* x_68; lean_object* x_69; lean_object* x_70; -x_68 = lean_ctor_get(x_61, 0); -x_69 = lean_ctor_get(x_61, 1); +lean_object* x_69; lean_object* x_70; lean_object* x_71; +x_69 = lean_ctor_get(x_62, 0); +x_70 = lean_ctor_get(x_62, 1); +lean_inc(x_70); lean_inc(x_69); -lean_inc(x_68); -lean_dec(x_61); -x_70 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_70, 0, x_68); -lean_ctor_set(x_70, 1, x_69); -return x_70; +lean_dec(x_62); +x_71 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_71, 0, x_69); +lean_ctor_set(x_71, 1, x_70); +return x_71; } } } case 1: { -lean_object* x_71; lean_object* x_72; lean_object* x_73; -lean_dec(x_55); -x_71 = lean_ctor_get(x_58, 1); -lean_inc(x_71); -lean_dec(x_58); -x_72 = lean_ctor_get(x_59, 0); +lean_object* x_72; lean_object* x_73; lean_object* x_74; +lean_dec(x_56); +x_72 = lean_ctor_get(x_59, 1); lean_inc(x_72); lean_dec(x_59); +x_73 = lean_ctor_get(x_60, 0); +lean_inc(x_73); +lean_dec(x_60); +lean_inc(x_14); lean_inc(x_13); lean_inc(x_12); lean_inc(x_11); -lean_inc(x_10); -x_73 = l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_addDeclToUnfoldOrTheorem(x_29, x_72, x_56, x_57, x_10, x_11, x_12, x_13, x_71); -if (lean_obj_tag(x_73) == 0) +x_74 = l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_addDeclToUnfoldOrTheorem(x_30, x_73, x_57, x_58, x_11, x_12, x_13, x_14, x_72); +if (lean_obj_tag(x_74) == 0) { -lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; -x_74 = lean_ctor_get(x_73, 0); -lean_inc(x_74); -x_75 = lean_ctor_get(x_73, 1); +lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; +x_75 = lean_ctor_get(x_74, 0); lean_inc(x_75); -lean_dec(x_73); -if (lean_is_scalar(x_30)) { - x_76 = lean_alloc_ctor(0, 2, 0); -} else { - x_76 = x_30; -} -lean_ctor_set(x_76, 0, x_28); -lean_ctor_set(x_76, 1, x_74); -if (lean_is_scalar(x_27)) { +x_76 = lean_ctor_get(x_74, 1); +lean_inc(x_76); +lean_dec(x_74); +if (lean_is_scalar(x_31)) { x_77 = lean_alloc_ctor(0, 2, 0); } else { - x_77 = x_27; + x_77 = x_31; } -lean_ctor_set(x_77, 0, x_26); -lean_ctor_set(x_77, 1, x_76); -x_78 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_78, 0, x_77); -x_18 = x_78; -x_19 = x_75; -goto block_24; +lean_ctor_set(x_77, 0, x_29); +lean_ctor_set(x_77, 1, x_75); +if (lean_is_scalar(x_28)) { + x_78 = lean_alloc_ctor(0, 2, 0); +} else { + x_78 = x_28; +} +lean_ctor_set(x_78, 0, x_27); +lean_ctor_set(x_78, 1, x_77); +x_79 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_79, 0, x_78); +x_19 = x_79; +x_20 = x_76; +goto block_25; } else { -uint8_t x_79; -lean_dec(x_30); +uint8_t x_80; +lean_dec(x_31); +lean_dec(x_29); lean_dec(x_28); lean_dec(x_27); -lean_dec(x_26); +lean_dec(x_14); lean_dec(x_13); lean_dec(x_12); lean_dec(x_11); @@ -6613,263 +6614,76 @@ lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); lean_dec(x_7); -lean_dec(x_6); -x_79 = !lean_is_exclusive(x_73); -if (x_79 == 0) +x_80 = !lean_is_exclusive(x_74); +if (x_80 == 0) { -return x_73; +return x_74; } else { -lean_object* x_80; lean_object* x_81; lean_object* x_82; -x_80 = lean_ctor_get(x_73, 0); -x_81 = lean_ctor_get(x_73, 1); +lean_object* x_81; lean_object* x_82; lean_object* x_83; +x_81 = lean_ctor_get(x_74, 0); +x_82 = lean_ctor_get(x_74, 1); +lean_inc(x_82); lean_inc(x_81); -lean_inc(x_80); -lean_dec(x_73); -x_82 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_82, 0, x_80); -lean_ctor_set(x_82, 1, x_81); -return x_82; +lean_dec(x_74); +x_83 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_83, 0, x_81); +lean_ctor_set(x_83, 1, x_82); +return x_83; } } } default: { -lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; -lean_dec(x_55); -x_83 = lean_ctor_get(x_58, 1); -lean_inc(x_83); -lean_dec(x_58); -x_84 = lean_ctor_get(x_59, 0); +lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; +lean_dec(x_56); +x_84 = lean_ctor_get(x_59, 1); lean_inc(x_84); lean_dec(x_59); -x_85 = l_Lean_Meta_SimpExtension_getTheorems(x_84, x_12, x_13, x_83); -lean_dec(x_84); -x_86 = lean_ctor_get(x_85, 0); -lean_inc(x_86); -x_87 = lean_ctor_get(x_85, 1); -lean_inc(x_87); +x_85 = lean_ctor_get(x_60, 0); +lean_inc(x_85); +lean_dec(x_60); +x_86 = l_Lean_Meta_SimpExtension_getTheorems(x_85, x_13, x_14, x_84); lean_dec(x_85); -x_88 = lean_array_push(x_26, x_86); -if (lean_is_scalar(x_30)) { - x_89 = lean_alloc_ctor(0, 2, 0); -} else { - x_89 = x_30; -} -lean_ctor_set(x_89, 0, x_28); -lean_ctor_set(x_89, 1, x_29); -if (lean_is_scalar(x_27)) { +x_87 = lean_ctor_get(x_86, 0); +lean_inc(x_87); +x_88 = lean_ctor_get(x_86, 1); +lean_inc(x_88); +lean_dec(x_86); +x_89 = lean_array_push(x_27, x_87); +if (lean_is_scalar(x_31)) { x_90 = lean_alloc_ctor(0, 2, 0); } else { - x_90 = x_27; + x_90 = x_31; } -lean_ctor_set(x_90, 0, x_88); -lean_ctor_set(x_90, 1, x_89); -x_91 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_91, 0, x_90); -x_18 = x_91; -x_19 = x_87; -goto block_24; +lean_ctor_set(x_90, 0, x_29); +lean_ctor_set(x_90, 1, x_30); +if (lean_is_scalar(x_28)) { + x_91 = lean_alloc_ctor(0, 2, 0); +} else { + x_91 = x_28; +} +lean_ctor_set(x_91, 0, x_89); +lean_ctor_set(x_91, 1, x_90); +x_92 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_92, 0, x_91); +x_19 = x_92; +x_20 = x_88; +goto block_25; } } } else { -uint8_t x_92; -lean_dec(x_55); -lean_dec(x_30); -lean_dec(x_29); -lean_dec(x_28); -lean_dec(x_27); -lean_dec(x_26); -lean_dec(x_13); -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); -x_92 = !lean_is_exclusive(x_58); -if (x_92 == 0) -{ -return x_58; -} -else -{ -lean_object* x_93; lean_object* x_94; lean_object* x_95; -x_93 = lean_ctor_get(x_58, 0); -x_94 = lean_ctor_get(x_58, 1); -lean_inc(x_94); -lean_inc(x_93); -lean_dec(x_58); -x_95 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_95, 0, x_93); -lean_ctor_set(x_95, 1, x_94); -return x_95; -} -} -} -} -} -} -else -{ -lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; +uint8_t x_93; +lean_dec(x_56); lean_dec(x_31); -x_105 = lean_unsigned_to_nat(1u); -x_106 = l_Lean_Syntax_getArg(x_17, x_105); -lean_dec(x_17); -lean_inc(x_10); -lean_inc(x_106); -x_107 = l_Lean_Elab_Term_isLocalIdent_x3f(x_106, x_8, x_9, x_10, x_11, x_12, x_13, x_14); -x_108 = lean_ctor_get(x_107, 0); -lean_inc(x_108); -x_109 = lean_ctor_get(x_107, 1); -lean_inc(x_109); -lean_dec(x_107); -if (x_1 == 0) -{ -lean_object* x_130; -lean_dec(x_108); -x_130 = lean_box(0); -x_110 = x_130; -goto block_129; -} -else -{ -if (lean_obj_tag(x_108) == 0) -{ -lean_object* x_131; -x_131 = lean_box(0); -x_110 = x_131; -goto block_129; -} -else -{ -lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; -lean_dec(x_108); -lean_dec(x_30); -lean_dec(x_27); -x_132 = l_Lean_Syntax_getId(x_106); -lean_dec(x_106); -x_133 = l_Lean_Meta_SimpTheorems_eraseCore(x_29, x_132); -x_134 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_134, 0, x_28); -lean_ctor_set(x_134, 1, x_133); -x_135 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_135, 0, x_26); -lean_ctor_set(x_135, 1, x_134); -x_136 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_136, 0, x_135); -x_18 = x_136; -x_19 = x_109; -goto block_24; -} -} -block_129: -{ -lean_object* x_111; lean_object* x_112; -lean_dec(x_110); -x_111 = lean_box(0); -lean_inc(x_13); -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); -x_112 = l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__2(x_106, x_111, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_109); -if (lean_obj_tag(x_112) == 0) -{ -lean_object* x_113; lean_object* x_114; lean_object* x_115; -x_113 = lean_ctor_get(x_112, 0); -lean_inc(x_113); -x_114 = lean_ctor_get(x_112, 1); -lean_inc(x_114); -lean_dec(x_112); -lean_inc(x_13); -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); -x_115 = l_Lean_Meta_SimpTheorems_erase___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__17(x_29, x_113, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_114); -if (lean_obj_tag(x_115) == 0) -{ -lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; -x_116 = lean_ctor_get(x_115, 0); -lean_inc(x_116); -x_117 = lean_ctor_get(x_115, 1); -lean_inc(x_117); -lean_dec(x_115); -if (lean_is_scalar(x_30)) { - x_118 = lean_alloc_ctor(0, 2, 0); -} else { - x_118 = x_30; -} -lean_ctor_set(x_118, 0, x_28); -lean_ctor_set(x_118, 1, x_116); -if (lean_is_scalar(x_27)) { - x_119 = lean_alloc_ctor(0, 2, 0); -} else { - x_119 = x_27; -} -lean_ctor_set(x_119, 0, x_26); -lean_ctor_set(x_119, 1, x_118); -x_120 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_120, 0, x_119); -x_18 = x_120; -x_19 = x_117; -goto block_24; -} -else -{ -uint8_t x_121; -lean_dec(x_30); -lean_dec(x_28); -lean_dec(x_27); -lean_dec(x_26); -lean_dec(x_13); -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); -x_121 = !lean_is_exclusive(x_115); -if (x_121 == 0) -{ -return x_115; -} -else -{ -lean_object* x_122; lean_object* x_123; lean_object* x_124; -x_122 = lean_ctor_get(x_115, 0); -x_123 = lean_ctor_get(x_115, 1); -lean_inc(x_123); -lean_inc(x_122); -lean_dec(x_115); -x_124 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_124, 0, x_122); -lean_ctor_set(x_124, 1, x_123); -return x_124; -} -} -} -else -{ -uint8_t x_125; lean_dec(x_30); lean_dec(x_29); lean_dec(x_28); lean_dec(x_27); -lean_dec(x_26); +lean_dec(x_14); lean_dec(x_13); lean_dec(x_12); lean_dec(x_11); @@ -6877,49 +6691,270 @@ lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); lean_dec(x_7); -lean_dec(x_6); -x_125 = !lean_is_exclusive(x_112); -if (x_125 == 0) +x_93 = !lean_is_exclusive(x_59); +if (x_93 == 0) { -return x_112; +return x_59; } else { -lean_object* x_126; lean_object* x_127; lean_object* x_128; -x_126 = lean_ctor_get(x_112, 0); -x_127 = lean_ctor_get(x_112, 1); -lean_inc(x_127); -lean_inc(x_126); -lean_dec(x_112); -x_128 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_128, 0, x_126); -lean_ctor_set(x_128, 1, x_127); -return x_128; +lean_object* x_94; lean_object* x_95; lean_object* x_96; +x_94 = lean_ctor_get(x_59, 0); +x_95 = lean_ctor_get(x_59, 1); +lean_inc(x_95); +lean_inc(x_94); +lean_dec(x_59); +x_96 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_96, 0, x_94); +lean_ctor_set(x_96, 1, x_95); +return x_96; } } } } -block_24: +} +} +else { -lean_object* x_20; size_t x_21; size_t x_22; -x_20 = lean_ctor_get(x_18, 0); -lean_inc(x_20); +lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; +lean_dec(x_32); +x_106 = lean_unsigned_to_nat(1u); +x_107 = l_Lean_Syntax_getArg(x_18, x_106); lean_dec(x_18); -x_21 = 1; -x_22 = lean_usize_add(x_4, x_21); -x_4 = x_22; -x_5 = x_20; -x_14 = x_19; +lean_inc(x_11); +lean_inc(x_107); +x_108 = l_Lean_Elab_Term_isLocalIdent_x3f(x_107, x_9, x_10, x_11, x_12, x_13, x_14, x_15); +x_109 = lean_ctor_get(x_108, 0); +lean_inc(x_109); +x_110 = lean_ctor_get(x_108, 1); +lean_inc(x_110); +lean_dec(x_108); +if (x_2 == 0) +{ +lean_object* x_139; +lean_dec(x_109); +x_139 = lean_box(0); +x_111 = x_139; +goto block_138; +} +else +{ +if (lean_obj_tag(x_109) == 0) +{ +lean_object* x_140; +x_140 = lean_box(0); +x_111 = x_140; +goto block_138; +} +else +{ +lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; +lean_dec(x_109); +lean_dec(x_31); +lean_dec(x_28); +x_141 = l_Lean_Syntax_getId(x_107); +lean_dec(x_107); +x_142 = l_Lean_Meta_SimpTheorems_eraseCore(x_30, x_141); +x_143 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_143, 0, x_29); +lean_ctor_set(x_143, 1, x_142); +x_144 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_144, 0, x_27); +lean_ctor_set(x_144, 1, x_143); +x_145 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_145, 0, x_144); +x_19 = x_145; +x_20 = x_110; +goto block_25; +} +} +block_138: +{ +lean_object* x_112; lean_object* x_113; +lean_dec(x_111); +x_112 = lean_box(0); +lean_inc(x_14); +lean_inc(x_13); +lean_inc(x_12); +lean_inc(x_11); +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +x_113 = l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__2(x_107, x_112, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_110); +if (lean_obj_tag(x_113) == 0) +{ +lean_object* x_114; uint8_t x_115; +x_114 = lean_ctor_get(x_1, 0); +x_115 = lean_ctor_get_uint8(x_114, sizeof(void*)*2 + 11); +if (x_115 == 0) +{ +lean_object* x_116; lean_object* x_117; lean_object* x_118; +x_116 = lean_ctor_get(x_113, 0); +lean_inc(x_116); +x_117 = lean_ctor_get(x_113, 1); +lean_inc(x_117); +lean_dec(x_113); +lean_inc(x_14); +lean_inc(x_13); +lean_inc(x_12); +lean_inc(x_11); +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +x_118 = l_Lean_Meta_SimpTheorems_erase___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__17(x_30, x_116, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_117); +if (lean_obj_tag(x_118) == 0) +{ +lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; +x_119 = lean_ctor_get(x_118, 0); +lean_inc(x_119); +x_120 = lean_ctor_get(x_118, 1); +lean_inc(x_120); +lean_dec(x_118); +if (lean_is_scalar(x_31)) { + x_121 = lean_alloc_ctor(0, 2, 0); +} else { + x_121 = x_31; +} +lean_ctor_set(x_121, 0, x_29); +lean_ctor_set(x_121, 1, x_119); +if (lean_is_scalar(x_28)) { + x_122 = lean_alloc_ctor(0, 2, 0); +} else { + x_122 = x_28; +} +lean_ctor_set(x_122, 0, x_27); +lean_ctor_set(x_122, 1, x_121); +x_123 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_123, 0, x_122); +x_19 = x_123; +x_20 = x_120; +goto block_25; +} +else +{ +uint8_t x_124; +lean_dec(x_31); +lean_dec(x_29); +lean_dec(x_28); +lean_dec(x_27); +lean_dec(x_14); +lean_dec(x_13); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +x_124 = !lean_is_exclusive(x_118); +if (x_124 == 0) +{ +return x_118; +} +else +{ +lean_object* x_125; lean_object* x_126; lean_object* x_127; +x_125 = lean_ctor_get(x_118, 0); +x_126 = lean_ctor_get(x_118, 1); +lean_inc(x_126); +lean_inc(x_125); +lean_dec(x_118); +x_127 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_127, 0, x_125); +lean_ctor_set(x_127, 1, x_126); +return x_127; +} +} +} +else +{ +lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; +x_128 = lean_ctor_get(x_113, 0); +lean_inc(x_128); +x_129 = lean_ctor_get(x_113, 1); +lean_inc(x_129); +lean_dec(x_113); +x_130 = l_Lean_Meta_SimpTheorems_eraseCore(x_30, x_128); +if (lean_is_scalar(x_31)) { + x_131 = lean_alloc_ctor(0, 2, 0); +} else { + x_131 = x_31; +} +lean_ctor_set(x_131, 0, x_29); +lean_ctor_set(x_131, 1, x_130); +if (lean_is_scalar(x_28)) { + x_132 = lean_alloc_ctor(0, 2, 0); +} else { + x_132 = x_28; +} +lean_ctor_set(x_132, 0, x_27); +lean_ctor_set(x_132, 1, x_131); +x_133 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_133, 0, x_132); +x_19 = x_133; +x_20 = x_129; +goto block_25; +} +} +else +{ +uint8_t x_134; +lean_dec(x_31); +lean_dec(x_30); +lean_dec(x_29); +lean_dec(x_28); +lean_dec(x_27); +lean_dec(x_14); +lean_dec(x_13); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +x_134 = !lean_is_exclusive(x_113); +if (x_134 == 0) +{ +return x_113; +} +else +{ +lean_object* x_135; lean_object* x_136; lean_object* x_137; +x_135 = lean_ctor_get(x_113, 0); +x_136 = lean_ctor_get(x_113, 1); +lean_inc(x_136); +lean_inc(x_135); +lean_dec(x_113); +x_137 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_137, 0, x_135); +lean_ctor_set(x_137, 1, x_136); +return x_137; +} +} +} +} +block_25: +{ +lean_object* x_21; size_t x_22; size_t x_23; +x_21 = lean_ctor_get(x_19, 0); +lean_inc(x_21); +lean_dec(x_19); +x_22 = 1; +x_23 = lean_usize_add(x_5, x_22); +x_5 = x_23; +x_6 = x_21; +x_15 = x_20; goto _start; } } } } -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___lambda__1(uint8_t x_1, lean_object* x_2, size_t x_3, size_t 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, lean_object* x_14, lean_object* x_15) { +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___lambda__1(lean_object* x_1, uint8_t x_2, lean_object* x_3, size_t x_4, size_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, lean_object* x_14, lean_object* x_15) { _start: { lean_object* x_16; -x_16 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18(x_1, x_2, x_3, x_4, x_5, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15); +x_16 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15); if (lean_obj_tag(x_16) == 0) { lean_object* x_17; lean_object* x_18; uint8_t x_19; @@ -6941,12 +6976,12 @@ lean_inc(x_22); x_23 = lean_ctor_get(x_18, 1); lean_inc(x_23); lean_dec(x_18); -x_24 = lean_ctor_get(x_6, 0); +x_24 = lean_ctor_get(x_1, 0); x_25 = lean_unsigned_to_nat(0u); x_26 = lean_array_set(x_21, x_25, x_23); -x_27 = lean_ctor_get(x_6, 2); -x_28 = lean_ctor_get(x_6, 3); -x_29 = lean_ctor_get(x_6, 4); +x_27 = lean_ctor_get(x_1, 2); +x_28 = lean_ctor_get(x_1, 3); +x_29 = lean_ctor_get(x_1, 4); lean_inc(x_29); lean_inc(x_28); lean_inc(x_27); @@ -6979,12 +7014,12 @@ lean_inc(x_35); x_36 = lean_ctor_get(x_18, 1); lean_inc(x_36); lean_dec(x_18); -x_37 = lean_ctor_get(x_6, 0); +x_37 = lean_ctor_get(x_1, 0); x_38 = lean_unsigned_to_nat(0u); x_39 = lean_array_set(x_34, x_38, x_36); -x_40 = lean_ctor_get(x_6, 2); -x_41 = lean_ctor_get(x_6, 3); -x_42 = lean_ctor_get(x_6, 4); +x_40 = lean_ctor_get(x_1, 2); +x_41 = lean_ctor_get(x_1, 3); +x_42 = lean_ctor_get(x_1, 4); lean_inc(x_42); lean_inc(x_41); lean_inc(x_40); @@ -7071,12 +7106,12 @@ x_27 = lean_box(x_3); x_28 = lean_box_usize(x_26); x_29 = l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___boxed__const__1; x_30 = lean_alloc_closure((void*)(l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___lambda__1___boxed), 15, 6); -lean_closure_set(x_30, 0, x_27); -lean_closure_set(x_30, 1, x_20); -lean_closure_set(x_30, 2, x_28); -lean_closure_set(x_30, 3, x_29); -lean_closure_set(x_30, 4, x_24); -lean_closure_set(x_30, 5, x_2); +lean_closure_set(x_30, 0, x_2); +lean_closure_set(x_30, 1, x_27); +lean_closure_set(x_30, 2, x_20); +lean_closure_set(x_30, 3, x_28); +lean_closure_set(x_30, 4, x_29); +lean_closure_set(x_30, 5, x_24); x_31 = l_Lean_Elab_Tactic_withMainContext___rarg(x_30, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); return x_31; } @@ -7312,34 +7347,35 @@ lean_dec(x_3); return x_13; } } -LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18___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, lean_object* x_14) { +LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18___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, lean_object* x_14, lean_object* x_15) { _start: { -uint8_t x_15; size_t x_16; size_t x_17; lean_object* x_18; -x_15 = lean_unbox(x_1); -lean_dec(x_1); -x_16 = lean_unbox_usize(x_3); -lean_dec(x_3); +uint8_t x_16; size_t x_17; size_t x_18; lean_object* x_19; +x_16 = lean_unbox(x_2); +lean_dec(x_2); x_17 = lean_unbox_usize(x_4); lean_dec(x_4); -x_18 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18(x_15, x_2, x_16, x_17, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); -lean_dec(x_2); -return x_18; +x_18 = lean_unbox_usize(x_5); +lean_dec(x_5); +x_19 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___spec__18(x_1, x_16, x_3, x_17, x_18, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15); +lean_dec(x_3); +lean_dec(x_1); +return x_19; } } LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___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, lean_object* x_14, lean_object* x_15) { _start: { uint8_t x_16; size_t x_17; size_t x_18; lean_object* x_19; -x_16 = lean_unbox(x_1); -lean_dec(x_1); -x_17 = lean_unbox_usize(x_3); -lean_dec(x_3); -x_18 = lean_unbox_usize(x_4); -lean_dec(x_4); -x_19 = l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___lambda__1(x_16, x_2, x_17, x_18, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15); -lean_dec(x_6); +x_16 = lean_unbox(x_2); lean_dec(x_2); +x_17 = lean_unbox_usize(x_4); +lean_dec(x_4); +x_18 = lean_unbox_usize(x_5); +lean_dec(x_5); +x_19 = l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpArgs___lambda__1(x_1, x_16, x_3, x_17, x_18, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15); +lean_dec(x_3); +lean_dec(x_1); return x_19; } } @@ -11800,7 +11836,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimp_declRange___c _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(260u); +x_1 = lean_unsigned_to_nat(263u); x_2 = lean_unsigned_to_nat(41u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -11812,7 +11848,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimp_declRange___c _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(263u); +x_1 = lean_unsigned_to_nat(266u); x_2 = lean_unsigned_to_nat(74u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -11840,7 +11876,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimp_declRange___c _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(260u); +x_1 = lean_unsigned_to_nat(263u); x_2 = lean_unsigned_to_nat(45u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -11852,7 +11888,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimp_declRange___c _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(260u); +x_1 = lean_unsigned_to_nat(263u); x_2 = lean_unsigned_to_nat(53u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -12141,7 +12177,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimpAll_declRange_ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(265u); +x_1 = lean_unsigned_to_nat(268u); x_2 = lean_unsigned_to_nat(44u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -12153,7 +12189,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimpAll_declRange_ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(269u); +x_1 = lean_unsigned_to_nat(272u); x_2 = lean_unsigned_to_nat(43u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -12181,7 +12217,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimpAll_declRange_ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(265u); +x_1 = lean_unsigned_to_nat(268u); x_2 = lean_unsigned_to_nat(48u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -12193,7 +12229,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimpAll_declRange_ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(265u); +x_1 = lean_unsigned_to_nat(268u); x_2 = lean_unsigned_to_nat(59u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); diff --git a/stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c b/stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c index fdc24b4903..bfa267b1da 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c @@ -28,6 +28,7 @@ lean_object* lean_expr_update_forall(lean_object*, uint8_t, lean_object*, lean_o lean_object* l_Lean_Meta_replaceTargetDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkImpCongrCtx(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_array_set(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_addMessageContextPartial___at_Lean_Core_instAddMessageContextCoreM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Expr_hasAnyFVar_visit___at_Lean_Expr_containsFVar___spec__1(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_PersistentArray_findSomeRevMAux___at_Lean_Meta_Simp_dischargeUsingAssumption___spec__4___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_throwMaxRecDepthAt___at_Lean_Meta_Simp_simp___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -72,6 +73,7 @@ lean_object* l_Lean_LocalDecl_userName(lean_object*); LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduce___spec__1(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_Meta_Simp_simp_tryAutoCongrTheorem_x3f___spec__2___lambda__1___boxed(lean_object**); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_congrDefault(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___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_findSomeRevM_x3f_find___at_Lean_Meta_Simp_dischargeUsingAssumption___spec__6___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_Meta_simpGoal___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_Meta_Simp_simp_processCongrHypothesis___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -160,6 +162,8 @@ static lean_object* l_Lean_Meta_Simp_DefaultMethods_discharge_x3f___lambda__2___ LEAN_EXPORT lean_object* l_Std_AssocList_replace___at_Lean_Meta_Simp_simp_cacheResult___spec__6(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_mkCongrSimp_x3f___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Std_AssocList_contains___at_Lean_Meta_Simp_simp_mkCongrSimp_x3f___spec__4(lean_object*, lean_object*); +static lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__1; +LEAN_EXPORT lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_panic___at_Lean_Meta_Simp_simp_simpStep___spec__1___closed__4; lean_object* l_Lean_Meta_isTypeCorrect(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_SimpLetCase_noConfusion___rarg(uint8_t, uint8_t, lean_object*); @@ -264,6 +268,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Simp_main(lean_object*, lean_object*, lean_ lean_object* l_Lean_Expr_projExpr_x21(lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_simpArrow(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_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_processCongrHypothesis___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_trySimpCongrTheorem_x3f___spec__1___closed__5; LEAN_EXPORT lean_object* l_Lean_Meta_transform___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimp___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -308,6 +313,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_simpForall___lambda__3(lean_objec LEAN_EXPORT lean_object* l_Std_HashMapImp_moveEntries___at_Lean_Meta_Simp_simp_mkCongrSimp_x3f___spec__6(lean_object*, lean_object*, lean_object*); lean_object* l_instInhabited___rarg(lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_mkImpCongr___closed__3; +LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef_go___boxed(lean_object*, lean_object*); static lean_object* l_Lean_Meta_Simp_simp_simpArrow___lambda__4___closed__5; lean_object* l_panic___at_Lean_Expr_getRevArg_x21___spec__1(lean_object*); static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_tryAutoCongrTheorem_x3f___spec__3___closed__3; @@ -331,6 +337,7 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_trySi lean_object* lean_st_mk_ref(lean_object*, lean_object*); static lean_object* l_Lean_Meta_Simp_removeUnnecessaryCasts_isDummyEqRec___closed__8; LEAN_EXPORT lean_object* l_Lean_Meta_transform_visit_visitLambda___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimp___spec__4(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___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_trySimpCongrTheorem_x3f___spec__1___closed__3; static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_congrArgs___spec__1___closed__3; uint8_t lean_is_matcher(lean_object*, lean_object*); @@ -349,6 +356,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_tryAutoCongrTheorem_x3f___lambda_ LEAN_EXPORT lean_object* l_ReaderT_bind___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimp___spec__12(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_tryAutoCongrTheorem_x3f___lambda__4(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_getProjectionFnInfo_x3f___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduceProjFn_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT uint8_t l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef_go(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_tryAutoCongrTheorem_x3f___spec__3___lambda__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_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_LocalContext_findDeclRevM_x3f___at_Lean_Meta_Simp_dischargeUsingAssumption___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_simpLambda(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -375,6 +383,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_simpApp(lean_object*, lean_object static lean_object* l_Lean_Meta_Simp_Config_updateArith___closed__4; LEAN_EXPORT lean_object* l_Lean_Meta_Simp_getSimpLetCase___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_Meta_Simp_simp_congrArgs___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_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__3; static lean_object* l_Lean_Meta_Simp_simp_simpArrow___lambda__4___closed__12; LEAN_EXPORT lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimp___spec__8(lean_object*, lean_object*); lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -421,6 +430,7 @@ size_t lean_usize_of_nat(lean_object*); lean_object* l_Lean_Meta_assertHypotheses(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_applySimpResultToFVarId___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_Meta_Simp_simp_trySimpCongrTheorem_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +uint8_t l_Lean_Expr_isLambda(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_withNewLemmas___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_withMVarContext___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_expr_update_proj(lean_object*, lean_object*); @@ -463,6 +473,7 @@ uint8_t l_Lean_Exception_isMaxHeartbeat(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_congr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_addTrace___at_Lean_Meta_Simp_simp_simpForall___spec__2___closed__7; LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_visitFn___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_reduceMatcher_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_assignExprMVar(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_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimp___spec__10___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_object*); lean_object* l_Lean_Meta_mkForallCongr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -477,6 +488,7 @@ LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_Simp_simp_trySimp LEAN_EXPORT lean_object* l_Lean_Meta_applySimpResultToTarget(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_SimpTheoremsArray_eraseTheorem(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_LocalContext_findDeclRevM_x3f___at_Lean_Meta_Simp_dischargeUsingAssumption___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__4; static lean_object* l_Lean_Meta_Simp_simp_tryAutoCongrTheorem_x3f___lambda__2___closed__1; LEAN_EXPORT lean_object* l_Lean_Meta_simpTargetCore___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_transform_visit_visitLet___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimp___spec__6(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*); @@ -567,6 +579,7 @@ static lean_object* l_Lean_Meta_Simp_simp___closed__1; LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_simpForall___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_Lean_Meta_Simp_simp_tryAutoCongrTheorem_x3f___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkFalseElim(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_Simp_DefaultMethods_discharge_x3f___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimp___spec__14___boxed(lean_object*, lean_object*); lean_object* lean_panic_fn(lean_object*, lean_object*); @@ -579,6 +592,7 @@ LEAN_EXPORT lean_object* l_Std_HashMapImp_find_x3f___at_Lean_Meta_Simp_simp___sp uint8_t l_Lean_MapDeclarationExtension_contains___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_getPropHyps(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_simpArrow___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_isProjectionFn___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_unfold_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_congrArgs___spec__1(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*); @@ -635,6 +649,7 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_simpGoal___spec LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_Simp_simp_mkCongrSimp_x3f___spec__9(lean_object*, size_t, size_t); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLetDeclImp___rarg(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_Simp_simp_trySimpCongrTheorem_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +uint8_t l_Lean_Meta_SimpTheoremsArray_isErased(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimp___spec__7___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simp_simpLit___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_Simp_simp_simpArrow___closed__2; @@ -660,6 +675,7 @@ static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_trySimpCon static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_simpGoal___spec__2___lambda__2___closed__1; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_congrArgs___spec__1___lambda__2(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_Meta_Simp_simp_cacheResult___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +uint8_t l_Lean_Meta_hasSmartUnfoldingDecl(lean_object*, lean_object*); static lean_object* l_panic___at_Lean_Meta_Simp_simp_tryAutoCongrTheorem_x3f___spec__4___closed__3; lean_object* l_Lean_Meta_reduceRecMatcher_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_throwMaxRecDepthAt___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduce___spec__1___closed__1; @@ -675,6 +691,7 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_tryAu LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduce___lambda__3(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_Meta_Simp_simp_tryAutoCongrTheorem_x3f___spec__3___lambda__2(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_Meta_Simp_SimpLetCase_noConfusion___rarg___lambda__1___boxed(lean_object*); +LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__2(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimp___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkOfEqTrue(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_addTrace___at_Lean_Meta_Simp_simp_simpForall___spec__2___closed__3; @@ -3952,6 +3969,359 @@ lean_dec(x_1); return x_8; } } +LEAN_EXPORT uint8_t l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef_go(lean_object* x_1, lean_object* x_2) { +_start: +{ +uint8_t x_3; +x_3 = l_Lean_Expr_isLambda(x_2); +if (x_3 == 0) +{ +lean_object* x_4; uint8_t x_5; +x_4 = l_Lean_Expr_getAppFn(x_2); +lean_dec(x_2); +x_5 = l_Lean_Expr_isConst(x_4); +if (x_5 == 0) +{ +uint8_t x_6; +lean_dec(x_4); +lean_dec(x_1); +x_6 = 0; +return x_6; +} +else +{ +lean_object* x_7; uint8_t x_8; +x_7 = l_Lean_Expr_constName_x21(x_4); +lean_dec(x_4); +x_8 = lean_is_matcher(x_1, x_7); +return x_8; +} +} +else +{ +lean_object* x_9; +x_9 = l_Lean_Expr_bindingBody_x21(x_2); +lean_dec(x_2); +x_2 = x_9; +goto _start; +} +} +} +LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef_go___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +uint8_t x_3; lean_object* x_4; +x_3 = l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef_go(x_1, x_2); +x_4 = lean_box(x_3); +return x_4; +} +} +LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__2(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; uint8_t x_7; +x_5 = lean_ctor_get(x_2, 3); +x_6 = l_Lean_addMessageContextPartial___at_Lean_Core_instAddMessageContextCoreM___spec__1(x_1, x_2, x_3, x_4); +x_7 = !lean_is_exclusive(x_6); +if (x_7 == 0) +{ +lean_object* x_8; lean_object* x_9; +x_8 = lean_ctor_get(x_6, 0); +lean_inc(x_5); +x_9 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_9, 0, x_5); +lean_ctor_set(x_9, 1, x_8); +lean_ctor_set_tag(x_6, 1); +lean_ctor_set(x_6, 0, x_9); +return x_6; +} +else +{ +lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; +x_10 = lean_ctor_get(x_6, 0); +x_11 = lean_ctor_get(x_6, 1); +lean_inc(x_11); +lean_inc(x_10); +lean_dec(x_6); +lean_inc(x_5); +x_12 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_12, 0, x_5); +lean_ctor_set(x_12, 1, x_10); +x_13 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_13, 0, x_12); +lean_ctor_set(x_13, 1, x_11); +return x_13; +} +} +} +static lean_object* _init_l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("unknown constant '"); +return x_1; +} +} +static lean_object* _init_l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__1; +x_2 = l_Lean_stringToMessageData(x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("'"); +return x_1; +} +} +static lean_object* _init_l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__3; +x_2 = l_Lean_stringToMessageData(x_1); +return x_2; +} +} +LEAN_EXPORT lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1(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; +x_5 = lean_st_ref_get(x_3, x_4); +x_6 = !lean_is_exclusive(x_5); +if (x_6 == 0) +{ +lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; +x_7 = lean_ctor_get(x_5, 0); +x_8 = lean_ctor_get(x_5, 1); +x_9 = lean_ctor_get(x_7, 0); +lean_inc(x_9); +lean_dec(x_7); +lean_inc(x_1); +x_10 = lean_environment_find(x_9, x_1); +if (lean_obj_tag(x_10) == 0) +{ +lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; +lean_free_object(x_5); +x_11 = lean_box(0); +x_12 = l_Lean_mkConst(x_1, x_11); +x_13 = lean_alloc_ctor(2, 1, 0); +lean_ctor_set(x_13, 0, x_12); +x_14 = l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__2; +x_15 = lean_alloc_ctor(10, 2, 0); +lean_ctor_set(x_15, 0, x_14); +lean_ctor_set(x_15, 1, x_13); +x_16 = l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__4; +x_17 = lean_alloc_ctor(10, 2, 0); +lean_ctor_set(x_17, 0, x_15); +lean_ctor_set(x_17, 1, x_16); +x_18 = l_Lean_throwError___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__2(x_17, x_2, x_3, x_8); +return x_18; +} +else +{ +lean_object* x_19; +lean_dec(x_1); +x_19 = lean_ctor_get(x_10, 0); +lean_inc(x_19); +lean_dec(x_10); +lean_ctor_set(x_5, 0, x_19); +return x_5; +} +} +else +{ +lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; +x_20 = lean_ctor_get(x_5, 0); +x_21 = lean_ctor_get(x_5, 1); +lean_inc(x_21); +lean_inc(x_20); +lean_dec(x_5); +x_22 = lean_ctor_get(x_20, 0); +lean_inc(x_22); +lean_dec(x_20); +lean_inc(x_1); +x_23 = lean_environment_find(x_22, x_1); +if (lean_obj_tag(x_23) == 0) +{ +lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; +x_24 = lean_box(0); +x_25 = l_Lean_mkConst(x_1, x_24); +x_26 = lean_alloc_ctor(2, 1, 0); +lean_ctor_set(x_26, 0, x_25); +x_27 = l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__2; +x_28 = lean_alloc_ctor(10, 2, 0); +lean_ctor_set(x_28, 0, x_27); +lean_ctor_set(x_28, 1, x_26); +x_29 = l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__4; +x_30 = lean_alloc_ctor(10, 2, 0); +lean_ctor_set(x_30, 0, x_28); +lean_ctor_set(x_30, 1, x_29); +x_31 = l_Lean_throwError___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__2(x_30, x_2, x_3, x_21); +return x_31; +} +else +{ +lean_object* x_32; lean_object* x_33; +lean_dec(x_1); +x_32 = lean_ctor_get(x_23, 0); +lean_inc(x_32); +lean_dec(x_23); +x_33 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_33, 0, x_32); +lean_ctor_set(x_33, 1, x_21); +return x_33; +} +} +} +} +LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef(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_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1(x_1, x_2, x_3, x_4); +if (lean_obj_tag(x_5) == 0) +{ +lean_object* x_6; +x_6 = lean_ctor_get(x_5, 0); +lean_inc(x_6); +if (lean_obj_tag(x_6) == 1) +{ +lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; +x_7 = lean_ctor_get(x_5, 1); +lean_inc(x_7); +lean_dec(x_5); +x_8 = lean_ctor_get(x_6, 0); +lean_inc(x_8); +lean_dec(x_6); +x_9 = lean_st_ref_get(x_3, x_7); +x_10 = !lean_is_exclusive(x_9); +if (x_10 == 0) +{ +lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; lean_object* x_15; +x_11 = lean_ctor_get(x_9, 0); +x_12 = lean_ctor_get(x_11, 0); +lean_inc(x_12); +lean_dec(x_11); +x_13 = lean_ctor_get(x_8, 1); +lean_inc(x_13); +lean_dec(x_8); +x_14 = l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef_go(x_12, x_13); +x_15 = lean_box(x_14); +lean_ctor_set(x_9, 0, x_15); +return x_9; +} +else +{ +lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21; lean_object* x_22; +x_16 = lean_ctor_get(x_9, 0); +x_17 = lean_ctor_get(x_9, 1); +lean_inc(x_17); +lean_inc(x_16); +lean_dec(x_9); +x_18 = lean_ctor_get(x_16, 0); +lean_inc(x_18); +lean_dec(x_16); +x_19 = lean_ctor_get(x_8, 1); +lean_inc(x_19); +lean_dec(x_8); +x_20 = l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef_go(x_18, x_19); +x_21 = lean_box(x_20); +x_22 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_22, 0, x_21); +lean_ctor_set(x_22, 1, x_17); +return x_22; +} +} +else +{ +uint8_t x_23; +lean_dec(x_6); +x_23 = !lean_is_exclusive(x_5); +if (x_23 == 0) +{ +lean_object* x_24; uint8_t x_25; lean_object* x_26; +x_24 = lean_ctor_get(x_5, 0); +lean_dec(x_24); +x_25 = 0; +x_26 = lean_box(x_25); +lean_ctor_set(x_5, 0, x_26); +return x_5; +} +else +{ +lean_object* x_27; uint8_t x_28; lean_object* x_29; lean_object* x_30; +x_27 = lean_ctor_get(x_5, 1); +lean_inc(x_27); +lean_dec(x_5); +x_28 = 0; +x_29 = lean_box(x_28); +x_30 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_30, 0, x_29); +lean_ctor_set(x_30, 1, x_27); +return x_30; +} +} +} +else +{ +uint8_t x_31; +x_31 = !lean_is_exclusive(x_5); +if (x_31 == 0) +{ +return x_5; +} +else +{ +lean_object* x_32; lean_object* x_33; lean_object* x_34; +x_32 = lean_ctor_get(x_5, 0); +x_33 = lean_ctor_get(x_5, 1); +lean_inc(x_33); +lean_inc(x_32); +lean_dec(x_5); +x_34 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_34, 0, x_32); +lean_ctor_set(x_34, 1, x_33); +return x_34; +} +} +} +} +LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__2___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_throwError___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__2(x_1, x_2, x_3, x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_5; +} +} +LEAN_EXPORT lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___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_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1(x_1, x_2, x_3, x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___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___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef(x_1, x_2, x_3, x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_5; +} +} LEAN_EXPORT lean_object* l_Lean_isProjectionFn___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_unfold_x3f___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { _start: { @@ -3997,281 +4367,1159 @@ return x_24; LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_unfold_x3f___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_object* x_8, lean_object* x_9, lean_object* x_10) { _start: { -uint8_t x_11; -x_11 = l_Lean_Meta_Simp_Context_isDeclToUnfold(x_4, x_1); -if (x_11 == 0) +lean_object* x_11; uint8_t x_12; +x_11 = lean_ctor_get(x_4, 0); +lean_inc(x_11); +x_12 = lean_ctor_get_uint8(x_11, sizeof(void*)*2 + 11); +lean_dec(x_11); +if (x_12 == 0) { -lean_object* x_12; lean_object* x_13; +uint8_t x_13; +x_13 = l_Lean_Meta_Simp_Context_isDeclToUnfold(x_4, x_1); +if (x_13 == 0) +{ +lean_object* x_14; lean_object* x_15; lean_dec(x_9); lean_dec(x_8); lean_dec(x_7); lean_dec(x_6); lean_dec(x_2); -x_12 = lean_box(0); -x_13 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_13, 0, x_12); -lean_ctor_set(x_13, 1, x_10); -return x_13; +x_14 = lean_box(0); +x_15 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_15, 0, x_14); +lean_ctor_set(x_15, 1, x_10); +return x_15; } else { -uint8_t x_14; -x_14 = !lean_is_exclusive(x_6); -if (x_14 == 0) -{ -lean_object* x_15; uint8_t x_16; -x_15 = lean_ctor_get(x_6, 0); -x_16 = !lean_is_exclusive(x_15); +uint8_t x_16; +x_16 = !lean_is_exclusive(x_6); if (x_16 == 0) { -uint8_t x_17; lean_object* x_18; -x_17 = 1; -lean_ctor_set_uint8(x_15, 5, x_17); -x_18 = l_Lean_Meta_unfoldDefinition_x3f(x_2, x_6, x_7, x_8, x_9, x_10); -if (lean_obj_tag(x_18) == 0) +lean_object* x_17; uint8_t x_18; +x_17 = lean_ctor_get(x_6, 0); +x_18 = !lean_is_exclusive(x_17); +if (x_18 == 0) { -uint8_t x_19; -x_19 = !lean_is_exclusive(x_18); -if (x_19 == 0) +uint8_t x_19; lean_object* x_20; +x_19 = 1; +lean_ctor_set_uint8(x_17, 5, x_19); +x_20 = l_Lean_Meta_unfoldDefinition_x3f(x_2, x_6, x_7, x_8, x_9, x_10); +if (lean_obj_tag(x_20) == 0) { -return x_18; +uint8_t x_21; +x_21 = !lean_is_exclusive(x_20); +if (x_21 == 0) +{ +return x_20; } else { -lean_object* x_20; lean_object* x_21; lean_object* x_22; -x_20 = lean_ctor_get(x_18, 0); -x_21 = lean_ctor_get(x_18, 1); -lean_inc(x_21); -lean_inc(x_20); -lean_dec(x_18); -x_22 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_22, 0, x_20); -lean_ctor_set(x_22, 1, x_21); -return x_22; +lean_object* x_22; lean_object* x_23; lean_object* x_24; +x_22 = lean_ctor_get(x_20, 0); +x_23 = lean_ctor_get(x_20, 1); +lean_inc(x_23); +lean_inc(x_22); +lean_dec(x_20); +x_24 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_24, 0, x_22); +lean_ctor_set(x_24, 1, x_23); +return x_24; } } else { -uint8_t x_23; -x_23 = !lean_is_exclusive(x_18); -if (x_23 == 0) +uint8_t x_25; +x_25 = !lean_is_exclusive(x_20); +if (x_25 == 0) { -return x_18; +return x_20; } else { -lean_object* x_24; lean_object* x_25; lean_object* x_26; -x_24 = lean_ctor_get(x_18, 0); -x_25 = lean_ctor_get(x_18, 1); -lean_inc(x_25); -lean_inc(x_24); -lean_dec(x_18); -x_26 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_26, 0, x_24); -lean_ctor_set(x_26, 1, x_25); -return x_26; +lean_object* x_26; lean_object* x_27; lean_object* x_28; +x_26 = lean_ctor_get(x_20, 0); +x_27 = lean_ctor_get(x_20, 1); +lean_inc(x_27); +lean_inc(x_26); +lean_dec(x_20); +x_28 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_28, 0, x_26); +lean_ctor_set(x_28, 1, x_27); +return x_28; } } } else { -uint8_t x_27; uint8_t x_28; uint8_t x_29; uint8_t x_30; uint8_t x_31; uint8_t x_32; uint8_t x_33; uint8_t x_34; uint8_t x_35; uint8_t x_36; uint8_t x_37; uint8_t x_38; uint8_t x_39; uint8_t x_40; lean_object* x_41; lean_object* x_42; -x_27 = lean_ctor_get_uint8(x_15, 0); -x_28 = lean_ctor_get_uint8(x_15, 1); -x_29 = lean_ctor_get_uint8(x_15, 2); -x_30 = lean_ctor_get_uint8(x_15, 3); -x_31 = lean_ctor_get_uint8(x_15, 4); -x_32 = lean_ctor_get_uint8(x_15, 6); -x_33 = lean_ctor_get_uint8(x_15, 7); -x_34 = lean_ctor_get_uint8(x_15, 8); -x_35 = lean_ctor_get_uint8(x_15, 9); -x_36 = lean_ctor_get_uint8(x_15, 10); -x_37 = lean_ctor_get_uint8(x_15, 11); -x_38 = lean_ctor_get_uint8(x_15, 12); -x_39 = lean_ctor_get_uint8(x_15, 13); -lean_dec(x_15); -x_40 = 1; -x_41 = lean_alloc_ctor(0, 0, 14); -lean_ctor_set_uint8(x_41, 0, x_27); -lean_ctor_set_uint8(x_41, 1, x_28); -lean_ctor_set_uint8(x_41, 2, x_29); -lean_ctor_set_uint8(x_41, 3, x_30); -lean_ctor_set_uint8(x_41, 4, x_31); -lean_ctor_set_uint8(x_41, 5, x_40); -lean_ctor_set_uint8(x_41, 6, x_32); -lean_ctor_set_uint8(x_41, 7, x_33); -lean_ctor_set_uint8(x_41, 8, x_34); -lean_ctor_set_uint8(x_41, 9, x_35); -lean_ctor_set_uint8(x_41, 10, x_36); -lean_ctor_set_uint8(x_41, 11, x_37); -lean_ctor_set_uint8(x_41, 12, x_38); -lean_ctor_set_uint8(x_41, 13, x_39); -lean_ctor_set(x_6, 0, x_41); -x_42 = l_Lean_Meta_unfoldDefinition_x3f(x_2, x_6, x_7, x_8, x_9, x_10); -if (lean_obj_tag(x_42) == 0) +uint8_t x_29; uint8_t x_30; uint8_t x_31; uint8_t x_32; uint8_t x_33; uint8_t x_34; uint8_t x_35; uint8_t x_36; uint8_t x_37; uint8_t x_38; uint8_t x_39; uint8_t x_40; uint8_t x_41; uint8_t x_42; lean_object* x_43; lean_object* x_44; +x_29 = lean_ctor_get_uint8(x_17, 0); +x_30 = lean_ctor_get_uint8(x_17, 1); +x_31 = lean_ctor_get_uint8(x_17, 2); +x_32 = lean_ctor_get_uint8(x_17, 3); +x_33 = lean_ctor_get_uint8(x_17, 4); +x_34 = lean_ctor_get_uint8(x_17, 6); +x_35 = lean_ctor_get_uint8(x_17, 7); +x_36 = lean_ctor_get_uint8(x_17, 8); +x_37 = lean_ctor_get_uint8(x_17, 9); +x_38 = lean_ctor_get_uint8(x_17, 10); +x_39 = lean_ctor_get_uint8(x_17, 11); +x_40 = lean_ctor_get_uint8(x_17, 12); +x_41 = lean_ctor_get_uint8(x_17, 13); +lean_dec(x_17); +x_42 = 1; +x_43 = lean_alloc_ctor(0, 0, 14); +lean_ctor_set_uint8(x_43, 0, x_29); +lean_ctor_set_uint8(x_43, 1, x_30); +lean_ctor_set_uint8(x_43, 2, x_31); +lean_ctor_set_uint8(x_43, 3, x_32); +lean_ctor_set_uint8(x_43, 4, x_33); +lean_ctor_set_uint8(x_43, 5, x_42); +lean_ctor_set_uint8(x_43, 6, x_34); +lean_ctor_set_uint8(x_43, 7, x_35); +lean_ctor_set_uint8(x_43, 8, x_36); +lean_ctor_set_uint8(x_43, 9, x_37); +lean_ctor_set_uint8(x_43, 10, x_38); +lean_ctor_set_uint8(x_43, 11, x_39); +lean_ctor_set_uint8(x_43, 12, x_40); +lean_ctor_set_uint8(x_43, 13, x_41); +lean_ctor_set(x_6, 0, x_43); +x_44 = l_Lean_Meta_unfoldDefinition_x3f(x_2, x_6, x_7, x_8, x_9, x_10); +if (lean_obj_tag(x_44) == 0) { -lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; -x_43 = lean_ctor_get(x_42, 0); -lean_inc(x_43); -x_44 = lean_ctor_get(x_42, 1); -lean_inc(x_44); -if (lean_is_exclusive(x_42)) { - lean_ctor_release(x_42, 0); - lean_ctor_release(x_42, 1); - x_45 = x_42; +lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; +x_45 = lean_ctor_get(x_44, 0); +lean_inc(x_45); +x_46 = lean_ctor_get(x_44, 1); +lean_inc(x_46); +if (lean_is_exclusive(x_44)) { + lean_ctor_release(x_44, 0); + lean_ctor_release(x_44, 1); + x_47 = x_44; } else { - lean_dec_ref(x_42); - x_45 = lean_box(0); + lean_dec_ref(x_44); + x_47 = lean_box(0); } -if (lean_is_scalar(x_45)) { - x_46 = lean_alloc_ctor(0, 2, 0); +if (lean_is_scalar(x_47)) { + x_48 = lean_alloc_ctor(0, 2, 0); } else { - x_46 = x_45; + x_48 = x_47; } -lean_ctor_set(x_46, 0, x_43); -lean_ctor_set(x_46, 1, x_44); -return x_46; +lean_ctor_set(x_48, 0, x_45); +lean_ctor_set(x_48, 1, x_46); +return x_48; } else { -lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; -x_47 = lean_ctor_get(x_42, 0); -lean_inc(x_47); -x_48 = lean_ctor_get(x_42, 1); -lean_inc(x_48); -if (lean_is_exclusive(x_42)) { - lean_ctor_release(x_42, 0); - lean_ctor_release(x_42, 1); - x_49 = x_42; +lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; +x_49 = lean_ctor_get(x_44, 0); +lean_inc(x_49); +x_50 = lean_ctor_get(x_44, 1); +lean_inc(x_50); +if (lean_is_exclusive(x_44)) { + lean_ctor_release(x_44, 0); + lean_ctor_release(x_44, 1); + x_51 = x_44; } else { - lean_dec_ref(x_42); - x_49 = lean_box(0); + lean_dec_ref(x_44); + x_51 = lean_box(0); } -if (lean_is_scalar(x_49)) { - x_50 = lean_alloc_ctor(1, 2, 0); +if (lean_is_scalar(x_51)) { + x_52 = lean_alloc_ctor(1, 2, 0); } else { - x_50 = x_49; + x_52 = x_51; } -lean_ctor_set(x_50, 0, x_47); -lean_ctor_set(x_50, 1, x_48); -return x_50; +lean_ctor_set(x_52, 0, x_49); +lean_ctor_set(x_52, 1, x_50); +return x_52; } } } else { -lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; uint8_t x_57; uint8_t x_58; uint8_t x_59; uint8_t x_60; uint8_t x_61; uint8_t x_62; uint8_t x_63; uint8_t x_64; uint8_t x_65; uint8_t x_66; uint8_t x_67; uint8_t x_68; uint8_t x_69; lean_object* x_70; uint8_t x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; -x_51 = lean_ctor_get(x_6, 0); -x_52 = lean_ctor_get(x_6, 1); -x_53 = lean_ctor_get(x_6, 2); -x_54 = lean_ctor_get(x_6, 3); -x_55 = lean_ctor_get(x_6, 4); -x_56 = lean_ctor_get(x_6, 5); +lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; uint8_t x_59; uint8_t x_60; uint8_t x_61; uint8_t x_62; uint8_t x_63; uint8_t x_64; uint8_t x_65; uint8_t x_66; uint8_t x_67; uint8_t x_68; uint8_t x_69; uint8_t x_70; uint8_t x_71; lean_object* x_72; uint8_t x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; +x_53 = lean_ctor_get(x_6, 0); +x_54 = lean_ctor_get(x_6, 1); +x_55 = lean_ctor_get(x_6, 2); +x_56 = lean_ctor_get(x_6, 3); +x_57 = lean_ctor_get(x_6, 4); +x_58 = lean_ctor_get(x_6, 5); +lean_inc(x_58); +lean_inc(x_57); lean_inc(x_56); lean_inc(x_55); lean_inc(x_54); lean_inc(x_53); -lean_inc(x_52); -lean_inc(x_51); lean_dec(x_6); -x_57 = lean_ctor_get_uint8(x_51, 0); -x_58 = lean_ctor_get_uint8(x_51, 1); -x_59 = lean_ctor_get_uint8(x_51, 2); -x_60 = lean_ctor_get_uint8(x_51, 3); -x_61 = lean_ctor_get_uint8(x_51, 4); -x_62 = lean_ctor_get_uint8(x_51, 6); -x_63 = lean_ctor_get_uint8(x_51, 7); -x_64 = lean_ctor_get_uint8(x_51, 8); -x_65 = lean_ctor_get_uint8(x_51, 9); -x_66 = lean_ctor_get_uint8(x_51, 10); -x_67 = lean_ctor_get_uint8(x_51, 11); -x_68 = lean_ctor_get_uint8(x_51, 12); -x_69 = lean_ctor_get_uint8(x_51, 13); -if (lean_is_exclusive(x_51)) { - x_70 = x_51; +x_59 = lean_ctor_get_uint8(x_53, 0); +x_60 = lean_ctor_get_uint8(x_53, 1); +x_61 = lean_ctor_get_uint8(x_53, 2); +x_62 = lean_ctor_get_uint8(x_53, 3); +x_63 = lean_ctor_get_uint8(x_53, 4); +x_64 = lean_ctor_get_uint8(x_53, 6); +x_65 = lean_ctor_get_uint8(x_53, 7); +x_66 = lean_ctor_get_uint8(x_53, 8); +x_67 = lean_ctor_get_uint8(x_53, 9); +x_68 = lean_ctor_get_uint8(x_53, 10); +x_69 = lean_ctor_get_uint8(x_53, 11); +x_70 = lean_ctor_get_uint8(x_53, 12); +x_71 = lean_ctor_get_uint8(x_53, 13); +if (lean_is_exclusive(x_53)) { + x_72 = x_53; } else { - lean_dec_ref(x_51); - x_70 = lean_box(0); + lean_dec_ref(x_53); + x_72 = lean_box(0); } -x_71 = 1; -if (lean_is_scalar(x_70)) { - x_72 = lean_alloc_ctor(0, 0, 14); +x_73 = 1; +if (lean_is_scalar(x_72)) { + x_74 = lean_alloc_ctor(0, 0, 14); } else { - x_72 = x_70; + x_74 = x_72; } -lean_ctor_set_uint8(x_72, 0, x_57); -lean_ctor_set_uint8(x_72, 1, x_58); -lean_ctor_set_uint8(x_72, 2, x_59); -lean_ctor_set_uint8(x_72, 3, x_60); -lean_ctor_set_uint8(x_72, 4, x_61); -lean_ctor_set_uint8(x_72, 5, x_71); -lean_ctor_set_uint8(x_72, 6, x_62); -lean_ctor_set_uint8(x_72, 7, x_63); -lean_ctor_set_uint8(x_72, 8, x_64); -lean_ctor_set_uint8(x_72, 9, x_65); -lean_ctor_set_uint8(x_72, 10, x_66); -lean_ctor_set_uint8(x_72, 11, x_67); -lean_ctor_set_uint8(x_72, 12, x_68); -lean_ctor_set_uint8(x_72, 13, x_69); -x_73 = lean_alloc_ctor(0, 6, 0); -lean_ctor_set(x_73, 0, x_72); -lean_ctor_set(x_73, 1, x_52); -lean_ctor_set(x_73, 2, x_53); -lean_ctor_set(x_73, 3, x_54); -lean_ctor_set(x_73, 4, x_55); -lean_ctor_set(x_73, 5, x_56); -x_74 = l_Lean_Meta_unfoldDefinition_x3f(x_2, x_73, x_7, x_8, x_9, x_10); -if (lean_obj_tag(x_74) == 0) +lean_ctor_set_uint8(x_74, 0, x_59); +lean_ctor_set_uint8(x_74, 1, x_60); +lean_ctor_set_uint8(x_74, 2, x_61); +lean_ctor_set_uint8(x_74, 3, x_62); +lean_ctor_set_uint8(x_74, 4, x_63); +lean_ctor_set_uint8(x_74, 5, x_73); +lean_ctor_set_uint8(x_74, 6, x_64); +lean_ctor_set_uint8(x_74, 7, x_65); +lean_ctor_set_uint8(x_74, 8, x_66); +lean_ctor_set_uint8(x_74, 9, x_67); +lean_ctor_set_uint8(x_74, 10, x_68); +lean_ctor_set_uint8(x_74, 11, x_69); +lean_ctor_set_uint8(x_74, 12, x_70); +lean_ctor_set_uint8(x_74, 13, x_71); +x_75 = lean_alloc_ctor(0, 6, 0); +lean_ctor_set(x_75, 0, x_74); +lean_ctor_set(x_75, 1, x_54); +lean_ctor_set(x_75, 2, x_55); +lean_ctor_set(x_75, 3, x_56); +lean_ctor_set(x_75, 4, x_57); +lean_ctor_set(x_75, 5, x_58); +x_76 = l_Lean_Meta_unfoldDefinition_x3f(x_2, x_75, x_7, x_8, x_9, x_10); +if (lean_obj_tag(x_76) == 0) { -lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; -x_75 = lean_ctor_get(x_74, 0); -lean_inc(x_75); -x_76 = lean_ctor_get(x_74, 1); -lean_inc(x_76); -if (lean_is_exclusive(x_74)) { - lean_ctor_release(x_74, 0); - lean_ctor_release(x_74, 1); - x_77 = x_74; +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); +lean_inc(x_78); +if (lean_is_exclusive(x_76)) { + lean_ctor_release(x_76, 0); + lean_ctor_release(x_76, 1); + x_79 = x_76; } else { - lean_dec_ref(x_74); - x_77 = lean_box(0); + lean_dec_ref(x_76); + x_79 = lean_box(0); } -if (lean_is_scalar(x_77)) { - x_78 = lean_alloc_ctor(0, 2, 0); +if (lean_is_scalar(x_79)) { + x_80 = lean_alloc_ctor(0, 2, 0); } else { - x_78 = x_77; + x_80 = x_79; } -lean_ctor_set(x_78, 0, x_75); -lean_ctor_set(x_78, 1, x_76); -return x_78; +lean_ctor_set(x_80, 0, x_77); +lean_ctor_set(x_80, 1, x_78); +return x_80; } else { -lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; -x_79 = lean_ctor_get(x_74, 0); -lean_inc(x_79); -x_80 = lean_ctor_get(x_74, 1); -lean_inc(x_80); -if (lean_is_exclusive(x_74)) { - lean_ctor_release(x_74, 0); - lean_ctor_release(x_74, 1); - x_81 = x_74; +lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; +x_81 = lean_ctor_get(x_76, 0); +lean_inc(x_81); +x_82 = lean_ctor_get(x_76, 1); +lean_inc(x_82); +if (lean_is_exclusive(x_76)) { + lean_ctor_release(x_76, 0); + lean_ctor_release(x_76, 1); + x_83 = x_76; } else { - lean_dec_ref(x_74); - x_81 = lean_box(0); + lean_dec_ref(x_76); + x_83 = lean_box(0); } -if (lean_is_scalar(x_81)) { - x_82 = lean_alloc_ctor(1, 2, 0); +if (lean_is_scalar(x_83)) { + x_84 = lean_alloc_ctor(1, 2, 0); } else { - x_82 = x_81; + x_84 = x_83; } -lean_ctor_set(x_82, 0, x_79); -lean_ctor_set(x_82, 1, x_80); -return x_82; +lean_ctor_set(x_84, 0, x_81); +lean_ctor_set(x_84, 1, x_82); +return x_84; } } } } +else +{ +lean_object* x_85; uint8_t x_86; +x_85 = lean_ctor_get(x_4, 1); +lean_inc(x_85); +lean_dec(x_4); +lean_inc(x_1); +x_86 = l_Lean_Meta_SimpTheoremsArray_isErased(x_85, x_1); +if (x_86 == 0) +{ +lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; uint8_t x_91; +x_87 = lean_st_ref_get(x_9, x_10); +x_88 = lean_ctor_get(x_87, 0); +lean_inc(x_88); +x_89 = lean_ctor_get(x_87, 1); +lean_inc(x_89); +lean_dec(x_87); +x_90 = lean_ctor_get(x_88, 0); +lean_inc(x_90); +lean_dec(x_88); +lean_inc(x_1); +x_91 = l_Lean_Meta_hasSmartUnfoldingDecl(x_90, x_1); +if (x_91 == 0) +{ +lean_object* x_92; +x_92 = l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef(x_1, x_8, x_9, x_89); +if (lean_obj_tag(x_92) == 0) +{ +lean_object* x_93; uint8_t x_94; +x_93 = lean_ctor_get(x_92, 0); +lean_inc(x_93); +x_94 = lean_unbox(x_93); +lean_dec(x_93); +if (x_94 == 0) +{ +uint8_t x_95; +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_2); +x_95 = !lean_is_exclusive(x_92); +if (x_95 == 0) +{ +lean_object* x_96; lean_object* x_97; +x_96 = lean_ctor_get(x_92, 0); +lean_dec(x_96); +x_97 = lean_box(0); +lean_ctor_set(x_92, 0, x_97); +return x_92; +} +else +{ +lean_object* x_98; lean_object* x_99; lean_object* x_100; +x_98 = lean_ctor_get(x_92, 1); +lean_inc(x_98); +lean_dec(x_92); +x_99 = lean_box(0); +x_100 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_100, 0, x_99); +lean_ctor_set(x_100, 1, x_98); +return x_100; +} +} +else +{ +lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; uint8_t x_108; +x_101 = lean_ctor_get(x_6, 0); +lean_inc(x_101); +x_102 = lean_ctor_get(x_92, 1); +lean_inc(x_102); +lean_dec(x_92); +x_103 = lean_ctor_get(x_6, 1); +lean_inc(x_103); +x_104 = lean_ctor_get(x_6, 2); +lean_inc(x_104); +x_105 = lean_ctor_get(x_6, 3); +lean_inc(x_105); +x_106 = lean_ctor_get(x_6, 4); +lean_inc(x_106); +x_107 = lean_ctor_get(x_6, 5); +lean_inc(x_107); +x_108 = !lean_is_exclusive(x_101); +if (x_108 == 0) +{ +uint8_t x_109; lean_object* x_110; lean_object* x_111; +x_109 = 1; +lean_ctor_set_uint8(x_101, 5, x_109); +x_110 = lean_alloc_ctor(0, 6, 0); +lean_ctor_set(x_110, 0, x_101); +lean_ctor_set(x_110, 1, x_103); +lean_ctor_set(x_110, 2, x_104); +lean_ctor_set(x_110, 3, x_105); +lean_ctor_set(x_110, 4, x_106); +lean_ctor_set(x_110, 5, x_107); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +x_111 = l_Lean_Meta_unfoldDefinition_x3f(x_2, x_110, x_7, x_8, x_9, x_102); +if (lean_obj_tag(x_111) == 0) +{ +lean_object* x_112; +x_112 = lean_ctor_get(x_111, 0); +lean_inc(x_112); +if (lean_obj_tag(x_112) == 0) +{ +uint8_t x_113; +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +x_113 = !lean_is_exclusive(x_111); +if (x_113 == 0) +{ +lean_object* x_114; lean_object* x_115; +x_114 = lean_ctor_get(x_111, 0); +lean_dec(x_114); +x_115 = lean_box(0); +lean_ctor_set(x_111, 0, x_115); +return x_111; +} +else +{ +lean_object* x_116; lean_object* x_117; lean_object* x_118; +x_116 = lean_ctor_get(x_111, 1); +lean_inc(x_116); +lean_dec(x_111); +x_117 = lean_box(0); +x_118 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_118, 0, x_117); +lean_ctor_set(x_118, 1, x_116); +return x_118; +} +} +else +{ +lean_object* x_119; uint8_t x_120; +x_119 = lean_ctor_get(x_111, 1); +lean_inc(x_119); +lean_dec(x_111); +x_120 = !lean_is_exclusive(x_112); +if (x_120 == 0) +{ +lean_object* x_121; lean_object* x_122; +x_121 = lean_ctor_get(x_112, 0); +x_122 = l_Lean_Meta_reduceMatcher_x3f(x_121, x_6, x_7, x_8, x_9, x_119); +if (lean_obj_tag(x_122) == 0) +{ +lean_object* x_123; +x_123 = lean_ctor_get(x_122, 0); +lean_inc(x_123); +if (lean_obj_tag(x_123) == 0) +{ +uint8_t x_124; +x_124 = !lean_is_exclusive(x_122); +if (x_124 == 0) +{ +lean_object* x_125; lean_object* x_126; +x_125 = lean_ctor_get(x_122, 0); +lean_dec(x_125); +x_126 = lean_ctor_get(x_123, 0); +lean_inc(x_126); +lean_dec(x_123); +lean_ctor_set(x_112, 0, x_126); +lean_ctor_set(x_122, 0, x_112); +return x_122; +} +else +{ +lean_object* x_127; lean_object* x_128; lean_object* x_129; +x_127 = lean_ctor_get(x_122, 1); +lean_inc(x_127); +lean_dec(x_122); +x_128 = lean_ctor_get(x_123, 0); +lean_inc(x_128); +lean_dec(x_123); +lean_ctor_set(x_112, 0, x_128); +x_129 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_129, 0, x_112); +lean_ctor_set(x_129, 1, x_127); +return x_129; +} +} +else +{ +uint8_t x_130; +lean_dec(x_123); +lean_free_object(x_112); +x_130 = !lean_is_exclusive(x_122); +if (x_130 == 0) +{ +lean_object* x_131; lean_object* x_132; +x_131 = lean_ctor_get(x_122, 0); +lean_dec(x_131); +x_132 = lean_box(0); +lean_ctor_set(x_122, 0, x_132); +return x_122; +} +else +{ +lean_object* x_133; lean_object* x_134; lean_object* x_135; +x_133 = lean_ctor_get(x_122, 1); +lean_inc(x_133); +lean_dec(x_122); +x_134 = lean_box(0); +x_135 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_135, 0, x_134); +lean_ctor_set(x_135, 1, x_133); +return x_135; +} +} +} +else +{ +uint8_t x_136; +lean_free_object(x_112); +x_136 = !lean_is_exclusive(x_122); +if (x_136 == 0) +{ +return x_122; +} +else +{ +lean_object* x_137; lean_object* x_138; lean_object* x_139; +x_137 = lean_ctor_get(x_122, 0); +x_138 = lean_ctor_get(x_122, 1); +lean_inc(x_138); +lean_inc(x_137); +lean_dec(x_122); +x_139 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_139, 0, x_137); +lean_ctor_set(x_139, 1, x_138); +return x_139; +} +} +} +else +{ +lean_object* x_140; lean_object* x_141; +x_140 = lean_ctor_get(x_112, 0); +lean_inc(x_140); +lean_dec(x_112); +x_141 = l_Lean_Meta_reduceMatcher_x3f(x_140, x_6, x_7, x_8, x_9, x_119); +if (lean_obj_tag(x_141) == 0) +{ +lean_object* x_142; +x_142 = lean_ctor_get(x_141, 0); +lean_inc(x_142); +if (lean_obj_tag(x_142) == 0) +{ +lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; +x_143 = lean_ctor_get(x_141, 1); +lean_inc(x_143); +if (lean_is_exclusive(x_141)) { + lean_ctor_release(x_141, 0); + lean_ctor_release(x_141, 1); + x_144 = x_141; +} else { + lean_dec_ref(x_141); + x_144 = lean_box(0); +} +x_145 = lean_ctor_get(x_142, 0); +lean_inc(x_145); +lean_dec(x_142); +x_146 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_146, 0, x_145); +if (lean_is_scalar(x_144)) { + x_147 = lean_alloc_ctor(0, 2, 0); +} else { + x_147 = x_144; +} +lean_ctor_set(x_147, 0, x_146); +lean_ctor_set(x_147, 1, x_143); +return x_147; +} +else +{ +lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; +lean_dec(x_142); +x_148 = lean_ctor_get(x_141, 1); +lean_inc(x_148); +if (lean_is_exclusive(x_141)) { + lean_ctor_release(x_141, 0); + lean_ctor_release(x_141, 1); + x_149 = x_141; +} else { + lean_dec_ref(x_141); + x_149 = lean_box(0); +} +x_150 = lean_box(0); +if (lean_is_scalar(x_149)) { + x_151 = lean_alloc_ctor(0, 2, 0); +} else { + x_151 = x_149; +} +lean_ctor_set(x_151, 0, x_150); +lean_ctor_set(x_151, 1, x_148); +return x_151; +} +} +else +{ +lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_155; +x_152 = lean_ctor_get(x_141, 0); +lean_inc(x_152); +x_153 = lean_ctor_get(x_141, 1); +lean_inc(x_153); +if (lean_is_exclusive(x_141)) { + lean_ctor_release(x_141, 0); + lean_ctor_release(x_141, 1); + x_154 = x_141; +} else { + lean_dec_ref(x_141); + x_154 = lean_box(0); +} +if (lean_is_scalar(x_154)) { + x_155 = lean_alloc_ctor(1, 2, 0); +} else { + x_155 = x_154; +} +lean_ctor_set(x_155, 0, x_152); +lean_ctor_set(x_155, 1, x_153); +return x_155; +} +} +} +} +else +{ +uint8_t x_156; +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +x_156 = !lean_is_exclusive(x_111); +if (x_156 == 0) +{ +return x_111; +} +else +{ +lean_object* x_157; lean_object* x_158; lean_object* x_159; +x_157 = lean_ctor_get(x_111, 0); +x_158 = lean_ctor_get(x_111, 1); +lean_inc(x_158); +lean_inc(x_157); +lean_dec(x_111); +x_159 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_159, 0, x_157); +lean_ctor_set(x_159, 1, x_158); +return x_159; +} +} +} +else +{ +uint8_t x_160; uint8_t x_161; uint8_t x_162; uint8_t x_163; uint8_t x_164; uint8_t x_165; uint8_t x_166; uint8_t x_167; uint8_t x_168; uint8_t x_169; uint8_t x_170; uint8_t x_171; uint8_t x_172; uint8_t x_173; lean_object* x_174; lean_object* x_175; lean_object* x_176; +x_160 = lean_ctor_get_uint8(x_101, 0); +x_161 = lean_ctor_get_uint8(x_101, 1); +x_162 = lean_ctor_get_uint8(x_101, 2); +x_163 = lean_ctor_get_uint8(x_101, 3); +x_164 = lean_ctor_get_uint8(x_101, 4); +x_165 = lean_ctor_get_uint8(x_101, 6); +x_166 = lean_ctor_get_uint8(x_101, 7); +x_167 = lean_ctor_get_uint8(x_101, 8); +x_168 = lean_ctor_get_uint8(x_101, 9); +x_169 = lean_ctor_get_uint8(x_101, 10); +x_170 = lean_ctor_get_uint8(x_101, 11); +x_171 = lean_ctor_get_uint8(x_101, 12); +x_172 = lean_ctor_get_uint8(x_101, 13); +lean_dec(x_101); +x_173 = 1; +x_174 = lean_alloc_ctor(0, 0, 14); +lean_ctor_set_uint8(x_174, 0, x_160); +lean_ctor_set_uint8(x_174, 1, x_161); +lean_ctor_set_uint8(x_174, 2, x_162); +lean_ctor_set_uint8(x_174, 3, x_163); +lean_ctor_set_uint8(x_174, 4, x_164); +lean_ctor_set_uint8(x_174, 5, x_173); +lean_ctor_set_uint8(x_174, 6, x_165); +lean_ctor_set_uint8(x_174, 7, x_166); +lean_ctor_set_uint8(x_174, 8, x_167); +lean_ctor_set_uint8(x_174, 9, x_168); +lean_ctor_set_uint8(x_174, 10, x_169); +lean_ctor_set_uint8(x_174, 11, x_170); +lean_ctor_set_uint8(x_174, 12, x_171); +lean_ctor_set_uint8(x_174, 13, x_172); +x_175 = lean_alloc_ctor(0, 6, 0); +lean_ctor_set(x_175, 0, x_174); +lean_ctor_set(x_175, 1, x_103); +lean_ctor_set(x_175, 2, x_104); +lean_ctor_set(x_175, 3, x_105); +lean_ctor_set(x_175, 4, x_106); +lean_ctor_set(x_175, 5, x_107); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +x_176 = l_Lean_Meta_unfoldDefinition_x3f(x_2, x_175, x_7, x_8, x_9, x_102); +if (lean_obj_tag(x_176) == 0) +{ +lean_object* x_177; +x_177 = lean_ctor_get(x_176, 0); +lean_inc(x_177); +if (lean_obj_tag(x_177) == 0) +{ +lean_object* x_178; lean_object* x_179; lean_object* x_180; lean_object* x_181; +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +x_178 = lean_ctor_get(x_176, 1); +lean_inc(x_178); +if (lean_is_exclusive(x_176)) { + lean_ctor_release(x_176, 0); + lean_ctor_release(x_176, 1); + x_179 = x_176; +} else { + lean_dec_ref(x_176); + x_179 = lean_box(0); +} +x_180 = lean_box(0); +if (lean_is_scalar(x_179)) { + x_181 = lean_alloc_ctor(0, 2, 0); +} else { + x_181 = x_179; +} +lean_ctor_set(x_181, 0, x_180); +lean_ctor_set(x_181, 1, x_178); +return x_181; +} +else +{ +lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; +x_182 = lean_ctor_get(x_176, 1); +lean_inc(x_182); +lean_dec(x_176); +x_183 = lean_ctor_get(x_177, 0); +lean_inc(x_183); +if (lean_is_exclusive(x_177)) { + lean_ctor_release(x_177, 0); + x_184 = x_177; +} else { + lean_dec_ref(x_177); + x_184 = lean_box(0); +} +x_185 = l_Lean_Meta_reduceMatcher_x3f(x_183, x_6, x_7, x_8, x_9, x_182); +if (lean_obj_tag(x_185) == 0) +{ +lean_object* x_186; +x_186 = lean_ctor_get(x_185, 0); +lean_inc(x_186); +if (lean_obj_tag(x_186) == 0) +{ +lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; lean_object* x_191; +x_187 = lean_ctor_get(x_185, 1); +lean_inc(x_187); +if (lean_is_exclusive(x_185)) { + lean_ctor_release(x_185, 0); + lean_ctor_release(x_185, 1); + x_188 = x_185; +} else { + lean_dec_ref(x_185); + x_188 = lean_box(0); +} +x_189 = lean_ctor_get(x_186, 0); +lean_inc(x_189); +lean_dec(x_186); +if (lean_is_scalar(x_184)) { + x_190 = lean_alloc_ctor(1, 1, 0); +} else { + x_190 = x_184; +} +lean_ctor_set(x_190, 0, x_189); +if (lean_is_scalar(x_188)) { + x_191 = lean_alloc_ctor(0, 2, 0); +} else { + x_191 = x_188; +} +lean_ctor_set(x_191, 0, x_190); +lean_ctor_set(x_191, 1, x_187); +return x_191; +} +else +{ +lean_object* x_192; lean_object* x_193; lean_object* x_194; lean_object* x_195; +lean_dec(x_186); +lean_dec(x_184); +x_192 = lean_ctor_get(x_185, 1); +lean_inc(x_192); +if (lean_is_exclusive(x_185)) { + lean_ctor_release(x_185, 0); + lean_ctor_release(x_185, 1); + x_193 = x_185; +} else { + lean_dec_ref(x_185); + x_193 = lean_box(0); +} +x_194 = lean_box(0); +if (lean_is_scalar(x_193)) { + x_195 = lean_alloc_ctor(0, 2, 0); +} else { + x_195 = x_193; +} +lean_ctor_set(x_195, 0, x_194); +lean_ctor_set(x_195, 1, x_192); +return x_195; +} +} +else +{ +lean_object* x_196; lean_object* x_197; lean_object* x_198; lean_object* x_199; +lean_dec(x_184); +x_196 = lean_ctor_get(x_185, 0); +lean_inc(x_196); +x_197 = lean_ctor_get(x_185, 1); +lean_inc(x_197); +if (lean_is_exclusive(x_185)) { + lean_ctor_release(x_185, 0); + lean_ctor_release(x_185, 1); + x_198 = x_185; +} else { + lean_dec_ref(x_185); + x_198 = lean_box(0); +} +if (lean_is_scalar(x_198)) { + x_199 = lean_alloc_ctor(1, 2, 0); +} else { + x_199 = x_198; +} +lean_ctor_set(x_199, 0, x_196); +lean_ctor_set(x_199, 1, x_197); +return x_199; +} +} +} +else +{ +lean_object* x_200; lean_object* x_201; lean_object* x_202; lean_object* x_203; +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +x_200 = lean_ctor_get(x_176, 0); +lean_inc(x_200); +x_201 = lean_ctor_get(x_176, 1); +lean_inc(x_201); +if (lean_is_exclusive(x_176)) { + lean_ctor_release(x_176, 0); + lean_ctor_release(x_176, 1); + x_202 = x_176; +} else { + lean_dec_ref(x_176); + x_202 = lean_box(0); +} +if (lean_is_scalar(x_202)) { + x_203 = lean_alloc_ctor(1, 2, 0); +} else { + x_203 = x_202; +} +lean_ctor_set(x_203, 0, x_200); +lean_ctor_set(x_203, 1, x_201); +return x_203; +} +} +} +} +else +{ +uint8_t x_204; +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_2); +x_204 = !lean_is_exclusive(x_92); +if (x_204 == 0) +{ +return x_92; +} +else +{ +lean_object* x_205; lean_object* x_206; lean_object* x_207; +x_205 = lean_ctor_get(x_92, 0); +x_206 = lean_ctor_get(x_92, 1); +lean_inc(x_206); +lean_inc(x_205); +lean_dec(x_92); +x_207 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_207, 0, x_205); +lean_ctor_set(x_207, 1, x_206); +return x_207; +} +} +} +else +{ +uint8_t x_208; +lean_dec(x_1); +x_208 = !lean_is_exclusive(x_6); +if (x_208 == 0) +{ +lean_object* x_209; uint8_t x_210; +x_209 = lean_ctor_get(x_6, 0); +x_210 = !lean_is_exclusive(x_209); +if (x_210 == 0) +{ +uint8_t x_211; lean_object* x_212; +x_211 = 1; +lean_ctor_set_uint8(x_209, 5, x_211); +x_212 = l_Lean_Meta_unfoldDefinition_x3f(x_2, x_6, x_7, x_8, x_9, x_89); +if (lean_obj_tag(x_212) == 0) +{ +uint8_t x_213; +x_213 = !lean_is_exclusive(x_212); +if (x_213 == 0) +{ +return x_212; +} +else +{ +lean_object* x_214; lean_object* x_215; lean_object* x_216; +x_214 = lean_ctor_get(x_212, 0); +x_215 = lean_ctor_get(x_212, 1); +lean_inc(x_215); +lean_inc(x_214); +lean_dec(x_212); +x_216 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_216, 0, x_214); +lean_ctor_set(x_216, 1, x_215); +return x_216; +} +} +else +{ +uint8_t x_217; +x_217 = !lean_is_exclusive(x_212); +if (x_217 == 0) +{ +return x_212; +} +else +{ +lean_object* x_218; lean_object* x_219; lean_object* x_220; +x_218 = lean_ctor_get(x_212, 0); +x_219 = lean_ctor_get(x_212, 1); +lean_inc(x_219); +lean_inc(x_218); +lean_dec(x_212); +x_220 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_220, 0, x_218); +lean_ctor_set(x_220, 1, x_219); +return x_220; +} +} +} +else +{ +uint8_t x_221; uint8_t x_222; uint8_t x_223; uint8_t x_224; uint8_t x_225; uint8_t x_226; uint8_t x_227; uint8_t x_228; uint8_t x_229; uint8_t x_230; uint8_t x_231; uint8_t x_232; uint8_t x_233; uint8_t x_234; lean_object* x_235; lean_object* x_236; +x_221 = lean_ctor_get_uint8(x_209, 0); +x_222 = lean_ctor_get_uint8(x_209, 1); +x_223 = lean_ctor_get_uint8(x_209, 2); +x_224 = lean_ctor_get_uint8(x_209, 3); +x_225 = lean_ctor_get_uint8(x_209, 4); +x_226 = lean_ctor_get_uint8(x_209, 6); +x_227 = lean_ctor_get_uint8(x_209, 7); +x_228 = lean_ctor_get_uint8(x_209, 8); +x_229 = lean_ctor_get_uint8(x_209, 9); +x_230 = lean_ctor_get_uint8(x_209, 10); +x_231 = lean_ctor_get_uint8(x_209, 11); +x_232 = lean_ctor_get_uint8(x_209, 12); +x_233 = lean_ctor_get_uint8(x_209, 13); +lean_dec(x_209); +x_234 = 1; +x_235 = lean_alloc_ctor(0, 0, 14); +lean_ctor_set_uint8(x_235, 0, x_221); +lean_ctor_set_uint8(x_235, 1, x_222); +lean_ctor_set_uint8(x_235, 2, x_223); +lean_ctor_set_uint8(x_235, 3, x_224); +lean_ctor_set_uint8(x_235, 4, x_225); +lean_ctor_set_uint8(x_235, 5, x_234); +lean_ctor_set_uint8(x_235, 6, x_226); +lean_ctor_set_uint8(x_235, 7, x_227); +lean_ctor_set_uint8(x_235, 8, x_228); +lean_ctor_set_uint8(x_235, 9, x_229); +lean_ctor_set_uint8(x_235, 10, x_230); +lean_ctor_set_uint8(x_235, 11, x_231); +lean_ctor_set_uint8(x_235, 12, x_232); +lean_ctor_set_uint8(x_235, 13, x_233); +lean_ctor_set(x_6, 0, x_235); +x_236 = l_Lean_Meta_unfoldDefinition_x3f(x_2, x_6, x_7, x_8, x_9, x_89); +if (lean_obj_tag(x_236) == 0) +{ +lean_object* x_237; lean_object* x_238; lean_object* x_239; lean_object* x_240; +x_237 = lean_ctor_get(x_236, 0); +lean_inc(x_237); +x_238 = lean_ctor_get(x_236, 1); +lean_inc(x_238); +if (lean_is_exclusive(x_236)) { + lean_ctor_release(x_236, 0); + lean_ctor_release(x_236, 1); + x_239 = x_236; +} else { + lean_dec_ref(x_236); + x_239 = lean_box(0); +} +if (lean_is_scalar(x_239)) { + x_240 = lean_alloc_ctor(0, 2, 0); +} else { + x_240 = x_239; +} +lean_ctor_set(x_240, 0, x_237); +lean_ctor_set(x_240, 1, x_238); +return x_240; +} +else +{ +lean_object* x_241; lean_object* x_242; lean_object* x_243; lean_object* x_244; +x_241 = lean_ctor_get(x_236, 0); +lean_inc(x_241); +x_242 = lean_ctor_get(x_236, 1); +lean_inc(x_242); +if (lean_is_exclusive(x_236)) { + lean_ctor_release(x_236, 0); + lean_ctor_release(x_236, 1); + x_243 = x_236; +} else { + lean_dec_ref(x_236); + x_243 = lean_box(0); +} +if (lean_is_scalar(x_243)) { + x_244 = lean_alloc_ctor(1, 2, 0); +} else { + x_244 = x_243; +} +lean_ctor_set(x_244, 0, x_241); +lean_ctor_set(x_244, 1, x_242); +return x_244; +} +} +} +else +{ +lean_object* x_245; lean_object* x_246; lean_object* x_247; lean_object* x_248; lean_object* x_249; lean_object* x_250; uint8_t x_251; uint8_t x_252; uint8_t x_253; uint8_t x_254; uint8_t x_255; uint8_t x_256; uint8_t x_257; uint8_t x_258; uint8_t x_259; uint8_t x_260; uint8_t x_261; uint8_t x_262; uint8_t x_263; lean_object* x_264; uint8_t x_265; lean_object* x_266; lean_object* x_267; lean_object* x_268; +x_245 = lean_ctor_get(x_6, 0); +x_246 = lean_ctor_get(x_6, 1); +x_247 = lean_ctor_get(x_6, 2); +x_248 = lean_ctor_get(x_6, 3); +x_249 = lean_ctor_get(x_6, 4); +x_250 = lean_ctor_get(x_6, 5); +lean_inc(x_250); +lean_inc(x_249); +lean_inc(x_248); +lean_inc(x_247); +lean_inc(x_246); +lean_inc(x_245); +lean_dec(x_6); +x_251 = lean_ctor_get_uint8(x_245, 0); +x_252 = lean_ctor_get_uint8(x_245, 1); +x_253 = lean_ctor_get_uint8(x_245, 2); +x_254 = lean_ctor_get_uint8(x_245, 3); +x_255 = lean_ctor_get_uint8(x_245, 4); +x_256 = lean_ctor_get_uint8(x_245, 6); +x_257 = lean_ctor_get_uint8(x_245, 7); +x_258 = lean_ctor_get_uint8(x_245, 8); +x_259 = lean_ctor_get_uint8(x_245, 9); +x_260 = lean_ctor_get_uint8(x_245, 10); +x_261 = lean_ctor_get_uint8(x_245, 11); +x_262 = lean_ctor_get_uint8(x_245, 12); +x_263 = lean_ctor_get_uint8(x_245, 13); +if (lean_is_exclusive(x_245)) { + x_264 = x_245; +} else { + lean_dec_ref(x_245); + x_264 = lean_box(0); +} +x_265 = 1; +if (lean_is_scalar(x_264)) { + x_266 = lean_alloc_ctor(0, 0, 14); +} else { + x_266 = x_264; +} +lean_ctor_set_uint8(x_266, 0, x_251); +lean_ctor_set_uint8(x_266, 1, x_252); +lean_ctor_set_uint8(x_266, 2, x_253); +lean_ctor_set_uint8(x_266, 3, x_254); +lean_ctor_set_uint8(x_266, 4, x_255); +lean_ctor_set_uint8(x_266, 5, x_265); +lean_ctor_set_uint8(x_266, 6, x_256); +lean_ctor_set_uint8(x_266, 7, x_257); +lean_ctor_set_uint8(x_266, 8, x_258); +lean_ctor_set_uint8(x_266, 9, x_259); +lean_ctor_set_uint8(x_266, 10, x_260); +lean_ctor_set_uint8(x_266, 11, x_261); +lean_ctor_set_uint8(x_266, 12, x_262); +lean_ctor_set_uint8(x_266, 13, x_263); +x_267 = lean_alloc_ctor(0, 6, 0); +lean_ctor_set(x_267, 0, x_266); +lean_ctor_set(x_267, 1, x_246); +lean_ctor_set(x_267, 2, x_247); +lean_ctor_set(x_267, 3, x_248); +lean_ctor_set(x_267, 4, x_249); +lean_ctor_set(x_267, 5, x_250); +x_268 = l_Lean_Meta_unfoldDefinition_x3f(x_2, x_267, x_7, x_8, x_9, x_89); +if (lean_obj_tag(x_268) == 0) +{ +lean_object* x_269; lean_object* x_270; lean_object* x_271; lean_object* x_272; +x_269 = lean_ctor_get(x_268, 0); +lean_inc(x_269); +x_270 = lean_ctor_get(x_268, 1); +lean_inc(x_270); +if (lean_is_exclusive(x_268)) { + lean_ctor_release(x_268, 0); + lean_ctor_release(x_268, 1); + x_271 = x_268; +} else { + lean_dec_ref(x_268); + x_271 = lean_box(0); +} +if (lean_is_scalar(x_271)) { + x_272 = lean_alloc_ctor(0, 2, 0); +} else { + x_272 = x_271; +} +lean_ctor_set(x_272, 0, x_269); +lean_ctor_set(x_272, 1, x_270); +return x_272; +} +else +{ +lean_object* x_273; lean_object* x_274; lean_object* x_275; lean_object* x_276; +x_273 = lean_ctor_get(x_268, 0); +lean_inc(x_273); +x_274 = lean_ctor_get(x_268, 1); +lean_inc(x_274); +if (lean_is_exclusive(x_268)) { + lean_ctor_release(x_268, 0); + lean_ctor_release(x_268, 1); + x_275 = x_268; +} else { + lean_dec_ref(x_268); + x_275 = lean_box(0); +} +if (lean_is_scalar(x_275)) { + x_276 = lean_alloc_ctor(1, 2, 0); +} else { + x_276 = x_275; +} +lean_ctor_set(x_276, 0, x_273); +lean_ctor_set(x_276, 1, x_274); +return x_276; +} +} +} +} +else +{ +lean_object* x_277; lean_object* x_278; +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_2); +lean_dec(x_1); +x_277 = lean_box(0); +x_278 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_278, 0, x_277); +lean_ctor_set(x_278, 1, x_10); +return x_278; +} +} +} } LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_unfold_x3f___lambda__2(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) { _start: @@ -12361,7 +13609,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_Lean_Meta_Simp_simp_simpStep___closed__1; x_2 = l_Lean_Meta_Simp_simp_simpStep___closed__2; -x_3 = lean_unsigned_to_nat(214u); +x_3 = lean_unsigned_to_nat(245u); x_4 = lean_unsigned_to_nat(26u); x_5 = l_Lean_Meta_Simp_simp_simpStep___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -14584,7 +15832,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_Lean_Meta_Simp_simp_simpStep___closed__1; x_2 = l_Lean_Meta_Simp_simp_simpLet___closed__1; -x_3 = lean_unsigned_to_nat(524u); +x_3 = lean_unsigned_to_nat(555u); x_4 = lean_unsigned_to_nat(35u); x_5 = l_Lean_Meta_Simp_simp_simpStep___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -21989,7 +23237,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_Lean_Meta_Simp_simp_simpStep___closed__1; x_2 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_tryAutoCongrTheorem_x3f___spec__2___closed__1; -x_3 = lean_unsigned_to_nat(329u); +x_3 = lean_unsigned_to_nat(360u); x_4 = lean_unsigned_to_nat(13u); x_5 = l_Lean_Meta_Simp_simp_simpStep___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -25009,7 +26257,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_Lean_Meta_Simp_simp_simpStep___closed__1; x_2 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_tryAutoCongrTheorem_x3f___spec__2___closed__1; -x_3 = lean_unsigned_to_nat(364u); +x_3 = lean_unsigned_to_nat(395u); x_4 = lean_unsigned_to_nat(13u); x_5 = l_Lean_Meta_Simp_simp_simpStep___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -29749,7 +30997,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_Lean_Meta_Simp_simp_simpStep___closed__1; x_2 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simp_tryAutoCongrTheorem_x3f___spec__2___closed__1; -x_3 = lean_unsigned_to_nat(365u); +x_3 = lean_unsigned_to_nat(396u); x_4 = lean_unsigned_to_nat(63u); x_5 = l_Lean_Meta_Simp_simp_simpStep___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -42108,6 +43356,14 @@ l_Lean_getProjectionFnInfo_x3f___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean lean_mark_persistent(l_Lean_getProjectionFnInfo_x3f___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduceProjFn_x3f___spec__1___closed__1); l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduceProjFn_x3f___closed__1 = _init_l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduceProjFn_x3f___closed__1(); lean_mark_persistent(l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduceProjFn_x3f___closed__1); +l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__1 = _init_l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__1(); +lean_mark_persistent(l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__1); +l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__2 = _init_l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__2(); +lean_mark_persistent(l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__2); +l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__3 = _init_l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__3(); +lean_mark_persistent(l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__3); +l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__4 = _init_l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__4(); +lean_mark_persistent(l_Lean_getConstInfo___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_isMatchDef___spec__1___closed__4); l_Lean_throwMaxRecDepthAt___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduce___spec__1___closed__1 = _init_l_Lean_throwMaxRecDepthAt___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduce___spec__1___closed__1(); lean_mark_persistent(l_Lean_throwMaxRecDepthAt___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduce___spec__1___closed__1); l_Lean_throwMaxRecDepthAt___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduce___spec__1___closed__2 = _init_l_Lean_throwMaxRecDepthAt___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduce___spec__1___closed__2();