From 34853bcbd880aa0a19878cc16c7790ecee1ff9d1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Sep 2021 18:55:05 -0700 Subject: [PATCH] chore: update stage0 --- .../src/Lean/Elab/Tactic/BuiltinTactic.lean | 8 +- stage0/src/Lean/Expr.lean | 6 + stage0/src/Lean/Meta.lean | 1 + stage0/src/Lean/Meta/CongrTheorems.lean | 113 + stage0/src/Lean/Meta/FunInfo.lean | 3 + stage0/src/Lean/Meta/Tactic/Cases.lean | 10 +- stage0/src/library/compiler/llnf.cpp | 2 +- .../stdlib/Lean/Elab/Tactic/BuiltinTactic.c | 1644 ++++++++---- stage0/stdlib/Lean/Expr.c | 57 +- stage0/stdlib/Lean/Meta.c | 6 +- stage0/stdlib/Lean/Meta/Closure.c | 12 +- stage0/stdlib/Lean/Meta/CongrTheorems.c | 2279 +++++++++++++++++ stage0/stdlib/Lean/Meta/ExprDefEq.c | 10 +- stage0/stdlib/Lean/Meta/FunInfo.c | 20 + stage0/stdlib/Lean/Meta/Tactic/Cases.c | 6 +- .../stdlib/Lean/Meta/Tactic/Simp/SimpLemmas.c | 2 +- stage0/stdlib/Lean/Meta/Transform.c | 10 +- stage0/stdlib/Lean/MetavarContext.c | 14 +- stage0/stdlib/Lean/Widget/InteractiveCode.c | 6 +- 19 files changed, 3596 insertions(+), 613 deletions(-) create mode 100644 stage0/src/Lean/Meta/CongrTheorems.lean create mode 100644 stage0/stdlib/Lean/Meta/CongrTheorems.c diff --git a/stage0/src/Lean/Elab/Tactic/BuiltinTactic.lean b/stage0/src/Lean/Elab/Tactic/BuiltinTactic.lean index 589d8cd55a..0decab00c0 100644 --- a/stage0/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/stage0/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -220,15 +220,16 @@ def renameInaccessibles (mvarId : MVarId) (hs : Array Syntax) : TacticM MVarId : return mvarId else let mvarDecl ← getMVarDecl mvarId - let mut lctx := mvarDecl.lctx - let mut hs := hs + let mut lctx := mvarDecl.lctx + let mut hs := hs + let mut found : NameSet := {} let n := lctx.numIndices for i in [:n] do let j := n - i - 1 match lctx.getAt? j with | none => pure () | some localDecl => - if localDecl.userName.hasMacroScopes then + if localDecl.userName.hasMacroScopes || found.contains localDecl.userName then let h := hs.back if h.isIdent then let newName := h.getId @@ -236,6 +237,7 @@ def renameInaccessibles (mvarId : MVarId) (hs : Array Syntax) : TacticM MVarId : hs := hs.pop if hs.isEmpty then break + found := found.insert localDecl.userName unless hs.isEmpty do logError m!"too many variable names provided" let mvarNew ← mkFreshExprMVarAt lctx mvarDecl.localInstances mvarDecl.type MetavarKind.syntheticOpaque mvarDecl.userName diff --git a/stage0/src/Lean/Expr.lean b/stage0/src/Lean/Expr.lean index bb64135c77..42b307ea08 100644 --- a/stage0/src/Lean/Expr.lean +++ b/stage0/src/Lean/Expr.lean @@ -872,6 +872,12 @@ def isOptParam (e : Expr) : Bool := def isAutoParam (e : Expr) : Bool := e.isAppOfArity `autoParam 2 +partial def consumeAutoOptParam (e : Expr) : Expr := + if e.isOptParam || e.isAutoParam then + consumeAutoOptParam e.appFn!.appArg! + else + e + /-- Return true iff `e` contains a free variable which statisfies `p`. -/ @[inline] def hasAnyFVar (e : Expr) (p : FVarId → Bool) : Bool := let rec @[specialize] visit (e : Expr) := if !e.hasFVar then false else diff --git a/stage0/src/Lean/Meta.lean b/stage0/src/Lean/Meta.lean index 2c23fb1ca3..db84e59679 100644 --- a/stage0/src/Lean/Meta.lean +++ b/stage0/src/Lean/Meta.lean @@ -37,3 +37,4 @@ import Lean.Meta.GeneralizeVars import Lean.Meta.Injective import Lean.Meta.Structure import Lean.Meta.Constructions +import Lean.Meta.CongrTheorems diff --git a/stage0/src/Lean/Meta/CongrTheorems.lean b/stage0/src/Lean/Meta/CongrTheorems.lean new file mode 100644 index 0000000000..caa5aa31fb --- /dev/null +++ b/stage0/src/Lean/Meta/CongrTheorems.lean @@ -0,0 +1,113 @@ +/- +Copyright (c) 2021 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +import Lean.Meta.AppBuilder + +namespace Lean.Meta + +inductive CongrArgKind where + | /-- It is a parameter for the congruence theorem, the parameter occurs in the left and right hand sides. -/ + fixed + | /-- + It is not a parameter for the congruence theorem, the lemma was specialized for this parameter. + This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it. -/ + fixedNoParam + | /-- + The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : a_i = b_i`. + `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their equality. -/ + eq + | /-- + The congr-simp theorems contains only one parameter for this kind of argument, and congr theorems contains two. + They correspond to arguments that are subsingletons/propositions. -/ + cast + | /-- + The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : HEq a_i b_i`. + `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their heterogeneous equality. -/ + heq + +structure CongrTheorem where + type : Expr + proof : Expr + argKinds : Array CongrArgKind + +private def addPrimeToFVarUserNames (ys : Array Expr) (lctx : LocalContext) : LocalContext := do + let mut lctx := lctx + for y in ys do + let decl := lctx.getFVar! y + lctx := lctx.setUserName decl.fvarId (decl.userName.appendAfter "'") + return lctx + +private def setBinderInfosD (ys : Array Expr) (lctx : LocalContext) : LocalContext := do + let mut lctx := lctx + for y in ys do + let decl := lctx.getFVar! y + lctx := lctx.setBinderInfo decl.fvarId BinderInfo.default + return lctx + +partial def mkHCongrWithArity (f : Expr) (numArgs : Nat) : MetaM CongrTheorem := do + let fType ← inferType f + forallBoundedTelescope fType numArgs fun xs xType => + forallBoundedTelescope fType numArgs fun ys yType => do + if xs.size != numArgs then + throwError "failed to generate hcongr theorem, insufficient number of arguments" + else + let lctx := addPrimeToFVarUserNames ys (← getLCtx) |> setBinderInfosD ys |> setBinderInfosD xs + withLCtx lctx (← getLocalInstances) do + withNewEqs xs ys fun eqs argKinds => do + let mut hs := #[] + for x in xs, y in ys, eq in eqs do + hs := hs.push x |>.push y |>.push eq + let xType := xType.consumeAutoOptParam + let yType := yType.consumeAutoOptParam + let resultType ← if xType == yType then mkEq xType yType else mkHEq xType yType + let congrType ← mkForallFVars hs resultType + return { + type := congrType + proof := (← mkProof congrType) + argKinds + } +where + withNewEqs {α} (xs ys : Array Expr) (k : Array Expr → Array CongrArgKind → MetaM α) : MetaM α := + let rec loop (i : Nat) (eqs : Array Expr) (kinds : Array CongrArgKind) := do + if i < xs.size then + let x := xs[i] + let y := ys[i] + let xType := (← inferType x).consumeAutoOptParam + let yType := (← inferType y).consumeAutoOptParam + if xType == yType then + withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkEq x y) fun h => + loop (i+1) (eqs.push h) (kinds.push CongrArgKind.eq) + else + withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkHEq x y) fun h => + loop (i+1) (eqs.push h) (kinds.push CongrArgKind.heq) + else + k eqs kinds + loop 0 #[] #[] + + mkProof (type : Expr) : MetaM Expr := do + if let some (_, lhs, _) := type.eq? then + mkEqRefl lhs + else if let some (_, lhs, _, _) := type.heq? then + mkHEqRefl lhs + else + forallBoundedTelescope type (some 1) fun a type => + let a := a[0] + forallBoundedTelescope type (some 1) fun b motive => + let b := b[0] + let type := type.bindingBody!.instantiate1 a + withLocalDeclD motive.bindingName! motive.bindingDomain! fun eqPr => do + let type := type.bindingBody! + let motive := motive.bindingBody! + let minor ← mkProof type + let mut major := eqPr + if (← whnf (← inferType eqPr)).isHEq then + major ← mkEqOfHEq major + let motive ← mkLambdaFVars #[b] motive + mkLambdaFVars #[a, b, eqPr] (← mkEqNDRec motive minor major) + +def mkHCongr (f : Expr) : MetaM CongrTheorem := do + mkHCongrWithArity f (← getFunInfo f).getArity + +end Lean.Meta diff --git a/stage0/src/Lean/Meta/FunInfo.lean b/stage0/src/Lean/Meta/FunInfo.lean index db10b9f68b..c77d86bad6 100644 --- a/stage0/src/Lean/Meta/FunInfo.lean +++ b/stage0/src/Lean/Meta/FunInfo.lean @@ -75,4 +75,7 @@ def getFunInfo (fn : Expr) : MetaM FunInfo := def getFunInfoNArgs (fn : Expr) (nargs : Nat) : MetaM FunInfo := getFunInfoAux fn (some nargs) +def FunInfo.getArity (info : FunInfo) : Nat := + info.paramInfo.size + end Lean.Meta diff --git a/stage0/src/Lean/Meta/Tactic/Cases.lean b/stage0/src/Lean/Meta/Tactic/Cases.lean index 3633caa689..66c9aa4898 100644 --- a/stage0/src/Lean/Meta/Tactic/Cases.lean +++ b/stage0/src/Lean/Meta/Tactic/Cases.lean @@ -11,7 +11,7 @@ import Lean.Meta.Tactic.Subst namespace Lean.Meta -private def throwInductiveTypeExpected {α} (type : Expr) : MetaM α := do +private def throwInductiveTypeExpected (type : Expr) : MetaM α := do throwError "failed to compile pattern matching, inductive type expected{indentExpr type}" def getInductiveUniverseAndParams (type : Expr) : MetaM (List Level × Array Expr) := do @@ -31,7 +31,7 @@ private def mkEqAndProof (lhs rhs : Expr) : MetaM (Expr × Expr) := do else pure (mkApp4 (mkConst `HEq [u]) lhsType lhs rhsType rhs, mkApp2 (mkConst `HEq.refl [u]) lhsType lhs) -private partial def withNewEqs {α} (targets targetsNew : Array Expr) (k : Array Expr → Array Expr → MetaM α) : MetaM α := +private partial def withNewEqs (targets targetsNew : Array Expr) (k : Array Expr → Array Expr → MetaM α) : MetaM α := let rec loop (i : Nat) (newEqs : Array Expr) (newRefls : Array Expr) := do if h : i < targets.size then let (newEqType, newRefl) ← mkEqAndProof targets[i] targetsNew[i] @@ -145,7 +145,7 @@ private def mkCasesContext? (majorFVarId : FVarId) : MetaM (Option Context) := d if args.size != ival.numIndices + ival.numParams then pure none else match env.find? (Name.mkStr ival.name "casesOn") with | ConstantInfo.defnInfo cval => - pure $ some { + return some { inductiveVal := ival, casesOnVal := cval, majorDecl := majorDecl, @@ -172,7 +172,7 @@ private def hasIndepIndices (ctx : Context) : MetaM Bool := do else let lctx ← getLCtx let mctx ← getMCtx - pure $ lctx.all fun decl => + return lctx.all fun decl => decl.fvarId == ctx.majorDecl.fvarId || -- decl is the major ctx.majorTypeIndices.any (fun index => decl.fvarId == index.fvarId!) || -- decl is one of the indices mctx.findLocalDeclDependsOn decl (fun fvarId => ctx.majorTypeIndices.all $ fun idx => idx.fvarId! != fvarId) -- or does not depend on any index @@ -280,7 +280,7 @@ private def unifyCasesEqs (numEqs : Nat) (subgoals : Array CasesSubgoal) : MetaM match (← unifyEqs numEqs s.mvarId s.subst s.ctorName) with | none => pure subgoals | some (mvarId, subst) => - pure $ subgoals.push { s with + return subgoals.push { s with mvarId := mvarId, subst := subst, fields := s.fields.map (subst.apply ·) diff --git a/stage0/src/library/compiler/llnf.cpp b/stage0/src/library/compiler/llnf.cpp index 8489fe4c0f..c5cf4867e3 100644 --- a/stage0/src/library/compiler/llnf.cpp +++ b/stage0/src/library/compiler/llnf.cpp @@ -657,7 +657,7 @@ class to_lambda_pure_fn { cnstr_info k_info = get_cnstr_info(const_name(k)); unsigned nparams = k_val.get_nparams(); unsigned cidx = k_info.m_cidx; - name const & I = const_name(k).get_prefix(); + name const & I = k_val.get_induct(); if (optional r = ::lean::is_enum_type(env(), I)) { /* We use a literal for enumeration types. */ expr x = mk_let_decl(*to_uint_type(*r), mk_lit(literal(nat(cidx)))); diff --git a/stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c b/stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c index 4c58b3e322..d8a752a7c6 100644 --- a/stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c +++ b/stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c @@ -45,6 +45,7 @@ lean_object* l_Lean_resolveGlobalConstCore___at_Lean_Elab_Tactic_evalOpen___spec lean_object* l_Lean_Elab_Tactic_evalRotateRight(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_nat_div(lean_object*, lean_object*); lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Std_RBNode_insert___at_Lean_NameSet_insert___spec__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalTacticSeq1Indented(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_forEachVar___spec__1___lambda__1(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_Lean_Elab_Tactic_evalIntros___closed__1; @@ -198,7 +199,6 @@ lean_object* l___private_Lean_Elab_Tactic_BuiltinTactic_0__Lean_Elab_Tactic_find lean_object* l___regBuiltin_Lean_Elab_Tactic_evalAssumption(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalChoice___closed__5; static lean_object* l_Lean_Elab_Tactic_evalSubst___closed__3; -static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___closed__1; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalIntro___closed__2; lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRotateLeft(lean_object*); uint8_t l_Lean_Name_hasMacroScopes(lean_object*); @@ -230,7 +230,7 @@ static lean_object* l_Lean_Elab_Tactic_evalAssumption___rarg___closed__1; static lean_object* l_Lean_Elab_Tactic_evalIntro___closed__15; static lean_object* l_Lean_resolveGlobalConstNoOverloadCore___at_Lean_Elab_Tactic_evalOpen___spec__8___closed__2; static lean_object* l_Lean_Elab_Tactic_evalIntro___closed__18; -lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___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_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___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_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFirst___closed__4; lean_object* lean_st_ref_take(lean_object*, lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_evalManyTacticOptSemi___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*, lean_object*); @@ -269,7 +269,7 @@ lean_object* l_List_foldl___at_Array_appendList___spec__1___rarg(lean_object*, l lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFailIfSuccess(lean_object*); lean_object* l_Lean_Elab_Tactic_closeUsingOrAdmit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFocus___closed__1; -lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___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* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___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*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___closed__3; lean_object* l_Lean_Elab_Tactic_withTacticInfoContext___rarg(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_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalChoiceAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -297,6 +297,7 @@ lean_object* l_Lean_Elab_Tactic_evalIntros___lambda__2(lean_object*, lean_object lean_object* l_Lean_Elab_Tactic_evalFirst(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_evalOpen___spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_getGoals___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___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_object*); static lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Tactic_elabSetOption___spec__3___closed__3; static lean_object* l_Lean_Elab_Tactic_evalAllGoals___closed__1; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__4; @@ -391,6 +392,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalUnknown___closed__4; lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_evalOpen___spec__24(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*); size_t lean_usize_of_nat(lean_object*); lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFirst(lean_object*); +extern lean_object* l_Lean_NameSet_empty; extern lean_object* l_Lean_Elab_Tactic_tacticElabAttribute; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRotateLeft___closed__5; lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*); @@ -473,6 +475,7 @@ lean_object* l_Lean_Elab_Tactic_evalFirst___lambda__1(lean_object*, lean_object* lean_object* l_Lean_Syntax_getArgs(lean_object*); lean_object* l_Lean_Name_append(lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalRotateLeft(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___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* l_Lean_Syntax_getKind(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalAllGoals___closed__4; lean_object* l___private_Lean_Elab_Tactic_BuiltinTactic_0__Lean_Elab_Tactic_sortFVarIds___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -552,6 +555,7 @@ extern lean_object* l_Lean_Elab_unsupportedSyntaxExceptionId; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___closed__4; static lean_object* l_Lean_Elab_Tactic_evalIntro___closed__28; lean_object* l_Lean_Elab_elabSetOption___at_Lean_Elab_Tactic_elabSetOption___spec__1(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_NameSet_contains(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_evalSubst___closed__1; lean_object* l_Lean_Elab_Tactic_evalIntros(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_evalManyTacticOptSemi(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -13613,48 +13617,67 @@ lean_dec(x_3); return x_12; } } -lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___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, lean_object* x_11, lean_object* x_12) { +lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___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, lean_object* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14) { _start: { -lean_object* x_13; uint8_t x_14; -x_13 = lean_array_pop(x_2); -x_14 = l_Array_isEmpty___rarg(x_13); -if (x_14 == 0) +lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; +x_15 = l_Lean_LocalDecl_userName(x_1); +x_16 = lean_box(0); +x_17 = l_Std_RBNode_insert___at_Lean_NameSet_insert___spec__1(x_2, x_15, x_16); +x_18 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_18, 0, x_3); +lean_ctor_set(x_18, 1, x_4); +x_19 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_19, 0, x_17); +lean_ctor_set(x_19, 1, x_18); +x_20 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_20, 0, x_19); +x_21 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_21, 0, x_20); +lean_ctor_set(x_21, 1, x_14); +return x_21; +} +} +lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___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, lean_object* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14) { +_start: { -lean_object* x_15; lean_object* x_16; lean_object* x_17; -x_15 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_15, 0, x_1); -lean_ctor_set(x_15, 1, x_13); -x_16 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_16, 0, x_15); -x_17 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_17, 0, x_16); -lean_ctor_set(x_17, 1, x_12); -return x_17; +lean_object* x_15; uint8_t x_16; +x_15 = lean_array_pop(x_4); +x_16 = l_Array_isEmpty___rarg(x_15); +if (x_16 == 0) +{ +lean_object* x_17; lean_object* x_18; +x_17 = lean_box(0); +x_18 = lean_apply_13(x_1, x_2, x_3, x_15, x_17, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +return x_18; } else { -lean_object* x_18; lean_object* x_19; lean_object* x_20; -x_18 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_18, 0, x_1); -lean_ctor_set(x_18, 1, x_13); -x_19 = lean_alloc_ctor(0, 1, 0); -lean_ctor_set(x_19, 0, x_18); +lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; +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); +lean_dec(x_1); +x_19 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_19, 0, x_3); +lean_ctor_set(x_19, 1, x_15); x_20 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_20, 0, x_19); -lean_ctor_set(x_20, 1, x_12); -return x_20; +lean_ctor_set(x_20, 0, x_2); +lean_ctor_set(x_20, 1, x_19); +x_21 = lean_alloc_ctor(0, 1, 0); +lean_ctor_set(x_21, 0, 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_14); +return x_22; } } } -static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___closed__1() { -_start: -{ -lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__1___boxed), 12, 0); -return x_1; -} -} lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14) { _start: { @@ -13668,179 +13691,81 @@ x_17 = lean_unsigned_to_nat(0u); x_18 = lean_nat_dec_eq(x_3, x_17); if (x_18 == 0) { -lean_object* x_19; lean_object* x_20; uint8_t x_21; +lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_30; x_19 = lean_unsigned_to_nat(1u); x_20 = lean_nat_sub(x_3, x_19); lean_dec(x_3); -x_21 = !lean_is_exclusive(x_5); -if (x_21 == 0) +x_30 = !lean_is_exclusive(x_5); +if (x_30 == 0) { -lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; -x_22 = lean_ctor_get(x_5, 0); -x_23 = lean_ctor_get(x_5, 1); -x_24 = lean_nat_sub(x_1, x_4); -x_25 = lean_nat_sub(x_24, x_19); -lean_dec(x_24); -lean_inc(x_22); -x_26 = lean_local_ctx_get(x_22, x_25); -if (lean_obj_tag(x_26) == 0) -{ -lean_object* x_27; lean_object* x_28; -x_27 = lean_ctor_get(x_2, 2); -x_28 = lean_nat_add(x_4, x_27); -lean_dec(x_4); -x_3 = x_20; -x_4 = x_28; -goto _start; -} -else -{ -lean_object* x_30; lean_object* x_31; uint8_t x_32; -x_30 = lean_ctor_get(x_26, 0); -lean_inc(x_30); -lean_dec(x_26); -x_31 = l_Lean_LocalDecl_userName(x_30); -x_32 = l_Lean_Name_hasMacroScopes(x_31); -lean_dec(x_31); +lean_object* x_31; uint8_t x_32; +x_31 = lean_ctor_get(x_5, 1); +x_32 = !lean_is_exclusive(x_31); if (x_32 == 0) { -lean_object* x_33; lean_object* x_34; -lean_dec(x_30); -x_33 = lean_ctor_get(x_2, 2); -x_34 = lean_nat_add(x_4, x_33); -lean_dec(x_4); -x_3 = x_20; -x_4 = x_34; -goto _start; +lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; +x_33 = lean_ctor_get(x_5, 0); +x_34 = lean_ctor_get(x_31, 0); +x_35 = lean_ctor_get(x_31, 1); +x_36 = lean_nat_sub(x_1, x_4); +x_37 = lean_nat_sub(x_36, x_19); +lean_dec(x_36); +lean_inc(x_34); +x_38 = lean_local_ctx_get(x_34, x_37); +if (lean_obj_tag(x_38) == 0) +{ +lean_object* x_39; +x_39 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_39, 0, x_5); +x_21 = x_39; +x_22 = x_14; +goto block_29; } else { -lean_object* x_36; lean_object* x_37; uint8_t x_38; +lean_object* x_40; lean_object* x_41; lean_object* x_42; uint8_t x_43; +lean_free_object(x_31); lean_free_object(x_5); -x_36 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_23); -x_37 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___closed__1; -x_38 = l_Lean_Syntax_isIdent(x_36); -if (x_38 == 0) +x_40 = lean_ctor_get(x_38, 0); +lean_inc(x_40); +lean_dec(x_38); +lean_inc(x_40); +x_41 = lean_alloc_closure((void*)(l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__1___boxed), 14, 1); +lean_closure_set(x_41, 0, x_40); +x_42 = l_Lean_LocalDecl_userName(x_40); +x_43 = l_Lean_Name_hasMacroScopes(x_42); +if (x_43 == 0) { -lean_object* x_39; lean_object* x_40; -lean_dec(x_36); -lean_dec(x_30); -x_39 = 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_40 = lean_apply_12(x_37, x_22, x_23, x_39, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); -if (lean_obj_tag(x_40) == 0) +uint8_t x_44; +x_44 = l_Lean_NameSet_contains(x_33, x_42); +lean_dec(x_42); +if (x_44 == 0) { -lean_object* x_41; -x_41 = lean_ctor_get(x_40, 0); -lean_inc(x_41); -if (lean_obj_tag(x_41) == 0) -{ -uint8_t x_42; -lean_dec(x_20); -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); -lean_dec(x_4); -x_42 = !lean_is_exclusive(x_40); -if (x_42 == 0) -{ -lean_object* x_43; lean_object* x_44; -x_43 = lean_ctor_get(x_40, 0); -lean_dec(x_43); -x_44 = lean_ctor_get(x_41, 0); -lean_inc(x_44); +lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_dec(x_41); -lean_ctor_set(x_40, 0, x_44); -return x_40; -} -else -{ -lean_object* x_45; lean_object* x_46; lean_object* x_47; -x_45 = lean_ctor_get(x_40, 1); -lean_inc(x_45); +x_45 = lean_box(0); +x_46 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__1(x_40, x_33, x_34, x_35, x_45, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); lean_dec(x_40); -x_46 = lean_ctor_get(x_41, 0); -lean_inc(x_46); -lean_dec(x_41); -x_47 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_47, 0, x_46); -lean_ctor_set(x_47, 1, x_45); -return x_47; -} -} -else -{ -lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; -x_48 = lean_ctor_get(x_40, 1); +x_47 = lean_ctor_get(x_46, 0); +lean_inc(x_47); +x_48 = lean_ctor_get(x_46, 1); lean_inc(x_48); +lean_dec(x_46); +x_21 = x_47; +x_22 = x_48; +goto block_29; +} +else +{ +lean_object* x_49; uint8_t x_50; +x_49 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_35); +x_50 = l_Lean_Syntax_isIdent(x_49); +if (x_50 == 0) +{ +lean_object* x_51; lean_object* x_52; +lean_dec(x_49); lean_dec(x_40); -x_49 = lean_ctor_get(x_41, 0); -lean_inc(x_49); -lean_dec(x_41); -x_50 = lean_ctor_get(x_2, 2); -x_51 = lean_nat_add(x_4, x_50); -lean_dec(x_4); -x_3 = x_20; -x_4 = x_51; -x_5 = x_49; -x_14 = x_48; -goto _start; -} -} -else -{ -uint8_t x_53; -lean_dec(x_20); -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); -lean_dec(x_4); -x_53 = !lean_is_exclusive(x_40); -if (x_53 == 0) -{ -return x_40; -} -else -{ -lean_object* x_54; lean_object* x_55; lean_object* x_56; -x_54 = lean_ctor_get(x_40, 0); -x_55 = lean_ctor_get(x_40, 1); -lean_inc(x_55); -lean_inc(x_54); -lean_dec(x_40); -x_56 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_56, 0, x_54); -lean_ctor_set(x_56, 1, x_55); -return x_56; -} -} -} -else -{ -lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; -x_57 = l_Lean_Syntax_getId(x_36); -lean_dec(x_36); -x_58 = l_Lean_LocalDecl_fvarId(x_30); -lean_dec(x_30); -x_59 = l_Lean_LocalContext_setUserName(x_22, x_58, x_57); -x_60 = lean_box(0); +x_51 = lean_box(0); lean_inc(x_13); lean_inc(x_12); lean_inc(x_11); @@ -13849,15 +13774,22 @@ lean_inc(x_9); lean_inc(x_8); lean_inc(x_7); lean_inc(x_6); -x_61 = lean_apply_12(x_37, x_59, x_23, x_60, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); -if (lean_obj_tag(x_61) == 0) +x_52 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(x_41, x_33, x_34, x_35, x_51, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_52) == 0) { -lean_object* x_62; -x_62 = lean_ctor_get(x_61, 0); -lean_inc(x_62); -if (lean_obj_tag(x_62) == 0) +lean_object* x_53; lean_object* x_54; +x_53 = lean_ctor_get(x_52, 0); +lean_inc(x_53); +x_54 = lean_ctor_get(x_52, 1); +lean_inc(x_54); +lean_dec(x_52); +x_21 = x_53; +x_22 = x_54; +goto block_29; +} +else { -uint8_t x_63; +uint8_t x_55; lean_dec(x_20); lean_dec(x_13); lean_dec(x_12); @@ -13868,55 +13800,59 @@ lean_dec(x_8); lean_dec(x_7); lean_dec(x_6); lean_dec(x_4); -x_63 = !lean_is_exclusive(x_61); -if (x_63 == 0) +x_55 = !lean_is_exclusive(x_52); +if (x_55 == 0) +{ +return x_52; +} +else +{ +lean_object* x_56; lean_object* x_57; lean_object* x_58; +x_56 = lean_ctor_get(x_52, 0); +x_57 = lean_ctor_get(x_52, 1); +lean_inc(x_57); +lean_inc(x_56); +lean_dec(x_52); +x_58 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_58, 0, x_56); +lean_ctor_set(x_58, 1, x_57); +return x_58; +} +} +} +else +{ +lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; +x_59 = l_Lean_Syntax_getId(x_49); +lean_dec(x_49); +x_60 = l_Lean_LocalDecl_fvarId(x_40); +lean_dec(x_40); +x_61 = l_Lean_LocalContext_setUserName(x_34, x_60, x_59); +x_62 = 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_63 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(x_41, x_33, x_61, x_35, x_62, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_63) == 0) { lean_object* x_64; lean_object* x_65; -x_64 = lean_ctor_get(x_61, 0); -lean_dec(x_64); -x_65 = lean_ctor_get(x_62, 0); +x_64 = lean_ctor_get(x_63, 0); +lean_inc(x_64); +x_65 = lean_ctor_get(x_63, 1); lean_inc(x_65); -lean_dec(x_62); -lean_ctor_set(x_61, 0, x_65); -return x_61; +lean_dec(x_63); +x_21 = x_64; +x_22 = x_65; +goto block_29; } else { -lean_object* x_66; lean_object* x_67; lean_object* x_68; -x_66 = lean_ctor_get(x_61, 1); -lean_inc(x_66); -lean_dec(x_61); -x_67 = lean_ctor_get(x_62, 0); -lean_inc(x_67); -lean_dec(x_62); -x_68 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_68, 0, x_67); -lean_ctor_set(x_68, 1, x_66); -return x_68; -} -} -else -{ -lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; -x_69 = lean_ctor_get(x_61, 1); -lean_inc(x_69); -lean_dec(x_61); -x_70 = lean_ctor_get(x_62, 0); -lean_inc(x_70); -lean_dec(x_62); -x_71 = lean_ctor_get(x_2, 2); -x_72 = lean_nat_add(x_4, x_71); -lean_dec(x_4); -x_3 = x_20; -x_4 = x_72; -x_5 = x_70; -x_14 = x_69; -goto _start; -} -} -else -{ -uint8_t x_74; +uint8_t x_66; lean_dec(x_20); lean_dec(x_13); lean_dec(x_12); @@ -13927,204 +13863,231 @@ lean_dec(x_8); lean_dec(x_7); lean_dec(x_6); lean_dec(x_4); -x_74 = !lean_is_exclusive(x_61); -if (x_74 == 0) +x_66 = !lean_is_exclusive(x_63); +if (x_66 == 0) { -return x_61; +return x_63; } else { -lean_object* x_75; lean_object* x_76; lean_object* x_77; -x_75 = lean_ctor_get(x_61, 0); -x_76 = lean_ctor_get(x_61, 1); -lean_inc(x_76); +lean_object* x_67; lean_object* x_68; lean_object* x_69; +x_67 = lean_ctor_get(x_63, 0); +x_68 = lean_ctor_get(x_63, 1); +lean_inc(x_68); +lean_inc(x_67); +lean_dec(x_63); +x_69 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_69, 0, x_67); +lean_ctor_set(x_69, 1, x_68); +return x_69; +} +} +} +} +} +else +{ +lean_object* x_70; uint8_t x_71; +lean_dec(x_42); +x_70 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_35); +x_71 = l_Lean_Syntax_isIdent(x_70); +if (x_71 == 0) +{ +lean_object* x_72; lean_object* x_73; +lean_dec(x_70); +lean_dec(x_40); +x_72 = 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_73 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(x_41, x_33, x_34, x_35, x_72, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_73) == 0) +{ +lean_object* x_74; lean_object* x_75; +x_74 = lean_ctor_get(x_73, 0); +lean_inc(x_74); +x_75 = lean_ctor_get(x_73, 1); lean_inc(x_75); -lean_dec(x_61); -x_77 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_77, 0, x_75); -lean_ctor_set(x_77, 1, x_76); -return x_77; -} -} -} -} -} +lean_dec(x_73); +x_21 = x_74; +x_22 = x_75; +goto block_29; } else { -lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; -x_78 = lean_ctor_get(x_5, 0); -x_79 = lean_ctor_get(x_5, 1); -lean_inc(x_79); -lean_inc(x_78); -lean_dec(x_5); -x_80 = lean_nat_sub(x_1, x_4); -x_81 = lean_nat_sub(x_80, x_19); -lean_dec(x_80); -lean_inc(x_78); -x_82 = lean_local_ctx_get(x_78, x_81); -if (lean_obj_tag(x_82) == 0) -{ -lean_object* x_83; lean_object* x_84; lean_object* x_85; -x_83 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_83, 0, x_78); -lean_ctor_set(x_83, 1, x_79); -x_84 = lean_ctor_get(x_2, 2); -x_85 = lean_nat_add(x_4, x_84); +uint8_t x_76; +lean_dec(x_20); +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); lean_dec(x_4); -x_3 = x_20; -x_4 = x_85; -x_5 = x_83; -goto _start; +x_76 = !lean_is_exclusive(x_73); +if (x_76 == 0) +{ +return x_73; } else { -lean_object* x_87; lean_object* x_88; uint8_t x_89; -x_87 = lean_ctor_get(x_82, 0); -lean_inc(x_87); -lean_dec(x_82); -x_88 = l_Lean_LocalDecl_userName(x_87); -x_89 = l_Lean_Name_hasMacroScopes(x_88); -lean_dec(x_88); -if (x_89 == 0) +lean_object* x_77; lean_object* x_78; lean_object* x_79; +x_77 = lean_ctor_get(x_73, 0); +x_78 = lean_ctor_get(x_73, 1); +lean_inc(x_78); +lean_inc(x_77); +lean_dec(x_73); +x_79 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_79, 0, x_77); +lean_ctor_set(x_79, 1, x_78); +return x_79; +} +} +} +else { -lean_object* x_90; lean_object* x_91; lean_object* x_92; -lean_dec(x_87); -x_90 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_90, 0, x_78); -lean_ctor_set(x_90, 1, x_79); -x_91 = lean_ctor_get(x_2, 2); -x_92 = lean_nat_add(x_4, x_91); +lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; +x_80 = l_Lean_Syntax_getId(x_70); +lean_dec(x_70); +x_81 = l_Lean_LocalDecl_fvarId(x_40); +lean_dec(x_40); +x_82 = l_Lean_LocalContext_setUserName(x_34, x_81, x_80); +x_83 = 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_84 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(x_41, x_33, x_82, x_35, x_83, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_84) == 0) +{ +lean_object* x_85; lean_object* x_86; +x_85 = lean_ctor_get(x_84, 0); +lean_inc(x_85); +x_86 = lean_ctor_get(x_84, 1); +lean_inc(x_86); +lean_dec(x_84); +x_21 = x_85; +x_22 = x_86; +goto block_29; +} +else +{ +uint8_t x_87; +lean_dec(x_20); +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); lean_dec(x_4); -x_3 = x_20; -x_4 = x_92; -x_5 = x_90; -goto _start; +x_87 = !lean_is_exclusive(x_84); +if (x_87 == 0) +{ +return x_84; } else { -lean_object* x_94; lean_object* x_95; uint8_t x_96; -x_94 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_79); -x_95 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___closed__1; -x_96 = l_Lean_Syntax_isIdent(x_94); -if (x_96 == 0) +lean_object* x_88; lean_object* x_89; lean_object* x_90; +x_88 = lean_ctor_get(x_84, 0); +x_89 = lean_ctor_get(x_84, 1); +lean_inc(x_89); +lean_inc(x_88); +lean_dec(x_84); +x_90 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_90, 0, x_88); +lean_ctor_set(x_90, 1, x_89); +return x_90; +} +} +} +} +} +} +else +{ +lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; +x_91 = lean_ctor_get(x_5, 0); +x_92 = lean_ctor_get(x_31, 0); +x_93 = lean_ctor_get(x_31, 1); +lean_inc(x_93); +lean_inc(x_92); +lean_dec(x_31); +x_94 = lean_nat_sub(x_1, x_4); +x_95 = lean_nat_sub(x_94, x_19); +lean_dec(x_94); +lean_inc(x_92); +x_96 = lean_local_ctx_get(x_92, x_95); +if (lean_obj_tag(x_96) == 0) { lean_object* x_97; lean_object* x_98; -lean_dec(x_94); -lean_dec(x_87); -x_97 = 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_98 = lean_apply_12(x_95, x_78, x_79, x_97, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); -if (lean_obj_tag(x_98) == 0) -{ -lean_object* x_99; -x_99 = lean_ctor_get(x_98, 0); -lean_inc(x_99); -if (lean_obj_tag(x_99) == 0) -{ -lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; -lean_dec(x_20); -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); -lean_dec(x_4); -x_100 = lean_ctor_get(x_98, 1); -lean_inc(x_100); -if (lean_is_exclusive(x_98)) { - lean_ctor_release(x_98, 0); - lean_ctor_release(x_98, 1); - x_101 = x_98; -} else { - lean_dec_ref(x_98); - x_101 = lean_box(0); -} -x_102 = lean_ctor_get(x_99, 0); -lean_inc(x_102); -lean_dec(x_99); -if (lean_is_scalar(x_101)) { - x_103 = lean_alloc_ctor(0, 2, 0); -} else { - x_103 = x_101; -} -lean_ctor_set(x_103, 0, x_102); -lean_ctor_set(x_103, 1, x_100); -return x_103; +x_97 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_97, 0, x_92); +lean_ctor_set(x_97, 1, x_93); +lean_ctor_set(x_5, 1, x_97); +x_98 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_98, 0, x_5); +x_21 = x_98; +x_22 = x_14; +goto block_29; } else { +lean_object* x_99; lean_object* x_100; lean_object* x_101; uint8_t x_102; +lean_free_object(x_5); +x_99 = lean_ctor_get(x_96, 0); +lean_inc(x_99); +lean_dec(x_96); +lean_inc(x_99); +x_100 = lean_alloc_closure((void*)(l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__1___boxed), 14, 1); +lean_closure_set(x_100, 0, x_99); +x_101 = l_Lean_LocalDecl_userName(x_99); +x_102 = l_Lean_Name_hasMacroScopes(x_101); +if (x_102 == 0) +{ +uint8_t x_103; +x_103 = l_Lean_NameSet_contains(x_91, x_101); +lean_dec(x_101); +if (x_103 == 0) +{ lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; -x_104 = lean_ctor_get(x_98, 1); -lean_inc(x_104); -lean_dec(x_98); -x_105 = lean_ctor_get(x_99, 0); -lean_inc(x_105); +lean_dec(x_100); +x_104 = lean_box(0); +x_105 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__1(x_99, x_91, x_92, x_93, x_104, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); lean_dec(x_99); -x_106 = lean_ctor_get(x_2, 2); -x_107 = lean_nat_add(x_4, x_106); -lean_dec(x_4); -x_3 = x_20; -x_4 = x_107; -x_5 = x_105; -x_14 = x_104; -goto _start; -} +x_106 = lean_ctor_get(x_105, 0); +lean_inc(x_106); +x_107 = lean_ctor_get(x_105, 1); +lean_inc(x_107); +lean_dec(x_105); +x_21 = x_106; +x_22 = x_107; +goto block_29; } else { -lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; -lean_dec(x_20); -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); -lean_dec(x_4); -x_109 = lean_ctor_get(x_98, 0); -lean_inc(x_109); -x_110 = lean_ctor_get(x_98, 1); -lean_inc(x_110); -if (lean_is_exclusive(x_98)) { - lean_ctor_release(x_98, 0); - lean_ctor_release(x_98, 1); - x_111 = x_98; -} else { - lean_dec_ref(x_98); - x_111 = lean_box(0); -} -if (lean_is_scalar(x_111)) { - x_112 = lean_alloc_ctor(1, 2, 0); -} else { - x_112 = x_111; -} -lean_ctor_set(x_112, 0, x_109); -lean_ctor_set(x_112, 1, x_110); -return x_112; -} -} -else +lean_object* x_108; uint8_t x_109; +x_108 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_93); +x_109 = l_Lean_Syntax_isIdent(x_108); +if (x_109 == 0) { -lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; -x_113 = l_Lean_Syntax_getId(x_94); -lean_dec(x_94); -x_114 = l_Lean_LocalDecl_fvarId(x_87); -lean_dec(x_87); -x_115 = l_Lean_LocalContext_setUserName(x_78, x_114, x_113); -x_116 = lean_box(0); +lean_object* x_110; lean_object* x_111; +lean_dec(x_108); +lean_dec(x_99); +x_110 = lean_box(0); lean_inc(x_13); lean_inc(x_12); lean_inc(x_11); @@ -14133,15 +14096,22 @@ lean_inc(x_9); lean_inc(x_8); lean_inc(x_7); lean_inc(x_6); -x_117 = lean_apply_12(x_95, x_115, x_79, x_116, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); -if (lean_obj_tag(x_117) == 0) +x_111 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(x_100, x_91, x_92, x_93, x_110, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_111) == 0) { -lean_object* x_118; -x_118 = lean_ctor_get(x_117, 0); -lean_inc(x_118); -if (lean_obj_tag(x_118) == 0) +lean_object* x_112; lean_object* x_113; +x_112 = lean_ctor_get(x_111, 0); +lean_inc(x_112); +x_113 = lean_ctor_get(x_111, 1); +lean_inc(x_113); +lean_dec(x_111); +x_21 = x_112; +x_22 = x_113; +goto block_29; +} +else { -lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; +lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_dec(x_20); lean_dec(x_13); lean_dec(x_12); @@ -14152,89 +14122,622 @@ lean_dec(x_8); lean_dec(x_7); lean_dec(x_6); lean_dec(x_4); -x_119 = lean_ctor_get(x_117, 1); -lean_inc(x_119); -if (lean_is_exclusive(x_117)) { - lean_ctor_release(x_117, 0); - lean_ctor_release(x_117, 1); - x_120 = x_117; +x_114 = lean_ctor_get(x_111, 0); +lean_inc(x_114); +x_115 = lean_ctor_get(x_111, 1); +lean_inc(x_115); +if (lean_is_exclusive(x_111)) { + lean_ctor_release(x_111, 0); + lean_ctor_release(x_111, 1); + x_116 = x_111; } else { - lean_dec_ref(x_117); - x_120 = lean_box(0); + lean_dec_ref(x_111); + x_116 = lean_box(0); } -x_121 = lean_ctor_get(x_118, 0); -lean_inc(x_121); -lean_dec(x_118); -if (lean_is_scalar(x_120)) { - x_122 = lean_alloc_ctor(0, 2, 0); +if (lean_is_scalar(x_116)) { + x_117 = lean_alloc_ctor(1, 2, 0); } else { - x_122 = x_120; + x_117 = x_116; +} +lean_ctor_set(x_117, 0, x_114); +lean_ctor_set(x_117, 1, x_115); +return x_117; } -lean_ctor_set(x_122, 0, x_121); -lean_ctor_set(x_122, 1, x_119); -return x_122; } else { -lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; -x_123 = lean_ctor_get(x_117, 1); +lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; +x_118 = l_Lean_Syntax_getId(x_108); +lean_dec(x_108); +x_119 = l_Lean_LocalDecl_fvarId(x_99); +lean_dec(x_99); +x_120 = l_Lean_LocalContext_setUserName(x_92, x_119, x_118); +x_121 = 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_122 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(x_100, x_91, x_120, x_93, x_121, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_122) == 0) +{ +lean_object* x_123; lean_object* x_124; +x_123 = lean_ctor_get(x_122, 0); lean_inc(x_123); -lean_dec(x_117); -x_124 = lean_ctor_get(x_118, 0); +x_124 = lean_ctor_get(x_122, 1); lean_inc(x_124); -lean_dec(x_118); -x_125 = lean_ctor_get(x_2, 2); -x_126 = lean_nat_add(x_4, x_125); +lean_dec(x_122); +x_21 = x_123; +x_22 = x_124; +goto block_29; +} +else +{ +lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; +lean_dec(x_20); +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); +lean_dec(x_4); +x_125 = lean_ctor_get(x_122, 0); +lean_inc(x_125); +x_126 = lean_ctor_get(x_122, 1); +lean_inc(x_126); +if (lean_is_exclusive(x_122)) { + lean_ctor_release(x_122, 0); + lean_ctor_release(x_122, 1); + x_127 = x_122; +} else { + lean_dec_ref(x_122); + x_127 = lean_box(0); +} +if (lean_is_scalar(x_127)) { + x_128 = lean_alloc_ctor(1, 2, 0); +} else { + x_128 = x_127; +} +lean_ctor_set(x_128, 0, x_125); +lean_ctor_set(x_128, 1, x_126); +return x_128; +} +} +} +} +else +{ +lean_object* x_129; uint8_t x_130; +lean_dec(x_101); +x_129 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_93); +x_130 = l_Lean_Syntax_isIdent(x_129); +if (x_130 == 0) +{ +lean_object* x_131; lean_object* x_132; +lean_dec(x_129); +lean_dec(x_99); +x_131 = 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_132 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(x_100, x_91, x_92, x_93, x_131, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_132) == 0) +{ +lean_object* x_133; lean_object* x_134; +x_133 = lean_ctor_get(x_132, 0); +lean_inc(x_133); +x_134 = lean_ctor_get(x_132, 1); +lean_inc(x_134); +lean_dec(x_132); +x_21 = x_133; +x_22 = x_134; +goto block_29; +} +else +{ +lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; +lean_dec(x_20); +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); +lean_dec(x_4); +x_135 = lean_ctor_get(x_132, 0); +lean_inc(x_135); +x_136 = lean_ctor_get(x_132, 1); +lean_inc(x_136); +if (lean_is_exclusive(x_132)) { + lean_ctor_release(x_132, 0); + lean_ctor_release(x_132, 1); + x_137 = x_132; +} else { + lean_dec_ref(x_132); + x_137 = lean_box(0); +} +if (lean_is_scalar(x_137)) { + x_138 = lean_alloc_ctor(1, 2, 0); +} else { + x_138 = x_137; +} +lean_ctor_set(x_138, 0, x_135); +lean_ctor_set(x_138, 1, x_136); +return x_138; +} +} +else +{ +lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; +x_139 = l_Lean_Syntax_getId(x_129); +lean_dec(x_129); +x_140 = l_Lean_LocalDecl_fvarId(x_99); +lean_dec(x_99); +x_141 = l_Lean_LocalContext_setUserName(x_92, x_140, x_139); +x_142 = 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_143 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(x_100, x_91, x_141, x_93, x_142, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_143) == 0) +{ +lean_object* x_144; lean_object* x_145; +x_144 = lean_ctor_get(x_143, 0); +lean_inc(x_144); +x_145 = lean_ctor_get(x_143, 1); +lean_inc(x_145); +lean_dec(x_143); +x_21 = x_144; +x_22 = x_145; +goto block_29; +} +else +{ +lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; +lean_dec(x_20); +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); +lean_dec(x_4); +x_146 = lean_ctor_get(x_143, 0); +lean_inc(x_146); +x_147 = lean_ctor_get(x_143, 1); +lean_inc(x_147); +if (lean_is_exclusive(x_143)) { + lean_ctor_release(x_143, 0); + lean_ctor_release(x_143, 1); + x_148 = x_143; +} else { + lean_dec_ref(x_143); + x_148 = lean_box(0); +} +if (lean_is_scalar(x_148)) { + x_149 = lean_alloc_ctor(1, 2, 0); +} else { + x_149 = x_148; +} +lean_ctor_set(x_149, 0, x_146); +lean_ctor_set(x_149, 1, x_147); +return x_149; +} +} +} +} +} +} +else +{ +lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; +x_150 = lean_ctor_get(x_5, 1); +x_151 = lean_ctor_get(x_5, 0); +lean_inc(x_150); +lean_inc(x_151); +lean_dec(x_5); +x_152 = lean_ctor_get(x_150, 0); +lean_inc(x_152); +x_153 = lean_ctor_get(x_150, 1); +lean_inc(x_153); +if (lean_is_exclusive(x_150)) { + lean_ctor_release(x_150, 0); + lean_ctor_release(x_150, 1); + x_154 = x_150; +} else { + lean_dec_ref(x_150); + x_154 = lean_box(0); +} +x_155 = lean_nat_sub(x_1, x_4); +x_156 = lean_nat_sub(x_155, x_19); +lean_dec(x_155); +lean_inc(x_152); +x_157 = lean_local_ctx_get(x_152, x_156); +if (lean_obj_tag(x_157) == 0) +{ +lean_object* x_158; lean_object* x_159; lean_object* x_160; +if (lean_is_scalar(x_154)) { + x_158 = lean_alloc_ctor(0, 2, 0); +} else { + x_158 = x_154; +} +lean_ctor_set(x_158, 0, x_152); +lean_ctor_set(x_158, 1, x_153); +x_159 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_159, 0, x_151); +lean_ctor_set(x_159, 1, x_158); +x_160 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_160, 0, x_159); +x_21 = x_160; +x_22 = x_14; +goto block_29; +} +else +{ +lean_object* x_161; lean_object* x_162; lean_object* x_163; uint8_t x_164; +lean_dec(x_154); +x_161 = lean_ctor_get(x_157, 0); +lean_inc(x_161); +lean_dec(x_157); +lean_inc(x_161); +x_162 = lean_alloc_closure((void*)(l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__1___boxed), 14, 1); +lean_closure_set(x_162, 0, x_161); +x_163 = l_Lean_LocalDecl_userName(x_161); +x_164 = l_Lean_Name_hasMacroScopes(x_163); +if (x_164 == 0) +{ +uint8_t x_165; +x_165 = l_Lean_NameSet_contains(x_151, x_163); +lean_dec(x_163); +if (x_165 == 0) +{ +lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; +lean_dec(x_162); +x_166 = lean_box(0); +x_167 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__1(x_161, x_151, x_152, x_153, x_166, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +lean_dec(x_161); +x_168 = lean_ctor_get(x_167, 0); +lean_inc(x_168); +x_169 = lean_ctor_get(x_167, 1); +lean_inc(x_169); +lean_dec(x_167); +x_21 = x_168; +x_22 = x_169; +goto block_29; +} +else +{ +lean_object* x_170; uint8_t x_171; +x_170 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_153); +x_171 = l_Lean_Syntax_isIdent(x_170); +if (x_171 == 0) +{ +lean_object* x_172; lean_object* x_173; +lean_dec(x_170); +lean_dec(x_161); +x_172 = 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_173 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(x_162, x_151, x_152, x_153, x_172, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_173) == 0) +{ +lean_object* x_174; lean_object* x_175; +x_174 = lean_ctor_get(x_173, 0); +lean_inc(x_174); +x_175 = lean_ctor_get(x_173, 1); +lean_inc(x_175); +lean_dec(x_173); +x_21 = x_174; +x_22 = x_175; +goto block_29; +} +else +{ +lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; +lean_dec(x_20); +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); +lean_dec(x_4); +x_176 = lean_ctor_get(x_173, 0); +lean_inc(x_176); +x_177 = lean_ctor_get(x_173, 1); +lean_inc(x_177); +if (lean_is_exclusive(x_173)) { + lean_ctor_release(x_173, 0); + lean_ctor_release(x_173, 1); + x_178 = x_173; +} else { + lean_dec_ref(x_173); + x_178 = lean_box(0); +} +if (lean_is_scalar(x_178)) { + x_179 = lean_alloc_ctor(1, 2, 0); +} else { + x_179 = x_178; +} +lean_ctor_set(x_179, 0, x_176); +lean_ctor_set(x_179, 1, x_177); +return x_179; +} +} +else +{ +lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; +x_180 = l_Lean_Syntax_getId(x_170); +lean_dec(x_170); +x_181 = l_Lean_LocalDecl_fvarId(x_161); +lean_dec(x_161); +x_182 = l_Lean_LocalContext_setUserName(x_152, x_181, x_180); +x_183 = 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_184 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(x_162, x_151, x_182, x_153, x_183, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_184) == 0) +{ +lean_object* x_185; lean_object* x_186; +x_185 = lean_ctor_get(x_184, 0); +lean_inc(x_185); +x_186 = lean_ctor_get(x_184, 1); +lean_inc(x_186); +lean_dec(x_184); +x_21 = x_185; +x_22 = x_186; +goto block_29; +} +else +{ +lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; +lean_dec(x_20); +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); +lean_dec(x_4); +x_187 = lean_ctor_get(x_184, 0); +lean_inc(x_187); +x_188 = lean_ctor_get(x_184, 1); +lean_inc(x_188); +if (lean_is_exclusive(x_184)) { + lean_ctor_release(x_184, 0); + lean_ctor_release(x_184, 1); + x_189 = x_184; +} else { + lean_dec_ref(x_184); + x_189 = lean_box(0); +} +if (lean_is_scalar(x_189)) { + x_190 = lean_alloc_ctor(1, 2, 0); +} else { + x_190 = x_189; +} +lean_ctor_set(x_190, 0, x_187); +lean_ctor_set(x_190, 1, x_188); +return x_190; +} +} +} +} +else +{ +lean_object* x_191; uint8_t x_192; +lean_dec(x_163); +x_191 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_153); +x_192 = l_Lean_Syntax_isIdent(x_191); +if (x_192 == 0) +{ +lean_object* x_193; lean_object* x_194; +lean_dec(x_191); +lean_dec(x_161); +x_193 = 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_194 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(x_162, x_151, x_152, x_153, x_193, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_194) == 0) +{ +lean_object* x_195; lean_object* x_196; +x_195 = lean_ctor_get(x_194, 0); +lean_inc(x_195); +x_196 = lean_ctor_get(x_194, 1); +lean_inc(x_196); +lean_dec(x_194); +x_21 = x_195; +x_22 = x_196; +goto block_29; +} +else +{ +lean_object* x_197; lean_object* x_198; lean_object* x_199; lean_object* x_200; +lean_dec(x_20); +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); +lean_dec(x_4); +x_197 = lean_ctor_get(x_194, 0); +lean_inc(x_197); +x_198 = lean_ctor_get(x_194, 1); +lean_inc(x_198); +if (lean_is_exclusive(x_194)) { + lean_ctor_release(x_194, 0); + lean_ctor_release(x_194, 1); + x_199 = x_194; +} else { + lean_dec_ref(x_194); + x_199 = lean_box(0); +} +if (lean_is_scalar(x_199)) { + x_200 = lean_alloc_ctor(1, 2, 0); +} else { + x_200 = x_199; +} +lean_ctor_set(x_200, 0, x_197); +lean_ctor_set(x_200, 1, x_198); +return x_200; +} +} +else +{ +lean_object* x_201; lean_object* x_202; lean_object* x_203; lean_object* x_204; lean_object* x_205; +x_201 = l_Lean_Syntax_getId(x_191); +lean_dec(x_191); +x_202 = l_Lean_LocalDecl_fvarId(x_161); +lean_dec(x_161); +x_203 = l_Lean_LocalContext_setUserName(x_152, x_202, x_201); +x_204 = 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_205 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(x_162, x_151, x_203, x_153, x_204, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_205) == 0) +{ +lean_object* x_206; lean_object* x_207; +x_206 = lean_ctor_get(x_205, 0); +lean_inc(x_206); +x_207 = lean_ctor_get(x_205, 1); +lean_inc(x_207); +lean_dec(x_205); +x_21 = x_206; +x_22 = x_207; +goto block_29; +} +else +{ +lean_object* x_208; lean_object* x_209; lean_object* x_210; lean_object* x_211; +lean_dec(x_20); +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); +lean_dec(x_4); +x_208 = lean_ctor_get(x_205, 0); +lean_inc(x_208); +x_209 = lean_ctor_get(x_205, 1); +lean_inc(x_209); +if (lean_is_exclusive(x_205)) { + lean_ctor_release(x_205, 0); + lean_ctor_release(x_205, 1); + x_210 = x_205; +} else { + lean_dec_ref(x_205); + x_210 = lean_box(0); +} +if (lean_is_scalar(x_210)) { + x_211 = lean_alloc_ctor(1, 2, 0); +} else { + x_211 = x_210; +} +lean_ctor_set(x_211, 0, x_208); +lean_ctor_set(x_211, 1, x_209); +return x_211; +} +} +} +} +} +block_29: +{ +if (lean_obj_tag(x_21) == 0) +{ +lean_object* x_23; lean_object* x_24; +lean_dec(x_20); +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); +lean_dec(x_4); +x_23 = lean_ctor_get(x_21, 0); +lean_inc(x_23); +lean_dec(x_21); +x_24 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_24, 0, x_23); +lean_ctor_set(x_24, 1, x_22); +return x_24; +} +else +{ +lean_object* x_25; lean_object* x_26; lean_object* x_27; +x_25 = lean_ctor_get(x_21, 0); +lean_inc(x_25); +lean_dec(x_21); +x_26 = lean_ctor_get(x_2, 2); +x_27 = lean_nat_add(x_4, x_26); lean_dec(x_4); x_3 = x_20; -x_4 = x_126; -x_5 = x_124; -x_14 = x_123; +x_4 = x_27; +x_5 = x_25; +x_14 = x_22; goto _start; } } -else -{ -lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; -lean_dec(x_20); -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); -lean_dec(x_4); -x_128 = lean_ctor_get(x_117, 0); -lean_inc(x_128); -x_129 = lean_ctor_get(x_117, 1); -lean_inc(x_129); -if (lean_is_exclusive(x_117)) { - lean_ctor_release(x_117, 0); - lean_ctor_release(x_117, 1); - x_130 = x_117; -} else { - lean_dec_ref(x_117); - x_130 = lean_box(0); -} -if (lean_is_scalar(x_130)) { - x_131 = lean_alloc_ctor(1, 2, 0); -} else { - x_131 = x_130; -} -lean_ctor_set(x_131, 0, x_128); -lean_ctor_set(x_131, 1, x_129); -return x_131; -} -} -} -} -} } else { -lean_object* x_132; +lean_object* x_212; lean_dec(x_13); lean_dec(x_12); lean_dec(x_11); @@ -14245,15 +14748,15 @@ lean_dec(x_7); lean_dec(x_6); lean_dec(x_4); lean_dec(x_3); -x_132 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_132, 0, x_5); -lean_ctor_set(x_132, 1, x_14); -return x_132; +x_212 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_212, 0, x_5); +lean_ctor_set(x_212, 1, x_14); +return x_212; } } else { -lean_object* x_133; +lean_object* x_213; lean_dec(x_13); lean_dec(x_12); lean_dec(x_11); @@ -14264,10 +14767,10 @@ lean_dec(x_7); lean_dec(x_6); lean_dec(x_4); lean_dec(x_3); -x_133 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_133, 0, x_5); -lean_ctor_set(x_133, 1, x_14); -return x_133; +x_213 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_213, 0, x_5); +lean_ctor_set(x_213, 1, x_14); +return x_213; } } } @@ -14347,7 +14850,7 @@ lean_inc(x_1); x_13 = l_Lean_Meta_getMVarDecl(x_1, x_7, x_8, x_9, x_10, x_11); if (lean_obj_tag(x_13) == 0) { -lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; +lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; x_14 = lean_ctor_get(x_13, 0); lean_inc(x_14); x_15 = lean_ctor_get(x_13, 1); @@ -14367,6 +14870,10 @@ lean_ctor_set(x_20, 2, x_19); x_21 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_21, 0, x_16); lean_ctor_set(x_21, 1, x_2); +x_22 = l_Lean_NameSet_empty; +x_23 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_23, 0, x_22); +lean_ctor_set(x_23, 1, x_21); lean_inc(x_10); lean_inc(x_9); lean_inc(x_8); @@ -14376,29 +14883,32 @@ lean_inc(x_5); lean_inc(x_4); lean_inc(x_3); lean_inc(x_17); -x_22 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1(x_17, x_20, x_17, x_18, x_21, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_15); +x_24 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1(x_17, x_20, x_17, x_18, x_23, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_15); lean_dec(x_20); lean_dec(x_17); -if (lean_obj_tag(x_22) == 0) +if (lean_obj_tag(x_24) == 0) { -lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27; -x_23 = lean_ctor_get(x_22, 0); -lean_inc(x_23); -x_24 = lean_ctor_get(x_22, 1); -lean_inc(x_24); -lean_dec(x_22); -x_25 = lean_ctor_get(x_23, 0); +lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; uint8_t x_30; +x_25 = lean_ctor_get(x_24, 0); lean_inc(x_25); -x_26 = lean_ctor_get(x_23, 1); +x_26 = lean_ctor_get(x_25, 1); lean_inc(x_26); -lean_dec(x_23); -x_27 = l_Array_isEmpty___rarg(x_26); +lean_dec(x_25); +x_27 = lean_ctor_get(x_24, 1); +lean_inc(x_27); +lean_dec(x_24); +x_28 = lean_ctor_get(x_26, 0); +lean_inc(x_28); +x_29 = lean_ctor_get(x_26, 1); +lean_inc(x_29); lean_dec(x_26); -if (x_27 == 0) +x_30 = l_Array_isEmpty___rarg(x_29); +lean_dec(x_29); +if (x_30 == 0) { -lean_object* x_28; uint8_t x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; -x_28 = l_Lean_Elab_Tactic_renameInaccessibles___closed__2; -x_29 = 2; +lean_object* x_31; uint8_t x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; +x_31 = l_Lean_Elab_Tactic_renameInaccessibles___closed__2; +x_32 = 2; lean_inc(x_10); lean_inc(x_9); lean_inc(x_8); @@ -14407,13 +14917,13 @@ lean_inc(x_6); lean_inc(x_5); lean_inc(x_4); lean_inc(x_3); -x_30 = l_Lean_Elab_log___at_Lean_Elab_Tactic_closeUsingOrAdmit___spec__3(x_28, x_29, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_24); -x_31 = lean_ctor_get(x_30, 0); -lean_inc(x_31); -x_32 = lean_ctor_get(x_30, 1); -lean_inc(x_32); -lean_dec(x_30); -x_33 = l_Lean_Elab_Tactic_renameInaccessibles___lambda__1(x_14, x_25, x_1, x_31, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_32); +x_33 = l_Lean_Elab_log___at_Lean_Elab_Tactic_closeUsingOrAdmit___spec__3(x_31, x_32, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_27); +x_34 = lean_ctor_get(x_33, 0); +lean_inc(x_34); +x_35 = lean_ctor_get(x_33, 1); +lean_inc(x_35); +lean_dec(x_33); +x_36 = l_Lean_Elab_Tactic_renameInaccessibles___lambda__1(x_14, x_28, x_1, x_34, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_35); lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); @@ -14422,14 +14932,14 @@ lean_dec(x_6); lean_dec(x_5); lean_dec(x_4); lean_dec(x_3); -lean_dec(x_31); -return x_33; +lean_dec(x_34); +return x_36; } else { -lean_object* x_34; lean_object* x_35; -x_34 = lean_box(0); -x_35 = l_Lean_Elab_Tactic_renameInaccessibles___lambda__1(x_14, x_25, x_1, x_34, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_24); +lean_object* x_37; lean_object* x_38; +x_37 = lean_box(0); +x_38 = l_Lean_Elab_Tactic_renameInaccessibles___lambda__1(x_14, x_28, x_1, x_37, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_27); lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); @@ -14438,12 +14948,12 @@ lean_dec(x_6); lean_dec(x_5); lean_dec(x_4); lean_dec(x_3); -return x_35; +return x_38; } } else { -uint8_t x_36; +uint8_t x_39; lean_dec(x_14); lean_dec(x_10); lean_dec(x_9); @@ -14454,29 +14964,29 @@ lean_dec(x_5); lean_dec(x_4); lean_dec(x_3); lean_dec(x_1); -x_36 = !lean_is_exclusive(x_22); -if (x_36 == 0) +x_39 = !lean_is_exclusive(x_24); +if (x_39 == 0) { -return x_22; +return x_24; } else { -lean_object* x_37; lean_object* x_38; lean_object* x_39; -x_37 = lean_ctor_get(x_22, 0); -x_38 = lean_ctor_get(x_22, 1); -lean_inc(x_38); -lean_inc(x_37); -lean_dec(x_22); -x_39 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_39, 0, x_37); -lean_ctor_set(x_39, 1, x_38); -return x_39; +lean_object* x_40; lean_object* x_41; lean_object* x_42; +x_40 = lean_ctor_get(x_24, 0); +x_41 = lean_ctor_get(x_24, 1); +lean_inc(x_41); +lean_inc(x_40); +lean_dec(x_24); +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; } } } else { -uint8_t x_40; +uint8_t x_43; lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); @@ -14487,29 +14997,29 @@ lean_dec(x_4); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_40 = !lean_is_exclusive(x_13); -if (x_40 == 0) +x_43 = !lean_is_exclusive(x_13); +if (x_43 == 0) { return x_13; } else { -lean_object* x_41; lean_object* x_42; lean_object* x_43; -x_41 = lean_ctor_get(x_13, 0); -x_42 = lean_ctor_get(x_13, 1); -lean_inc(x_42); -lean_inc(x_41); +lean_object* x_44; lean_object* x_45; lean_object* x_46; +x_44 = lean_ctor_get(x_13, 0); +x_45 = lean_ctor_get(x_13, 1); +lean_inc(x_45); +lean_inc(x_44); lean_dec(x_13); -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; +x_46 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_46, 0, x_44); +lean_ctor_set(x_46, 1, x_45); +return x_46; } } } else { -lean_object* x_44; +lean_object* x_47; lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); @@ -14519,18 +15029,20 @@ lean_dec(x_5); lean_dec(x_4); lean_dec(x_3); lean_dec(x_2); -x_44 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_44, 0, x_1); -lean_ctor_set(x_44, 1, x_11); -return x_44; +x_47 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_47, 0, x_1); +lean_ctor_set(x_47, 1, x_11); +return x_47; } } } -lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___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* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___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) { _start: { -lean_object* x_13; -x_13 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); +lean_object* x_15; +x_15 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__1(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); +lean_dec(x_13); +lean_dec(x_12); lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); @@ -14538,9 +15050,17 @@ lean_dec(x_8); lean_dec(x_7); lean_dec(x_6); lean_dec(x_5); -lean_dec(x_4); -lean_dec(x_3); -return x_13; +lean_dec(x_1); +return x_15; +} +} +lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2___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) { +_start: +{ +lean_object* x_15; +x_15 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(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); +lean_dec(x_5); +return x_15; } } lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__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) { @@ -16290,8 +16810,6 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalSubst___closed__3); res = l___regBuiltin_Lean_Elab_Tactic_evalSubst(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___closed__1 = _init_l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___closed__1(); -lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___closed__1); l_Lean_Elab_Tactic_renameInaccessibles___closed__1 = _init_l_Lean_Elab_Tactic_renameInaccessibles___closed__1(); lean_mark_persistent(l_Lean_Elab_Tactic_renameInaccessibles___closed__1); l_Lean_Elab_Tactic_renameInaccessibles___closed__2 = _init_l_Lean_Elab_Tactic_renameInaccessibles___closed__2(); diff --git a/stage0/stdlib/Lean/Expr.c b/stage0/stdlib/Lean/Expr.c index 3bcb7a07de..b1dd5d3780 100644 --- a/stage0/stdlib/Lean/Expr.c +++ b/stage0/stdlib/Lean/Expr.c @@ -123,6 +123,7 @@ lean_object* l_Lean_mkLHSGoal(lean_object*); static lean_object* l_Lean_mkDecIsTrue___closed__5; lean_object* l_Lean_instFVarIdSetEmptyCollection; lean_object* l_Lean_mkMVar(lean_object*); +lean_object* l_Lean_Expr_consumeAutoOptParam(lean_object*); size_t l_USize_sub(size_t, size_t); lean_object* l___private_Lean_Expr_0__Lean_Expr_etaExpandedAux(lean_object*, lean_object*); lean_object* l_Lean_Expr_hash___boxed(lean_object*); @@ -9776,6 +9777,42 @@ x_3 = lean_box(x_2); return x_3; } } +lean_object* l_Lean_Expr_consumeAutoOptParam(lean_object* x_1) { +_start: +{ +uint8_t x_2; +x_2 = l_Lean_Expr_isOptParam(x_1); +if (x_2 == 0) +{ +uint8_t x_3; +x_3 = l_Lean_Expr_isAutoParam(x_1); +if (x_3 == 0) +{ +return x_1; +} +else +{ +lean_object* x_4; lean_object* x_5; +x_4 = l_Lean_Expr_appFn_x21(x_1); +lean_dec(x_1); +x_5 = l_Lean_Expr_appArg_x21(x_4); +lean_dec(x_4); +x_1 = x_5; +goto _start; +} +} +else +{ +lean_object* x_7; lean_object* x_8; +x_7 = l_Lean_Expr_appFn_x21(x_1); +lean_dec(x_1); +x_8 = l_Lean_Expr_appArg_x21(x_7); +lean_dec(x_7); +x_1 = x_8; +goto _start; +} +} +} lean_object* l_Lean_Expr_hasAnyFVar_visit(lean_object* x_1, lean_object* x_2) { _start: { @@ -10150,7 +10187,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2; x_2 = l_Lean_Expr_updateApp_x21___closed__1; -x_3 = lean_unsigned_to_nat(908u); +x_3 = lean_unsigned_to_nat(914u); x_4 = lean_unsigned_to_nat(20u); x_5 = l_Lean_Expr_appFn_x21___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10222,7 +10259,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2; x_2 = l_Lean_Expr_updateConst_x21___closed__1; -x_3 = lean_unsigned_to_nat(917u); +x_3 = lean_unsigned_to_nat(923u); x_4 = lean_unsigned_to_nat(20u); x_5 = l_Lean_Expr_constName_x21___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10301,7 +10338,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2; x_2 = l_Lean_Expr_updateSort_x21___closed__1; -x_3 = lean_unsigned_to_nat(926u); +x_3 = lean_unsigned_to_nat(932u); x_4 = lean_unsigned_to_nat(16u); x_5 = l_Lean_Expr_updateSort_x21___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10385,7 +10422,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2; x_2 = l_Lean_Expr_updateMData_x21___closed__1; -x_3 = lean_unsigned_to_nat(943u); +x_3 = lean_unsigned_to_nat(949u); x_4 = lean_unsigned_to_nat(19u); x_5 = l_Lean_Expr_updateMData_x21___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10456,7 +10493,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2; x_2 = l_Lean_Expr_updateProj_x21___closed__1; -x_3 = lean_unsigned_to_nat(948u); +x_3 = lean_unsigned_to_nat(954u); x_4 = lean_unsigned_to_nat(20u); x_5 = l_Lean_Expr_updateProj_x21___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10540,7 +10577,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2; x_2 = l_Lean_Expr_updateForall_x21___closed__1; -x_3 = lean_unsigned_to_nat(957u); +x_3 = lean_unsigned_to_nat(963u); x_4 = lean_unsigned_to_nat(23u); x_5 = l_Lean_Expr_updateForall_x21___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10617,7 +10654,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2; x_2 = l_Lean_Expr_updateForallE_x21___closed__1; -x_3 = lean_unsigned_to_nat(962u); +x_3 = lean_unsigned_to_nat(968u); x_4 = lean_unsigned_to_nat(23u); x_5 = l_Lean_Expr_updateForall_x21___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10705,7 +10742,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2; x_2 = l_Lean_Expr_updateLambda_x21___closed__1; -x_3 = lean_unsigned_to_nat(971u); +x_3 = lean_unsigned_to_nat(977u); x_4 = lean_unsigned_to_nat(19u); x_5 = l_Lean_Expr_updateLambda_x21___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10782,7 +10819,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2; x_2 = l_Lean_Expr_updateLambdaE_x21___closed__1; -x_3 = lean_unsigned_to_nat(976u); +x_3 = lean_unsigned_to_nat(982u); x_4 = lean_unsigned_to_nat(19u); x_5 = l_Lean_Expr_updateLambda_x21___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10860,7 +10897,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2; x_2 = l_Lean_Expr_updateLet_x21___closed__1; -x_3 = lean_unsigned_to_nat(985u); +x_3 = lean_unsigned_to_nat(991u); x_4 = lean_unsigned_to_nat(22u); x_5 = l_Lean_Expr_letName_x21___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); diff --git a/stage0/stdlib/Lean/Meta.c b/stage0/stdlib/Lean/Meta.c index b05943c7ba..0755cd2729 100644 --- a/stage0/stdlib/Lean/Meta.c +++ b/stage0/stdlib/Lean/Meta.c @@ -1,6 +1,6 @@ // Lean compiler output // Module: Lean.Meta -// Imports: Init Lean.Meta.Basic Lean.Meta.LevelDefEq Lean.Meta.WHNF Lean.Meta.InferType Lean.Meta.FunInfo Lean.Meta.ExprDefEq Lean.Meta.DiscrTree Lean.Meta.Reduce Lean.Meta.Instances Lean.Meta.AbstractMVars Lean.Meta.SynthInstance Lean.Meta.AppBuilder Lean.Meta.Tactic Lean.Meta.KAbstract Lean.Meta.RecursorInfo Lean.Meta.GeneralizeTelescope Lean.Meta.Match Lean.Meta.ReduceEval Lean.Meta.Closure Lean.Meta.AbstractNestedProofs Lean.Meta.ForEachExpr Lean.Meta.Transform Lean.Meta.PPGoal Lean.Meta.UnificationHint Lean.Meta.Inductive Lean.Meta.SizeOf Lean.Meta.IndPredBelow Lean.Meta.Coe Lean.Meta.SortLocalDecls Lean.Meta.CollectFVars Lean.Meta.GeneralizeVars Lean.Meta.Injective Lean.Meta.Structure Lean.Meta.Constructions +// Imports: Init Lean.Meta.Basic Lean.Meta.LevelDefEq Lean.Meta.WHNF Lean.Meta.InferType Lean.Meta.FunInfo Lean.Meta.ExprDefEq Lean.Meta.DiscrTree Lean.Meta.Reduce Lean.Meta.Instances Lean.Meta.AbstractMVars Lean.Meta.SynthInstance Lean.Meta.AppBuilder Lean.Meta.Tactic Lean.Meta.KAbstract Lean.Meta.RecursorInfo Lean.Meta.GeneralizeTelescope Lean.Meta.Match Lean.Meta.ReduceEval Lean.Meta.Closure Lean.Meta.AbstractNestedProofs Lean.Meta.ForEachExpr Lean.Meta.Transform Lean.Meta.PPGoal Lean.Meta.UnificationHint Lean.Meta.Inductive Lean.Meta.SizeOf Lean.Meta.IndPredBelow Lean.Meta.Coe Lean.Meta.SortLocalDecls Lean.Meta.CollectFVars Lean.Meta.GeneralizeVars Lean.Meta.Injective Lean.Meta.Structure Lean.Meta.Constructions Lean.Meta.CongrTheorems #include #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -48,6 +48,7 @@ lean_object* initialize_Lean_Meta_GeneralizeVars(lean_object*); lean_object* initialize_Lean_Meta_Injective(lean_object*); lean_object* initialize_Lean_Meta_Structure(lean_object*); lean_object* initialize_Lean_Meta_Constructions(lean_object*); +lean_object* initialize_Lean_Meta_CongrTheorems(lean_object*); static bool _G_initialized = false; lean_object* initialize_Lean_Meta(lean_object* w) { lean_object * res; @@ -158,6 +159,9 @@ lean_dec_ref(res); res = initialize_Lean_Meta_Constructions(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +res = initialize_Lean_Meta_CongrTheorems(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); return lean_io_result_mk_ok(lean_box(0)); } #ifdef __cplusplus diff --git a/stage0/stdlib/Lean/Meta/Closure.c b/stage0/stdlib/Lean/Meta/Closure.c index b6d86d88c5..720de56fe9 100644 --- a/stage0/stdlib/Lean/Meta/Closure.c +++ b/stage0/stdlib/Lean/Meta/Closure.c @@ -3678,7 +3678,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_Closure_collectExprAux___closed__1; x_2 = l_Lean_Meta_Closure_collectExprAux___closed__2; -x_3 = lean_unsigned_to_nat(943u); +x_3 = lean_unsigned_to_nat(949u); x_4 = lean_unsigned_to_nat(19u); x_5 = l_Lean_Meta_Closure_collectExprAux___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -3707,7 +3707,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_Closure_collectExprAux___closed__1; x_2 = l_Lean_Meta_Closure_collectExprAux___closed__5; -x_3 = lean_unsigned_to_nat(948u); +x_3 = lean_unsigned_to_nat(954u); x_4 = lean_unsigned_to_nat(20u); x_5 = l_Lean_Meta_Closure_collectExprAux___closed__6; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -3736,7 +3736,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_Closure_collectExprAux___closed__1; x_2 = l_Lean_Meta_Closure_collectExprAux___closed__8; -x_3 = lean_unsigned_to_nat(908u); +x_3 = lean_unsigned_to_nat(914u); x_4 = lean_unsigned_to_nat(20u); x_5 = l_Lean_Meta_Closure_collectExprAux___closed__9; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -3765,7 +3765,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_Closure_collectExprAux___closed__1; x_2 = l_Lean_Meta_Closure_collectExprAux___closed__11; -x_3 = lean_unsigned_to_nat(976u); +x_3 = lean_unsigned_to_nat(982u); x_4 = lean_unsigned_to_nat(19u); x_5 = l_Lean_Meta_Closure_collectExprAux___closed__12; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -3794,7 +3794,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_Closure_collectExprAux___closed__1; x_2 = l_Lean_Meta_Closure_collectExprAux___closed__14; -x_3 = lean_unsigned_to_nat(962u); +x_3 = lean_unsigned_to_nat(968u); x_4 = lean_unsigned_to_nat(23u); x_5 = l_Lean_Meta_Closure_collectExprAux___closed__15; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -3823,7 +3823,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_Closure_collectExprAux___closed__1; x_2 = l_Lean_Meta_Closure_collectExprAux___closed__17; -x_3 = lean_unsigned_to_nat(985u); +x_3 = lean_unsigned_to_nat(991u); x_4 = lean_unsigned_to_nat(22u); x_5 = l_Lean_Meta_Closure_collectExprAux___closed__18; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); diff --git a/stage0/stdlib/Lean/Meta/CongrTheorems.c b/stage0/stdlib/Lean/Meta/CongrTheorems.c new file mode 100644 index 0000000000..5fe0a7fc0d --- /dev/null +++ b/stage0/stdlib/Lean/Meta/CongrTheorems.c @@ -0,0 +1,2279 @@ +// Lean compiler output +// Module: Lean.Meta.CongrTheorems +// Imports: Init Lean.Meta.AppBuilder +#include +#if defined(__clang__) +#pragma clang diagnostic ignored "-Wunused-parameter" +#pragma clang diagnostic ignored "-Wunused-label" +#elif defined(__GNUC__) && !defined(__CLANG__) +#pragma GCC diagnostic ignored "-Wunused-parameter" +#pragma GCC diagnostic ignored "-Wunused-label" +#pragma GCC diagnostic ignored "-Wunused-but-set-variable" +#endif +#ifdef __cplusplus +extern "C" { +#endif +lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___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_CongrArgKind_noConfusion___rarg(uint8_t, uint8_t, lean_object*); +size_t l_USize_add(size_t, size_t); +lean_object* l_Lean_stringToMessageData(lean_object*); +lean_object* lean_mk_empty_array_with_capacity(lean_object*); +lean_object* l_Lean_Meta_mkForallFVars(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_LocalDecl_userName(lean_object*); +lean_object* lean_name_mk_string(lean_object*, lean_object*); +lean_object* lean_array_uget(lean_object*, size_t); +lean_object* l_Lean_Expr_bindingDomain_x21(lean_object*); +lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkHCongrWithArity___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalDeclImp___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Expr_consumeAutoOptParam(lean_object*); +lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1(lean_object*); +static lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___closed__1; +lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Expr_appFn_x21(lean_object*); +static lean_object* l_Lean_Meta_mkHCongrWithArity___lambda__3___closed__2; +lean_object* lean_expr_instantiate1(lean_object*, lean_object*); +lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*); +lean_object* lean_array_push(lean_object*, lean_object*); +lean_object* lean_array_get_size(lean_object*); +lean_object* l_Lean_Meta_getFunInfo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___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* l_Lean_Expr_appArg_x21(lean_object*); +uint8_t l_USize_decLt(size_t, size_t); +lean_object* l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_setBinderInfosD(lean_object*, lean_object*); +lean_object* lean_nat_add(lean_object*, lean_object*); +lean_object* l_Lean_Meta_CongrArgKind_toCtorIdx___boxed(lean_object*); +lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___spec__1(lean_object*, size_t, size_t, lean_object*); +lean_object* l_Lean_Meta_mkEqRefl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_withLCtx___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_mkLeveErrorMessageCore___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_throwError___at_Lean_Meta_mkHCongrWithArity___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_LocalContext_setBinderInfo(lean_object*, lean_object*, uint8_t); +lean_object* l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___boxed(lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__2(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_Meta_mkHCongrWithArity_mkProof___closed__2; +uint8_t l_Lean_Expr_isHEq(lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg(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_fget(lean_object*, lean_object*); +uint8_t lean_nat_dec_eq(lean_object*, lean_object*); +static lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___closed__6; +lean_object* l_Lean_Meta_mkHCongrWithArity___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames(lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop(lean_object*); +static lean_object* l_Lean_Meta_mkHCongrWithArity___lambda__3___closed__1; +lean_object* lean_array_get(lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs___rarg___closed__1; +lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* lean_name_append_index_after(lean_object*, lean_object*); +lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_setBinderInfosD___spec__1(lean_object*, size_t, size_t, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_CongrArgKind_toCtorIdx(uint8_t); +lean_object* l_Lean_LocalContext_getFVar_x21(lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkEqNDRec(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_CongrArgKind_noConfusion___rarg___boxed(lean_object*, lean_object*, lean_object*); +uint8_t l_Lean_Expr_isAppOfArity(lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_instInhabitedExpr; +static lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___closed__4; +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_getLocalInstances(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_setBinderInfosD___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_CongrArgKind_noConfusion___rarg___closed__1; +lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +size_t lean_usize_of_nat(lean_object*); +lean_object* l_Lean_LocalDecl_fvarId(lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkHCongrWithArity___spec__2___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_mkHCongrWithArity_mkProof___lambda__1___closed__1; +lean_object* l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_setBinderInfosD___boxed(lean_object*, lean_object*); +lean_object* lean_name_append_after(lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Expr_bindingName_x21(lean_object*); +uint8_t lean_expr_eqv(lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_CongrArgKind_noConfusion___rarg___lambda__1(lean_object*); +static lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___closed__3; +lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Meta_addPPExplicitToExposeDiff_visit___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___closed__5; +lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___spec__1___closed__1; +lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_CongrArgKind_noConfusion___rarg___lambda__1___boxed(lean_object*); +lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_FunInfo_getArity(lean_object*); +lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1___closed__2; +lean_object* l_Lean_throwError___at_Lean_Meta_mkHCongrWithArity___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs(lean_object*); +lean_object* l_Lean_LocalContext_setUserName(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___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* l_Lean_Meta_mkHEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity___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* l_Lean_Meta_mkHEqRefl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___closed__2; +static lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___closed__1; +lean_object* l_Lean_Expr_bindingBody_x21(lean_object*); +lean_object* l_Lean_Meta_mkEqOfHEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___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_CongrArgKind_noConfusion(lean_object*); +uint8_t lean_nat_dec_lt(lean_object*, lean_object*); +lean_object* l_Lean_Meta_CongrArgKind_toCtorIdx(uint8_t x_1) { +_start: +{ +switch (x_1) { +case 0: +{ +lean_object* x_2; +x_2 = lean_unsigned_to_nat(0u); +return x_2; +} +case 1: +{ +lean_object* x_3; +x_3 = lean_unsigned_to_nat(1u); +return x_3; +} +case 2: +{ +lean_object* x_4; +x_4 = lean_unsigned_to_nat(2u); +return x_4; +} +case 3: +{ +lean_object* x_5; +x_5 = lean_unsigned_to_nat(3u); +return x_5; +} +default: +{ +lean_object* x_6; +x_6 = lean_unsigned_to_nat(4u); +return x_6; +} +} +} +} +lean_object* l_Lean_Meta_CongrArgKind_toCtorIdx___boxed(lean_object* x_1) { +_start: +{ +uint8_t x_2; lean_object* x_3; +x_2 = lean_unbox(x_1); +lean_dec(x_1); +x_3 = l_Lean_Meta_CongrArgKind_toCtorIdx(x_2); +return x_3; +} +} +lean_object* l_Lean_Meta_CongrArgKind_noConfusion___rarg___lambda__1(lean_object* x_1) { +_start: +{ +lean_inc(x_1); +return x_1; +} +} +static lean_object* _init_l_Lean_Meta_CongrArgKind_noConfusion___rarg___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Meta_CongrArgKind_noConfusion___rarg___lambda__1___boxed), 1, 0); +return x_1; +} +} +lean_object* l_Lean_Meta_CongrArgKind_noConfusion___rarg(uint8_t x_1, uint8_t x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l_Lean_Meta_CongrArgKind_noConfusion___rarg___closed__1; +return x_4; +} +} +lean_object* l_Lean_Meta_CongrArgKind_noConfusion(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_Lean_Meta_CongrArgKind_noConfusion___rarg___boxed), 3, 0); +return x_2; +} +} +lean_object* l_Lean_Meta_CongrArgKind_noConfusion___rarg___lambda__1___boxed(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = l_Lean_Meta_CongrArgKind_noConfusion___rarg___lambda__1(x_1); +lean_dec(x_1); +return x_2; +} +} +lean_object* l_Lean_Meta_CongrArgKind_noConfusion___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; uint8_t x_5; lean_object* x_6; +x_4 = lean_unbox(x_1); +lean_dec(x_1); +x_5 = lean_unbox(x_2); +lean_dec(x_2); +x_6 = l_Lean_Meta_CongrArgKind_noConfusion___rarg(x_4, x_5, x_3); +return x_6; +} +} +static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___spec__1___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("'"); +return x_1; +} +} +lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) { +_start: +{ +uint8_t x_5; +x_5 = x_3 < x_2; +if (x_5 == 0) +{ +return x_4; +} +else +{ +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; size_t x_13; size_t x_14; +x_6 = lean_array_uget(x_1, x_3); +lean_inc(x_4); +x_7 = l_Lean_LocalContext_getFVar_x21(x_4, x_6); +lean_dec(x_6); +x_8 = l_Lean_LocalDecl_fvarId(x_7); +x_9 = l_Lean_LocalDecl_userName(x_7); +lean_dec(x_7); +x_10 = l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___spec__1___closed__1; +x_11 = lean_name_append_after(x_9, x_10); +x_12 = l_Lean_LocalContext_setUserName(x_4, x_8, x_11); +x_13 = 1; +x_14 = x_3 + x_13; +x_3 = x_14; +x_4 = x_12; +goto _start; +} +} +} +lean_object* l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; size_t x_4; size_t x_5; lean_object* x_6; +x_3 = lean_array_get_size(x_1); +x_4 = lean_usize_of_nat(x_3); +lean_dec(x_3); +x_5 = 0; +x_6 = l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___spec__1(x_1, x_4, x_5, x_2); +return x_6; +} +} +lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +size_t x_5; size_t x_6; lean_object* x_7; +x_5 = lean_unbox_usize(x_2); +lean_dec(x_2); +x_6 = lean_unbox_usize(x_3); +lean_dec(x_3); +x_7 = l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___spec__1(x_1, x_5, x_6, x_4); +lean_dec(x_1); +return x_7; +} +} +lean_object* l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames(x_1, x_2); +lean_dec(x_1); +return x_3; +} +} +lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_setBinderInfosD___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) { +_start: +{ +uint8_t x_5; +x_5 = x_3 < x_2; +if (x_5 == 0) +{ +return x_4; +} +else +{ +lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; lean_object* x_10; size_t x_11; size_t x_12; +x_6 = lean_array_uget(x_1, x_3); +lean_inc(x_4); +x_7 = l_Lean_LocalContext_getFVar_x21(x_4, x_6); +lean_dec(x_6); +x_8 = l_Lean_LocalDecl_fvarId(x_7); +lean_dec(x_7); +x_9 = 0; +x_10 = l_Lean_LocalContext_setBinderInfo(x_4, x_8, x_9); +x_11 = 1; +x_12 = x_3 + x_11; +x_3 = x_12; +x_4 = x_10; +goto _start; +} +} +} +lean_object* l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_setBinderInfosD(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; size_t x_4; size_t x_5; lean_object* x_6; +x_3 = lean_array_get_size(x_1); +x_4 = lean_usize_of_nat(x_3); +lean_dec(x_3); +x_5 = 0; +x_6 = l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_setBinderInfosD___spec__1(x_1, x_4, x_5, x_2); +return x_6; +} +} +lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_setBinderInfosD___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +size_t x_5; size_t x_6; lean_object* x_7; +x_5 = lean_unbox_usize(x_2); +lean_dec(x_2); +x_6 = lean_unbox_usize(x_3); +lean_dec(x_3); +x_7 = l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_setBinderInfosD___spec__1(x_1, x_5, x_6, x_4); +lean_dec(x_1); +return x_7; +} +} +lean_object* l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_setBinderInfosD___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_setBinderInfosD(x_1, x_2); +lean_dec(x_1); +return x_3; +} +} +lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1___rarg(lean_object* x_1, uint8_t 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) { +_start: +{ +lean_object* x_10; +x_10 = l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalDeclImp___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9); +if (lean_obj_tag(x_10) == 0) +{ +uint8_t x_11; +x_11 = !lean_is_exclusive(x_10); +if (x_11 == 0) +{ +return x_10; +} +else +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; +x_12 = lean_ctor_get(x_10, 0); +x_13 = lean_ctor_get(x_10, 1); +lean_inc(x_13); +lean_inc(x_12); +lean_dec(x_10); +x_14 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_14, 0, x_12); +lean_ctor_set(x_14, 1, x_13); +return x_14; +} +} +else +{ +uint8_t x_15; +x_15 = !lean_is_exclusive(x_10); +if (x_15 == 0) +{ +return x_10; +} +else +{ +lean_object* x_16; lean_object* x_17; lean_object* x_18; +x_16 = lean_ctor_get(x_10, 0); +x_17 = lean_ctor_get(x_10, 1); +lean_inc(x_17); +lean_inc(x_16); +lean_dec(x_10); +x_18 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_18, 0, x_16); +lean_ctor_set(x_18, 1, x_17); +return x_18; +} +} +} +} +lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1___rarg___boxed), 9, 0); +return x_2; +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) { +_start: +{ +lean_object* x_13; uint8_t x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; +x_13 = lean_array_push(x_1, x_7); +x_14 = 4; +x_15 = lean_box(x_14); +x_16 = lean_array_push(x_2, x_15); +x_17 = l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg(x_3, x_4, x_5, x_6, x_13, x_16, x_8, x_9, x_10, x_11, x_12); +return x_17; +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___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, lean_object* x_11, lean_object* x_12) { +_start: +{ +lean_object* x_13; uint8_t x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; +x_13 = lean_array_push(x_1, x_7); +x_14 = 2; +x_15 = lean_box(x_14); +x_16 = lean_array_push(x_2, x_15); +x_17 = l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg(x_3, x_4, x_5, x_6, x_13, x_16, x_8, x_9, x_10, x_11, x_12); +return x_17; +} +} +static lean_object* _init_l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("e"); +return x_1; +} +} +static lean_object* _init_l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg(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) { +_start: +{ +lean_object* x_12; uint8_t x_13; +x_12 = lean_array_get_size(x_1); +x_13 = lean_nat_dec_lt(x_4, x_12); +lean_dec(x_12); +if (x_13 == 0) +{ +lean_object* x_14; +lean_dec(x_4); +lean_dec(x_2); +lean_dec(x_1); +x_14 = lean_apply_7(x_3, x_5, x_6, x_7, x_8, x_9, x_10, x_11); +return x_14; +} +else +{ +lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; +x_15 = l_Lean_instInhabitedExpr; +x_16 = lean_array_get(x_15, x_1, x_4); +x_17 = lean_array_get(x_15, x_2, x_4); +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +lean_inc(x_16); +x_18 = lean_infer_type(x_16, x_7, x_8, x_9, x_10, x_11); +if (lean_obj_tag(x_18) == 0) +{ +lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; +x_19 = lean_ctor_get(x_18, 0); +lean_inc(x_19); +x_20 = lean_ctor_get(x_18, 1); +lean_inc(x_20); +lean_dec(x_18); +x_21 = l_Lean_Expr_consumeAutoOptParam(x_19); +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +lean_inc(x_17); +x_22 = lean_infer_type(x_17, x_7, x_8, x_9, x_10, x_20); +if (lean_obj_tag(x_22) == 0) +{ +lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26; +x_23 = lean_ctor_get(x_22, 0); +lean_inc(x_23); +x_24 = lean_ctor_get(x_22, 1); +lean_inc(x_24); +lean_dec(x_22); +x_25 = l_Lean_Expr_consumeAutoOptParam(x_23); +x_26 = lean_expr_eqv(x_21, x_25); +lean_dec(x_25); +lean_dec(x_21); +if (x_26 == 0) +{ +lean_object* x_27; +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +x_27 = l_Lean_Meta_mkHEq(x_16, x_17, x_7, x_8, x_9, x_10, x_24); +if (lean_obj_tag(x_27) == 0) +{ +lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; uint8_t x_35; lean_object* x_36; +x_28 = lean_ctor_get(x_27, 0); +lean_inc(x_28); +x_29 = lean_ctor_get(x_27, 1); +lean_inc(x_29); +lean_dec(x_27); +x_30 = lean_unsigned_to_nat(1u); +x_31 = lean_nat_add(x_4, x_30); +lean_dec(x_4); +x_32 = l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___closed__2; +lean_inc(x_31); +x_33 = lean_name_append_index_after(x_32, x_31); +x_34 = lean_alloc_closure((void*)(l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___lambda__1), 12, 6); +lean_closure_set(x_34, 0, x_5); +lean_closure_set(x_34, 1, x_6); +lean_closure_set(x_34, 2, x_1); +lean_closure_set(x_34, 3, x_2); +lean_closure_set(x_34, 4, x_3); +lean_closure_set(x_34, 5, x_31); +x_35 = 0; +x_36 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1___rarg(x_33, x_35, x_28, x_34, x_7, x_8, x_9, x_10, x_29); +return x_36; +} +else +{ +uint8_t x_37; +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_37 = !lean_is_exclusive(x_27); +if (x_37 == 0) +{ +return x_27; +} +else +{ +lean_object* x_38; lean_object* x_39; lean_object* x_40; +x_38 = lean_ctor_get(x_27, 0); +x_39 = lean_ctor_get(x_27, 1); +lean_inc(x_39); +lean_inc(x_38); +lean_dec(x_27); +x_40 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_40, 0, x_38); +lean_ctor_set(x_40, 1, x_39); +return x_40; +} +} +} +else +{ +lean_object* x_41; +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +x_41 = l_Lean_Meta_mkEq(x_16, x_17, x_7, x_8, x_9, x_10, x_24); +if (lean_obj_tag(x_41) == 0) +{ +lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; uint8_t x_49; lean_object* x_50; +x_42 = lean_ctor_get(x_41, 0); +lean_inc(x_42); +x_43 = lean_ctor_get(x_41, 1); +lean_inc(x_43); +lean_dec(x_41); +x_44 = lean_unsigned_to_nat(1u); +x_45 = lean_nat_add(x_4, x_44); +lean_dec(x_4); +x_46 = l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___closed__2; +lean_inc(x_45); +x_47 = lean_name_append_index_after(x_46, x_45); +x_48 = lean_alloc_closure((void*)(l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___lambda__2), 12, 6); +lean_closure_set(x_48, 0, x_5); +lean_closure_set(x_48, 1, x_6); +lean_closure_set(x_48, 2, x_1); +lean_closure_set(x_48, 3, x_2); +lean_closure_set(x_48, 4, x_3); +lean_closure_set(x_48, 5, x_45); +x_49 = 0; +x_50 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1___rarg(x_47, x_49, x_42, x_48, x_7, x_8, x_9, x_10, x_43); +return x_50; +} +else +{ +uint8_t x_51; +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_51 = !lean_is_exclusive(x_41); +if (x_51 == 0) +{ +return x_41; +} +else +{ +lean_object* x_52; lean_object* x_53; lean_object* x_54; +x_52 = lean_ctor_get(x_41, 0); +x_53 = lean_ctor_get(x_41, 1); +lean_inc(x_53); +lean_inc(x_52); +lean_dec(x_41); +x_54 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_54, 0, x_52); +lean_ctor_set(x_54, 1, x_53); +return x_54; +} +} +} +} +else +{ +uint8_t x_55; +lean_dec(x_21); +lean_dec(x_17); +lean_dec(x_16); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_55 = !lean_is_exclusive(x_22); +if (x_55 == 0) +{ +return x_22; +} +else +{ +lean_object* x_56; lean_object* x_57; lean_object* x_58; +x_56 = lean_ctor_get(x_22, 0); +x_57 = lean_ctor_get(x_22, 1); +lean_inc(x_57); +lean_inc(x_56); +lean_dec(x_22); +x_58 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_58, 0, x_56); +lean_ctor_set(x_58, 1, x_57); +return x_58; +} +} +} +else +{ +uint8_t x_59; +lean_dec(x_17); +lean_dec(x_16); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_59 = !lean_is_exclusive(x_18); +if (x_59 == 0) +{ +return x_18; +} +else +{ +lean_object* x_60; lean_object* x_61; lean_object* x_62; +x_60 = lean_ctor_get(x_18, 0); +x_61 = lean_ctor_get(x_18, 1); +lean_inc(x_61); +lean_inc(x_60); +lean_dec(x_18); +x_62 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_62, 0, x_60); +lean_ctor_set(x_62, 1, x_61); +return x_62; +} +} +} +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg), 11, 0); +return x_2; +} +} +lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1___rarg___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) { +_start: +{ +uint8_t x_10; lean_object* x_11; +x_10 = lean_unbox(x_2); +lean_dec(x_2); +x_11 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1___rarg(x_1, x_10, x_3, x_4, x_5, x_6, x_7, x_8, x_9); +return x_11; +} +} +static lean_object* _init_l_Lean_Meta_mkHCongrWithArity_withNewEqs___rarg___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(0u); +x_2 = lean_mk_empty_array_with_capacity(x_1); +return x_2; +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +_start: +{ +lean_object* x_9; lean_object* x_10; lean_object* x_11; +x_9 = lean_unsigned_to_nat(0u); +x_10 = l_Lean_Meta_mkHCongrWithArity_withNewEqs___rarg___closed__1; +x_11 = l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg(x_1, x_2, x_3, x_9, x_10, x_10, x_4, x_5, x_6, x_7, x_8); +return x_11; +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_withNewEqs(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_Lean_Meta_mkHCongrWithArity_withNewEqs___rarg), 8, 0); +return x_2; +} +} +static lean_object* _init_l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(1u); +x_2 = lean_mk_empty_array_with_capacity(x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(3u); +x_2 = lean_mk_empty_array_with_capacity(x_1); +return x_2; +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___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, lean_object* x_11, lean_object* x_12) { +_start: +{ +lean_object* x_13; lean_object* x_14; uint8_t x_15; uint8_t x_16; lean_object* x_17; +x_13 = l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1___closed__1; +lean_inc(x_1); +x_14 = lean_array_push(x_13, x_1); +x_15 = 0; +x_16 = 1; +lean_inc(x_8); +x_17 = l_Lean_Meta_mkLambdaFVars(x_14, x_2, x_15, x_16, x_8, x_9, x_10, x_11, x_12); +if (lean_obj_tag(x_17) == 0) +{ +lean_object* x_18; lean_object* x_19; lean_object* x_20; +x_18 = lean_ctor_get(x_17, 0); +lean_inc(x_18); +x_19 = lean_ctor_get(x_17, 1); +lean_inc(x_19); +lean_dec(x_17); +lean_inc(x_11); +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +x_20 = l_Lean_Meta_mkEqNDRec(x_18, x_3, x_6, x_8, x_9, x_10, x_11, x_19); +if (lean_obj_tag(x_20) == 0) +{ +lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; +x_21 = lean_ctor_get(x_20, 0); +lean_inc(x_21); +x_22 = lean_ctor_get(x_20, 1); +lean_inc(x_22); +lean_dec(x_20); +x_23 = l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1___closed__2; +x_24 = lean_array_push(x_23, x_4); +x_25 = lean_array_push(x_24, x_1); +x_26 = lean_array_push(x_25, x_5); +x_27 = l_Lean_Meta_mkLambdaFVars(x_26, x_21, x_15, x_16, x_8, x_9, x_10, x_11, x_22); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +return x_27; +} +else +{ +uint8_t x_28; +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_1); +x_28 = !lean_is_exclusive(x_20); +if (x_28 == 0) +{ +return x_20; +} +else +{ +lean_object* x_29; lean_object* x_30; lean_object* x_31; +x_29 = lean_ctor_get(x_20, 0); +x_30 = lean_ctor_get(x_20, 1); +lean_inc(x_30); +lean_inc(x_29); +lean_dec(x_20); +x_31 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_31, 0, x_29); +lean_ctor_set(x_31, 1, x_30); +return x_31; +} +} +} +else +{ +uint8_t x_32; +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_1); +x_32 = !lean_is_exclusive(x_17); +if (x_32 == 0) +{ +return x_17; +} +else +{ +lean_object* x_33; lean_object* x_34; lean_object* x_35; +x_33 = lean_ctor_get(x_17, 0); +x_34 = lean_ctor_get(x_17, 1); +lean_inc(x_34); +lean_inc(x_33); +lean_dec(x_17); +x_35 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_35, 0, x_33); +lean_ctor_set(x_35, 1, x_34); +return x_35; +} +} +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___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: +{ +lean_object* x_11; lean_object* x_12; lean_object* x_13; +x_11 = l_Lean_Expr_bindingBody_x21(x_1); +lean_dec(x_1); +x_12 = l_Lean_Expr_bindingBody_x21(x_2); +lean_dec(x_2); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +lean_inc(x_6); +x_13 = l_Lean_Meta_mkHCongrWithArity_mkProof(x_11, x_6, x_7, x_8, x_9, x_10); +if (lean_obj_tag(x_13) == 0) +{ +lean_object* x_14; lean_object* x_15; lean_object* x_16; +x_14 = lean_ctor_get(x_13, 0); +lean_inc(x_14); +x_15 = lean_ctor_get(x_13, 1); +lean_inc(x_15); +lean_dec(x_13); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +lean_inc(x_6); +lean_inc(x_5); +x_16 = lean_infer_type(x_5, x_6, x_7, x_8, x_9, x_15); +if (lean_obj_tag(x_16) == 0) +{ +lean_object* x_17; lean_object* x_18; lean_object* x_19; +x_17 = lean_ctor_get(x_16, 0); +lean_inc(x_17); +x_18 = lean_ctor_get(x_16, 1); +lean_inc(x_18); +lean_dec(x_16); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +lean_inc(x_6); +x_19 = lean_whnf(x_17, x_6, x_7, x_8, x_9, x_18); +if (lean_obj_tag(x_19) == 0) +{ +lean_object* x_20; lean_object* x_21; uint8_t x_22; +x_20 = lean_ctor_get(x_19, 0); +lean_inc(x_20); +x_21 = lean_ctor_get(x_19, 1); +lean_inc(x_21); +lean_dec(x_19); +x_22 = l_Lean_Expr_isHEq(x_20); +lean_dec(x_20); +if (x_22 == 0) +{ +lean_object* x_23; lean_object* x_24; +x_23 = lean_box(0); +lean_inc(x_5); +x_24 = l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1(x_3, x_12, x_14, x_4, x_5, x_5, x_23, x_6, x_7, x_8, x_9, x_21); +return x_24; +} +else +{ +lean_object* x_25; +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +lean_inc(x_6); +lean_inc(x_5); +x_25 = l_Lean_Meta_mkEqOfHEq(x_5, x_6, x_7, x_8, x_9, x_21); +if (lean_obj_tag(x_25) == 0) +{ +lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; +x_26 = lean_ctor_get(x_25, 0); +lean_inc(x_26); +x_27 = lean_ctor_get(x_25, 1); +lean_inc(x_27); +lean_dec(x_25); +x_28 = lean_box(0); +x_29 = l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1(x_3, x_12, x_14, x_4, x_5, x_26, x_28, x_6, x_7, x_8, x_9, x_27); +return x_29; +} +else +{ +uint8_t x_30; +lean_dec(x_14); +lean_dec(x_12); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +x_30 = !lean_is_exclusive(x_25); +if (x_30 == 0) +{ +return x_25; +} +else +{ +lean_object* x_31; lean_object* x_32; lean_object* x_33; +x_31 = lean_ctor_get(x_25, 0); +x_32 = lean_ctor_get(x_25, 1); +lean_inc(x_32); +lean_inc(x_31); +lean_dec(x_25); +x_33 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_33, 0, x_31); +lean_ctor_set(x_33, 1, x_32); +return x_33; +} +} +} +} +else +{ +uint8_t x_34; +lean_dec(x_14); +lean_dec(x_12); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +x_34 = !lean_is_exclusive(x_19); +if (x_34 == 0) +{ +return x_19; +} +else +{ +lean_object* x_35; lean_object* x_36; lean_object* x_37; +x_35 = lean_ctor_get(x_19, 0); +x_36 = lean_ctor_get(x_19, 1); +lean_inc(x_36); +lean_inc(x_35); +lean_dec(x_19); +x_37 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_37, 0, x_35); +lean_ctor_set(x_37, 1, x_36); +return x_37; +} +} +} +else +{ +uint8_t x_38; +lean_dec(x_14); +lean_dec(x_12); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +x_38 = !lean_is_exclusive(x_16); +if (x_38 == 0) +{ +return x_16; +} +else +{ +lean_object* x_39; lean_object* x_40; lean_object* x_41; +x_39 = lean_ctor_get(x_16, 0); +x_40 = lean_ctor_get(x_16, 1); +lean_inc(x_40); +lean_inc(x_39); +lean_dec(x_16); +x_41 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_41, 0, x_39); +lean_ctor_set(x_41, 1, x_40); +return x_41; +} +} +} +else +{ +uint8_t x_42; +lean_dec(x_12); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +x_42 = !lean_is_exclusive(x_13); +if (x_42 == 0) +{ +return x_13; +} +else +{ +lean_object* x_43; lean_object* x_44; lean_object* x_45; +x_43 = lean_ctor_get(x_13, 0); +x_44 = lean_ctor_get(x_13, 1); +lean_inc(x_44); +lean_inc(x_43); +lean_dec(x_13); +x_45 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_45, 0, x_43); +lean_ctor_set(x_45, 1, x_44); +return x_45; +} +} +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__3(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) { +_start: +{ +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_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19; +x_10 = l_Lean_instInhabitedExpr; +x_11 = lean_unsigned_to_nat(0u); +x_12 = lean_array_get(x_10, x_3, x_11); +x_13 = l_Lean_Expr_bindingBody_x21(x_1); +x_14 = lean_expr_instantiate1(x_13, x_2); +lean_dec(x_13); +x_15 = l_Lean_Expr_bindingName_x21(x_4); +x_16 = l_Lean_Expr_bindingDomain_x21(x_4); +x_17 = lean_alloc_closure((void*)(l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__2), 10, 4); +lean_closure_set(x_17, 0, x_14); +lean_closure_set(x_17, 1, x_4); +lean_closure_set(x_17, 2, x_12); +lean_closure_set(x_17, 3, x_2); +x_18 = 0; +x_19 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1___rarg(x_15, x_18, x_16, x_17, x_5, x_6, x_7, x_8, x_9); +return x_19; +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +_start: +{ +lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; +x_9 = l_Lean_instInhabitedExpr; +x_10 = lean_unsigned_to_nat(0u); +x_11 = lean_array_get(x_9, x_2, x_10); +lean_inc(x_3); +x_12 = lean_alloc_closure((void*)(l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__3___boxed), 9, 2); +lean_closure_set(x_12, 0, x_3); +lean_closure_set(x_12, 1, x_11); +x_13 = l_Lean_Meta_forallBoundedTelescope___at_Lean_Meta_addPPExplicitToExposeDiff_visit___spec__2___rarg(x_3, x_1, x_12, x_4, x_5, x_6, x_7, x_8); +return x_13; +} +} +static lean_object* _init_l_Lean_Meta_mkHCongrWithArity_mkProof___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("Eq"); +return x_1; +} +} +static lean_object* _init_l_Lean_Meta_mkHCongrWithArity_mkProof___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Meta_mkHCongrWithArity_mkProof___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Meta_mkHCongrWithArity_mkProof___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("HEq"); +return x_1; +} +} +static lean_object* _init_l_Lean_Meta_mkHCongrWithArity_mkProof___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Meta_mkHCongrWithArity_mkProof___closed__3; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Meta_mkHCongrWithArity_mkProof___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(1u); +x_2 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Meta_mkHCongrWithArity_mkProof___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Meta_mkHCongrWithArity_mkProof___closed__5; +x_2 = lean_alloc_closure((void*)(l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__4___boxed), 8, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; lean_object* x_8; uint8_t x_9; +x_7 = l_Lean_Meta_mkHCongrWithArity_mkProof___closed__2; +x_8 = lean_unsigned_to_nat(3u); +x_9 = l_Lean_Expr_isAppOfArity(x_1, x_7, x_8); +if (x_9 == 0) +{ +lean_object* x_10; lean_object* x_11; uint8_t x_12; +x_10 = l_Lean_Meta_mkHCongrWithArity_mkProof___closed__4; +x_11 = lean_unsigned_to_nat(4u); +x_12 = l_Lean_Expr_isAppOfArity(x_1, x_10, x_11); +if (x_12 == 0) +{ +lean_object* x_13; lean_object* x_14; lean_object* x_15; +x_13 = l_Lean_Meta_mkHCongrWithArity_mkProof___closed__5; +x_14 = l_Lean_Meta_mkHCongrWithArity_mkProof___closed__6; +x_15 = l_Lean_Meta_forallBoundedTelescope___at_Lean_Meta_addPPExplicitToExposeDiff_visit___spec__2___rarg(x_1, x_13, x_14, x_2, x_3, x_4, x_5, x_6); +return x_15; +} +else +{ +lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; +x_16 = l_Lean_Expr_appFn_x21(x_1); +lean_dec(x_1); +x_17 = l_Lean_Expr_appFn_x21(x_16); +lean_dec(x_16); +x_18 = l_Lean_Expr_appArg_x21(x_17); +lean_dec(x_17); +x_19 = l_Lean_Meta_mkHEqRefl(x_18, x_2, x_3, x_4, x_5, x_6); +return x_19; +} +} +else +{ +lean_object* x_20; lean_object* x_21; lean_object* x_22; +x_20 = l_Lean_Expr_appFn_x21(x_1); +lean_dec(x_1); +x_21 = l_Lean_Expr_appArg_x21(x_20); +lean_dec(x_20); +x_22 = l_Lean_Meta_mkEqRefl(x_21, x_2, x_3, x_4, x_5, x_6); +return x_22; +} +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___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) { +_start: +{ +lean_object* x_13; +x_13 = l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); +lean_dec(x_7); +return x_13; +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__3___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) { +_start: +{ +lean_object* x_10; +x_10 = l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__3(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9); +lean_dec(x_3); +lean_dec(x_1); +return x_10; +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +_start: +{ +lean_object* x_9; +x_9 = l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__4(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); +lean_dec(x_2); +return x_9; +} +} +lean_object* l_Lean_throwError___at_Lean_Meta_mkHCongrWithArity___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) { +_start: +{ +lean_object* x_7; lean_object* x_8; uint8_t x_9; +x_7 = lean_ctor_get(x_4, 3); +x_8 = l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(x_1, x_2, x_3, x_4, x_5, x_6); +x_9 = !lean_is_exclusive(x_8); +if (x_9 == 0) +{ +lean_object* x_10; lean_object* x_11; +x_10 = lean_ctor_get(x_8, 0); +lean_inc(x_7); +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_7); +lean_ctor_set(x_11, 1, x_10); +lean_ctor_set_tag(x_8, 1); +lean_ctor_set(x_8, 0, x_11); +return x_8; +} +else +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; +x_12 = lean_ctor_get(x_8, 0); +x_13 = lean_ctor_get(x_8, 1); +lean_inc(x_13); +lean_inc(x_12); +lean_dec(x_8); +lean_inc(x_7); +x_14 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_14, 0, x_7); +lean_ctor_set(x_14, 1, x_12); +x_15 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_15, 0, x_14); +lean_ctor_set(x_15, 1, x_13); +return x_15; +} +} +} +lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkHCongrWithArity___spec__2(lean_object* x_1, size_t x_2, size_t 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) { +_start: +{ +uint8_t x_10; +x_10 = x_3 < x_2; +if (x_10 == 0) +{ +lean_object* x_11; +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_4); +lean_ctor_set(x_11, 1, x_9); +return x_11; +} +else +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15; +x_12 = lean_array_uget(x_1, x_3); +x_13 = lean_ctor_get(x_4, 1); +lean_inc(x_13); +x_14 = lean_ctor_get(x_13, 0); +lean_inc(x_14); +x_15 = !lean_is_exclusive(x_4); +if (x_15 == 0) +{ +lean_object* x_16; lean_object* x_17; uint8_t x_18; +x_16 = lean_ctor_get(x_4, 0); +x_17 = lean_ctor_get(x_4, 1); +lean_dec(x_17); +x_18 = !lean_is_exclusive(x_13); +if (x_18 == 0) +{ +lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24; +x_19 = lean_ctor_get(x_13, 1); +x_20 = lean_ctor_get(x_13, 0); +lean_dec(x_20); +x_21 = lean_ctor_get(x_14, 0); +lean_inc(x_21); +x_22 = lean_ctor_get(x_14, 1); +lean_inc(x_22); +x_23 = lean_ctor_get(x_14, 2); +lean_inc(x_23); +x_24 = lean_nat_dec_lt(x_22, x_23); +if (x_24 == 0) +{ +lean_object* x_25; +lean_dec(x_23); +lean_dec(x_22); +lean_dec(x_21); +lean_dec(x_12); +x_25 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_25, 0, x_4); +lean_ctor_set(x_25, 1, x_9); +return x_25; +} +else +{ +uint8_t x_26; +x_26 = !lean_is_exclusive(x_14); +if (x_26 == 0) +{ +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; lean_object* x_34; lean_object* x_35; uint8_t x_36; +x_27 = lean_ctor_get(x_14, 2); +lean_dec(x_27); +x_28 = lean_ctor_get(x_14, 1); +lean_dec(x_28); +x_29 = lean_ctor_get(x_14, 0); +lean_dec(x_29); +x_30 = lean_array_fget(x_21, x_22); +x_31 = lean_unsigned_to_nat(1u); +x_32 = lean_nat_add(x_22, x_31); +lean_dec(x_22); +lean_ctor_set(x_14, 1, x_32); +x_33 = lean_ctor_get(x_16, 0); +lean_inc(x_33); +x_34 = lean_ctor_get(x_16, 1); +lean_inc(x_34); +x_35 = lean_ctor_get(x_16, 2); +lean_inc(x_35); +x_36 = lean_nat_dec_lt(x_34, x_35); +if (x_36 == 0) +{ +lean_object* x_37; +lean_dec(x_35); +lean_dec(x_34); +lean_dec(x_33); +lean_dec(x_30); +lean_dec(x_12); +x_37 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_37, 0, x_4); +lean_ctor_set(x_37, 1, x_9); +return x_37; +} +else +{ +uint8_t x_38; +x_38 = !lean_is_exclusive(x_16); +if (x_38 == 0) +{ +lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; size_t x_47; size_t x_48; +x_39 = lean_ctor_get(x_16, 2); +lean_dec(x_39); +x_40 = lean_ctor_get(x_16, 1); +lean_dec(x_40); +x_41 = lean_ctor_get(x_16, 0); +lean_dec(x_41); +x_42 = lean_array_fget(x_33, x_34); +x_43 = lean_nat_add(x_34, x_31); +lean_dec(x_34); +lean_ctor_set(x_16, 1, x_43); +x_44 = lean_array_push(x_19, x_12); +x_45 = lean_array_push(x_44, x_42); +x_46 = lean_array_push(x_45, x_30); +lean_ctor_set(x_13, 1, x_46); +x_47 = 1; +x_48 = x_3 + x_47; +x_3 = x_48; +goto _start; +} +else +{ +lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; size_t x_56; size_t x_57; +lean_dec(x_16); +x_50 = lean_array_fget(x_33, x_34); +x_51 = lean_nat_add(x_34, x_31); +lean_dec(x_34); +x_52 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_52, 0, x_33); +lean_ctor_set(x_52, 1, x_51); +lean_ctor_set(x_52, 2, x_35); +x_53 = lean_array_push(x_19, x_12); +x_54 = lean_array_push(x_53, x_50); +x_55 = lean_array_push(x_54, x_30); +lean_ctor_set(x_13, 1, x_55); +lean_ctor_set(x_4, 0, x_52); +x_56 = 1; +x_57 = x_3 + x_56; +x_3 = x_57; +goto _start; +} +} +} +else +{ +lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; uint8_t x_66; +lean_dec(x_14); +x_59 = lean_array_fget(x_21, x_22); +x_60 = lean_unsigned_to_nat(1u); +x_61 = lean_nat_add(x_22, x_60); +lean_dec(x_22); +x_62 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_62, 0, x_21); +lean_ctor_set(x_62, 1, x_61); +lean_ctor_set(x_62, 2, x_23); +x_63 = lean_ctor_get(x_16, 0); +lean_inc(x_63); +x_64 = lean_ctor_get(x_16, 1); +lean_inc(x_64); +x_65 = lean_ctor_get(x_16, 2); +lean_inc(x_65); +x_66 = lean_nat_dec_lt(x_64, x_65); +if (x_66 == 0) +{ +lean_object* x_67; +lean_dec(x_65); +lean_dec(x_64); +lean_dec(x_63); +lean_dec(x_59); +lean_dec(x_12); +lean_ctor_set(x_13, 0, x_62); +x_67 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_67, 0, x_4); +lean_ctor_set(x_67, 1, x_9); +return x_67; +} +else +{ +lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; size_t x_75; size_t x_76; +if (lean_is_exclusive(x_16)) { + lean_ctor_release(x_16, 0); + lean_ctor_release(x_16, 1); + lean_ctor_release(x_16, 2); + x_68 = x_16; +} else { + lean_dec_ref(x_16); + x_68 = lean_box(0); +} +x_69 = lean_array_fget(x_63, x_64); +x_70 = lean_nat_add(x_64, x_60); +lean_dec(x_64); +if (lean_is_scalar(x_68)) { + x_71 = lean_alloc_ctor(0, 3, 0); +} else { + x_71 = x_68; +} +lean_ctor_set(x_71, 0, x_63); +lean_ctor_set(x_71, 1, x_70); +lean_ctor_set(x_71, 2, x_65); +x_72 = lean_array_push(x_19, x_12); +x_73 = lean_array_push(x_72, x_69); +x_74 = lean_array_push(x_73, x_59); +lean_ctor_set(x_13, 1, x_74); +lean_ctor_set(x_13, 0, x_62); +lean_ctor_set(x_4, 0, x_71); +x_75 = 1; +x_76 = x_3 + x_75; +x_3 = x_76; +goto _start; +} +} +} +} +else +{ +lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; uint8_t x_82; +x_78 = lean_ctor_get(x_13, 1); +lean_inc(x_78); +lean_dec(x_13); +x_79 = lean_ctor_get(x_14, 0); +lean_inc(x_79); +x_80 = lean_ctor_get(x_14, 1); +lean_inc(x_80); +x_81 = lean_ctor_get(x_14, 2); +lean_inc(x_81); +x_82 = lean_nat_dec_lt(x_80, x_81); +if (x_82 == 0) +{ +lean_object* x_83; lean_object* x_84; +lean_dec(x_81); +lean_dec(x_80); +lean_dec(x_79); +lean_dec(x_12); +x_83 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_83, 0, x_14); +lean_ctor_set(x_83, 1, x_78); +lean_ctor_set(x_4, 1, x_83); +x_84 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_84, 0, x_4); +lean_ctor_set(x_84, 1, x_9); +return x_84; +} +else +{ +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; uint8_t x_93; +if (lean_is_exclusive(x_14)) { + lean_ctor_release(x_14, 0); + lean_ctor_release(x_14, 1); + lean_ctor_release(x_14, 2); + x_85 = x_14; +} else { + lean_dec_ref(x_14); + x_85 = lean_box(0); +} +x_86 = lean_array_fget(x_79, x_80); +x_87 = lean_unsigned_to_nat(1u); +x_88 = lean_nat_add(x_80, x_87); +lean_dec(x_80); +if (lean_is_scalar(x_85)) { + x_89 = lean_alloc_ctor(0, 3, 0); +} else { + x_89 = x_85; +} +lean_ctor_set(x_89, 0, x_79); +lean_ctor_set(x_89, 1, x_88); +lean_ctor_set(x_89, 2, x_81); +x_90 = lean_ctor_get(x_16, 0); +lean_inc(x_90); +x_91 = lean_ctor_get(x_16, 1); +lean_inc(x_91); +x_92 = lean_ctor_get(x_16, 2); +lean_inc(x_92); +x_93 = lean_nat_dec_lt(x_91, x_92); +if (x_93 == 0) +{ +lean_object* x_94; lean_object* x_95; +lean_dec(x_92); +lean_dec(x_91); +lean_dec(x_90); +lean_dec(x_86); +lean_dec(x_12); +x_94 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_94, 0, x_89); +lean_ctor_set(x_94, 1, x_78); +lean_ctor_set(x_4, 1, x_94); +x_95 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_95, 0, x_4); +lean_ctor_set(x_95, 1, x_9); +return x_95; +} +else +{ +lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; size_t x_104; size_t x_105; +if (lean_is_exclusive(x_16)) { + lean_ctor_release(x_16, 0); + lean_ctor_release(x_16, 1); + lean_ctor_release(x_16, 2); + x_96 = x_16; +} else { + lean_dec_ref(x_16); + x_96 = lean_box(0); +} +x_97 = lean_array_fget(x_90, x_91); +x_98 = lean_nat_add(x_91, x_87); +lean_dec(x_91); +if (lean_is_scalar(x_96)) { + x_99 = lean_alloc_ctor(0, 3, 0); +} else { + x_99 = x_96; +} +lean_ctor_set(x_99, 0, x_90); +lean_ctor_set(x_99, 1, x_98); +lean_ctor_set(x_99, 2, x_92); +x_100 = lean_array_push(x_78, x_12); +x_101 = lean_array_push(x_100, x_97); +x_102 = lean_array_push(x_101, x_86); +x_103 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_103, 0, x_89); +lean_ctor_set(x_103, 1, x_102); +lean_ctor_set(x_4, 1, x_103); +lean_ctor_set(x_4, 0, x_99); +x_104 = 1; +x_105 = x_3 + x_104; +x_3 = x_105; +goto _start; +} +} +} +} +else +{ +lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; uint8_t x_113; +x_107 = lean_ctor_get(x_4, 0); +lean_inc(x_107); +lean_dec(x_4); +x_108 = lean_ctor_get(x_13, 1); +lean_inc(x_108); +if (lean_is_exclusive(x_13)) { + lean_ctor_release(x_13, 0); + lean_ctor_release(x_13, 1); + x_109 = x_13; +} else { + lean_dec_ref(x_13); + x_109 = lean_box(0); +} +x_110 = lean_ctor_get(x_14, 0); +lean_inc(x_110); +x_111 = lean_ctor_get(x_14, 1); +lean_inc(x_111); +x_112 = lean_ctor_get(x_14, 2); +lean_inc(x_112); +x_113 = lean_nat_dec_lt(x_111, x_112); +if (x_113 == 0) +{ +lean_object* x_114; lean_object* x_115; lean_object* x_116; +lean_dec(x_112); +lean_dec(x_111); +lean_dec(x_110); +lean_dec(x_12); +if (lean_is_scalar(x_109)) { + x_114 = lean_alloc_ctor(0, 2, 0); +} else { + x_114 = x_109; +} +lean_ctor_set(x_114, 0, x_14); +lean_ctor_set(x_114, 1, x_108); +x_115 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_115, 0, x_107); +lean_ctor_set(x_115, 1, x_114); +x_116 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_116, 0, x_115); +lean_ctor_set(x_116, 1, x_9); +return x_116; +} +else +{ +lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; uint8_t x_125; +if (lean_is_exclusive(x_14)) { + lean_ctor_release(x_14, 0); + lean_ctor_release(x_14, 1); + lean_ctor_release(x_14, 2); + x_117 = x_14; +} else { + lean_dec_ref(x_14); + x_117 = lean_box(0); +} +x_118 = lean_array_fget(x_110, x_111); +x_119 = lean_unsigned_to_nat(1u); +x_120 = lean_nat_add(x_111, x_119); +lean_dec(x_111); +if (lean_is_scalar(x_117)) { + x_121 = lean_alloc_ctor(0, 3, 0); +} else { + x_121 = x_117; +} +lean_ctor_set(x_121, 0, x_110); +lean_ctor_set(x_121, 1, x_120); +lean_ctor_set(x_121, 2, x_112); +x_122 = lean_ctor_get(x_107, 0); +lean_inc(x_122); +x_123 = lean_ctor_get(x_107, 1); +lean_inc(x_123); +x_124 = lean_ctor_get(x_107, 2); +lean_inc(x_124); +x_125 = lean_nat_dec_lt(x_123, x_124); +if (x_125 == 0) +{ +lean_object* x_126; lean_object* x_127; lean_object* x_128; +lean_dec(x_124); +lean_dec(x_123); +lean_dec(x_122); +lean_dec(x_118); +lean_dec(x_12); +if (lean_is_scalar(x_109)) { + x_126 = lean_alloc_ctor(0, 2, 0); +} else { + x_126 = x_109; +} +lean_ctor_set(x_126, 0, x_121); +lean_ctor_set(x_126, 1, x_108); +x_127 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_127, 0, x_107); +lean_ctor_set(x_127, 1, x_126); +x_128 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_128, 0, x_127); +lean_ctor_set(x_128, 1, x_9); +return x_128; +} +else +{ +lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; size_t x_138; size_t x_139; +if (lean_is_exclusive(x_107)) { + lean_ctor_release(x_107, 0); + lean_ctor_release(x_107, 1); + lean_ctor_release(x_107, 2); + x_129 = x_107; +} else { + lean_dec_ref(x_107); + x_129 = lean_box(0); +} +x_130 = lean_array_fget(x_122, x_123); +x_131 = lean_nat_add(x_123, x_119); +lean_dec(x_123); +if (lean_is_scalar(x_129)) { + x_132 = lean_alloc_ctor(0, 3, 0); +} else { + x_132 = x_129; +} +lean_ctor_set(x_132, 0, x_122); +lean_ctor_set(x_132, 1, x_131); +lean_ctor_set(x_132, 2, x_124); +x_133 = lean_array_push(x_108, x_12); +x_134 = lean_array_push(x_133, x_130); +x_135 = lean_array_push(x_134, x_118); +if (lean_is_scalar(x_109)) { + x_136 = lean_alloc_ctor(0, 2, 0); +} else { + x_136 = x_109; +} +lean_ctor_set(x_136, 0, x_121); +lean_ctor_set(x_136, 1, x_135); +x_137 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_137, 0, x_132); +lean_ctor_set(x_137, 1, x_136); +x_138 = 1; +x_139 = x_3 + x_138; +x_3 = x_139; +x_4 = x_137; +goto _start; +} +} +} +} +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity___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) { +_start: +{ +uint8_t x_9; uint8_t x_10; lean_object* x_11; +x_9 = 0; +x_10 = 1; +lean_inc(x_4); +x_11 = l_Lean_Meta_mkForallFVars(x_1, x_3, x_9, x_10, x_4, x_5, x_6, x_7, x_8); +if (lean_obj_tag(x_11) == 0) +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; +x_12 = lean_ctor_get(x_11, 0); +lean_inc(x_12); +x_13 = lean_ctor_get(x_11, 1); +lean_inc(x_13); +lean_dec(x_11); +lean_inc(x_12); +x_14 = l_Lean_Meta_mkHCongrWithArity_mkProof(x_12, x_4, x_5, x_6, x_7, x_13); +if (lean_obj_tag(x_14) == 0) +{ +uint8_t x_15; +x_15 = !lean_is_exclusive(x_14); +if (x_15 == 0) +{ +lean_object* x_16; lean_object* x_17; +x_16 = lean_ctor_get(x_14, 0); +x_17 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_17, 0, x_12); +lean_ctor_set(x_17, 1, x_16); +lean_ctor_set(x_17, 2, x_2); +lean_ctor_set(x_14, 0, x_17); +return x_14; +} +else +{ +lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; +x_18 = lean_ctor_get(x_14, 0); +x_19 = lean_ctor_get(x_14, 1); +lean_inc(x_19); +lean_inc(x_18); +lean_dec(x_14); +x_20 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_20, 0, x_12); +lean_ctor_set(x_20, 1, x_18); +lean_ctor_set(x_20, 2, x_2); +x_21 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_21, 0, x_20); +lean_ctor_set(x_21, 1, x_19); +return x_21; +} +} +else +{ +uint8_t x_22; +lean_dec(x_12); +lean_dec(x_2); +x_22 = !lean_is_exclusive(x_14); +if (x_22 == 0) +{ +return x_14; +} +else +{ +lean_object* x_23; lean_object* x_24; lean_object* x_25; +x_23 = lean_ctor_get(x_14, 0); +x_24 = lean_ctor_get(x_14, 1); +lean_inc(x_24); +lean_inc(x_23); +lean_dec(x_14); +x_25 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_25, 0, x_23); +lean_ctor_set(x_25, 1, x_24); +return x_25; +} +} +} +else +{ +uint8_t x_26; +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_2); +x_26 = !lean_is_exclusive(x_11); +if (x_26 == 0) +{ +return x_11; +} +else +{ +lean_object* x_27; lean_object* x_28; lean_object* x_29; +x_27 = lean_ctor_get(x_11, 0); +x_28 = lean_ctor_get(x_11, 1); +lean_inc(x_28); +lean_inc(x_27); +lean_dec(x_11); +x_29 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_29, 0, x_27); +lean_ctor_set(x_29, 1, x_28); +return x_29; +} +} +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity___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, lean_object* x_11, lean_object* x_12) { +_start: +{ +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_object* x_19; lean_object* x_20; size_t x_21; size_t x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; uint8_t x_30; +x_13 = lean_array_get_size(x_1); +x_14 = lean_unsigned_to_nat(0u); +x_15 = l_Array_toSubarray___rarg(x_1, x_14, x_13); +x_16 = lean_array_get_size(x_6); +x_17 = l_Array_toSubarray___rarg(x_6, x_14, x_16); +x_18 = l_Lean_Meta_mkHCongrWithArity_withNewEqs___rarg___closed__1; +x_19 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_19, 0, x_17); +lean_ctor_set(x_19, 1, x_18); +x_20 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_20, 0, x_15); +lean_ctor_set(x_20, 1, x_19); +x_21 = lean_usize_of_nat(x_2); +lean_dec(x_2); +x_22 = 0; +x_23 = l_Array_forInUnsafe_loop___at_Lean_Meta_mkHCongrWithArity___spec__2(x_3, x_21, x_22, x_20, x_8, x_9, x_10, x_11, x_12); +lean_dec(x_3); +x_24 = lean_ctor_get(x_23, 0); +lean_inc(x_24); +x_25 = lean_ctor_get(x_24, 1); +lean_inc(x_25); +lean_dec(x_24); +x_26 = lean_ctor_get(x_23, 1); +lean_inc(x_26); +lean_dec(x_23); +x_27 = lean_ctor_get(x_25, 1); +lean_inc(x_27); +lean_dec(x_25); +x_28 = l_Lean_Expr_consumeAutoOptParam(x_4); +x_29 = l_Lean_Expr_consumeAutoOptParam(x_5); +x_30 = lean_expr_eqv(x_28, x_29); +if (x_30 == 0) +{ +lean_object* x_31; +lean_inc(x_11); +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +x_31 = l_Lean_Meta_mkHEq(x_28, x_29, x_8, x_9, x_10, x_11, x_26); +if (lean_obj_tag(x_31) == 0) +{ +lean_object* x_32; lean_object* x_33; lean_object* x_34; +x_32 = lean_ctor_get(x_31, 0); +lean_inc(x_32); +x_33 = lean_ctor_get(x_31, 1); +lean_inc(x_33); +lean_dec(x_31); +x_34 = l_Lean_Meta_mkHCongrWithArity___lambda__1(x_27, x_7, x_32, x_8, x_9, x_10, x_11, x_33); +return x_34; +} +else +{ +uint8_t x_35; +lean_dec(x_27); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +x_35 = !lean_is_exclusive(x_31); +if (x_35 == 0) +{ +return x_31; +} +else +{ +lean_object* x_36; lean_object* x_37; lean_object* x_38; +x_36 = lean_ctor_get(x_31, 0); +x_37 = lean_ctor_get(x_31, 1); +lean_inc(x_37); +lean_inc(x_36); +lean_dec(x_31); +x_38 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_38, 0, x_36); +lean_ctor_set(x_38, 1, x_37); +return x_38; +} +} +} +else +{ +lean_object* x_39; +lean_inc(x_11); +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +x_39 = l_Lean_Meta_mkEq(x_28, x_29, x_8, x_9, x_10, x_11, x_26); +if (lean_obj_tag(x_39) == 0) +{ +lean_object* x_40; lean_object* x_41; lean_object* x_42; +x_40 = lean_ctor_get(x_39, 0); +lean_inc(x_40); +x_41 = lean_ctor_get(x_39, 1); +lean_inc(x_41); +lean_dec(x_39); +x_42 = l_Lean_Meta_mkHCongrWithArity___lambda__1(x_27, x_7, x_40, x_8, x_9, x_10, x_11, x_41); +return x_42; +} +else +{ +uint8_t x_43; +lean_dec(x_27); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +x_43 = !lean_is_exclusive(x_39); +if (x_43 == 0) +{ +return x_39; +} +else +{ +lean_object* x_44; lean_object* x_45; lean_object* x_46; +x_44 = lean_ctor_get(x_39, 0); +x_45 = lean_ctor_get(x_39, 1); +lean_inc(x_45); +lean_inc(x_44); +lean_dec(x_39); +x_46 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_46, 0, x_44); +lean_ctor_set(x_46, 1, x_45); +return x_46; +} +} +} +} +} +static lean_object* _init_l_Lean_Meta_mkHCongrWithArity___lambda__3___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("failed to generate hcongr theorem, insufficient number of arguments"); +return x_1; +} +} +static lean_object* _init_l_Lean_Meta_mkHCongrWithArity___lambda__3___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Meta_mkHCongrWithArity___lambda__3___closed__1; +x_2 = l_Lean_stringToMessageData(x_1); +return x_2; +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity___lambda__3(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: +{ +lean_object* x_11; uint8_t x_12; +x_11 = lean_array_get_size(x_1); +x_12 = lean_nat_dec_eq(x_11, x_2); +lean_dec(x_2); +if (x_12 == 0) +{ +lean_object* x_13; lean_object* x_14; +lean_dec(x_11); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_1); +x_13 = l_Lean_Meta_mkHCongrWithArity___lambda__3___closed__2; +x_14 = l_Lean_throwError___at_Lean_Meta_mkHCongrWithArity___spec__1(x_13, x_6, x_7, x_8, x_9, x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +return x_14; +} +else +{ +lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; +x_15 = lean_ctor_get(x_6, 1); +lean_inc(x_15); +x_16 = l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames(x_4, x_15); +x_17 = l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_setBinderInfosD(x_4, x_16); +x_18 = l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_setBinderInfosD(x_1, x_17); +x_19 = l_Lean_Meta_getLocalInstances(x_6, x_7, x_8, x_9, x_10); +x_20 = lean_ctor_get(x_19, 0); +lean_inc(x_20); +x_21 = lean_ctor_get(x_19, 1); +lean_inc(x_21); +lean_dec(x_19); +lean_inc(x_1); +lean_inc(x_4); +x_22 = lean_alloc_closure((void*)(l_Lean_Meta_mkHCongrWithArity___lambda__2), 12, 5); +lean_closure_set(x_22, 0, x_4); +lean_closure_set(x_22, 1, x_11); +lean_closure_set(x_22, 2, x_1); +lean_closure_set(x_22, 3, x_3); +lean_closure_set(x_22, 4, x_5); +x_23 = lean_alloc_closure((void*)(l_Lean_Meta_mkHCongrWithArity_withNewEqs___rarg), 8, 3); +lean_closure_set(x_23, 0, x_1); +lean_closure_set(x_23, 1, x_4); +lean_closure_set(x_23, 2, x_22); +x_24 = l_Lean_Meta_withLCtx___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_mkLeveErrorMessageCore___spec__2___rarg(x_18, x_20, x_23, x_6, x_7, x_8, x_9, x_21); +return x_24; +} +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity___lambda__4(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: +{ +lean_object* x_11; lean_object* x_12; +x_11 = lean_alloc_closure((void*)(l_Lean_Meta_mkHCongrWithArity___lambda__3), 10, 3); +lean_closure_set(x_11, 0, x_4); +lean_closure_set(x_11, 1, x_1); +lean_closure_set(x_11, 2, x_5); +x_12 = l_Lean_Meta_forallBoundedTelescope___at_Lean_Meta_addPPExplicitToExposeDiff_visit___spec__2___rarg(x_2, x_3, x_11, x_6, x_7, x_8, x_9, x_10); +return x_12; +} +} +lean_object* l_Lean_Meta_mkHCongrWithArity(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +_start: +{ +lean_object* x_8; +lean_inc(x_6); +lean_inc(x_5); +lean_inc(x_4); +lean_inc(x_3); +x_8 = lean_infer_type(x_1, x_3, x_4, x_5, x_6, x_7); +if (lean_obj_tag(x_8) == 0) +{ +lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; +x_9 = lean_ctor_get(x_8, 0); +lean_inc(x_9); +x_10 = lean_ctor_get(x_8, 1); +lean_inc(x_10); +lean_dec(x_8); +lean_inc(x_2); +x_11 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_11, 0, x_2); +lean_inc(x_11); +lean_inc(x_9); +x_12 = lean_alloc_closure((void*)(l_Lean_Meta_mkHCongrWithArity___lambda__4), 10, 3); +lean_closure_set(x_12, 0, x_2); +lean_closure_set(x_12, 1, x_9); +lean_closure_set(x_12, 2, x_11); +x_13 = l_Lean_Meta_forallBoundedTelescope___at_Lean_Meta_addPPExplicitToExposeDiff_visit___spec__2___rarg(x_9, x_11, x_12, x_3, x_4, x_5, x_6, x_10); +return x_13; +} +else +{ +uint8_t x_14; +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +x_14 = !lean_is_exclusive(x_8); +if (x_14 == 0) +{ +return x_8; +} +else +{ +lean_object* x_15; lean_object* x_16; lean_object* x_17; +x_15 = lean_ctor_get(x_8, 0); +x_16 = lean_ctor_get(x_8, 1); +lean_inc(x_16); +lean_inc(x_15); +lean_dec(x_8); +x_17 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_17, 0, x_15); +lean_ctor_set(x_17, 1, x_16); +return x_17; +} +} +} +} +lean_object* l_Lean_throwError___at_Lean_Meta_mkHCongrWithArity___spec__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) { +_start: +{ +lean_object* x_7; +x_7 = l_Lean_throwError___at_Lean_Meta_mkHCongrWithArity___spec__1(x_1, x_2, x_3, x_4, x_5, x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_7; +} +} +lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkHCongrWithArity___spec__2___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) { +_start: +{ +size_t x_10; size_t x_11; lean_object* x_12; +x_10 = lean_unbox_usize(x_2); +lean_dec(x_2); +x_11 = lean_unbox_usize(x_3); +lean_dec(x_3); +x_12 = l_Array_forInUnsafe_loop___at_Lean_Meta_mkHCongrWithArity___spec__2(x_1, x_10, x_11, x_4, x_5, x_6, x_7, x_8, x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_1); +return x_12; +} +} +lean_object* l_Lean_Meta_mkHCongr(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +lean_inc(x_5); +lean_inc(x_4); +lean_inc(x_3); +lean_inc(x_2); +lean_inc(x_1); +x_7 = l_Lean_Meta_getFunInfo(x_1, x_2, x_3, x_4, x_5, x_6); +if (lean_obj_tag(x_7) == 0) +{ +lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; +x_8 = lean_ctor_get(x_7, 0); +lean_inc(x_8); +x_9 = lean_ctor_get(x_7, 1); +lean_inc(x_9); +lean_dec(x_7); +x_10 = l_Lean_Meta_FunInfo_getArity(x_8); +lean_dec(x_8); +x_11 = l_Lean_Meta_mkHCongrWithArity(x_1, x_10, x_2, x_3, x_4, x_5, x_9); +return x_11; +} +else +{ +uint8_t x_12; +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_12 = !lean_is_exclusive(x_7); +if (x_12 == 0) +{ +return x_7; +} +else +{ +lean_object* x_13; lean_object* x_14; lean_object* x_15; +x_13 = lean_ctor_get(x_7, 0); +x_14 = lean_ctor_get(x_7, 1); +lean_inc(x_14); +lean_inc(x_13); +lean_dec(x_7); +x_15 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_15, 0, x_13); +lean_ctor_set(x_15, 1, x_14); +return x_15; +} +} +} +} +lean_object* initialize_Init(lean_object*); +lean_object* initialize_Lean_Meta_AppBuilder(lean_object*); +static bool _G_initialized = false; +lean_object* initialize_Lean_Meta_CongrTheorems(lean_object* w) { +lean_object * res; +if (_G_initialized) return lean_io_result_mk_ok(lean_box(0)); +_G_initialized = true; +res = initialize_Init(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +res = initialize_Lean_Meta_AppBuilder(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +l_Lean_Meta_CongrArgKind_noConfusion___rarg___closed__1 = _init_l_Lean_Meta_CongrArgKind_noConfusion___rarg___closed__1(); +lean_mark_persistent(l_Lean_Meta_CongrArgKind_noConfusion___rarg___closed__1); +l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___spec__1___closed__1 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___spec__1___closed__1(); +lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Meta_CongrTheorems_0__Lean_Meta_addPrimeToFVarUserNames___spec__1___closed__1); +l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___closed__1 = _init_l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___closed__1(); +lean_mark_persistent(l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___closed__1); +l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___closed__2 = _init_l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___closed__2(); +lean_mark_persistent(l_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___rarg___closed__2); +l_Lean_Meta_mkHCongrWithArity_withNewEqs___rarg___closed__1 = _init_l_Lean_Meta_mkHCongrWithArity_withNewEqs___rarg___closed__1(); +lean_mark_persistent(l_Lean_Meta_mkHCongrWithArity_withNewEqs___rarg___closed__1); +l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1___closed__1 = _init_l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1___closed__1(); +lean_mark_persistent(l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1___closed__1); +l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1___closed__2 = _init_l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1___closed__2(); +lean_mark_persistent(l_Lean_Meta_mkHCongrWithArity_mkProof___lambda__1___closed__2); +l_Lean_Meta_mkHCongrWithArity_mkProof___closed__1 = _init_l_Lean_Meta_mkHCongrWithArity_mkProof___closed__1(); +lean_mark_persistent(l_Lean_Meta_mkHCongrWithArity_mkProof___closed__1); +l_Lean_Meta_mkHCongrWithArity_mkProof___closed__2 = _init_l_Lean_Meta_mkHCongrWithArity_mkProof___closed__2(); +lean_mark_persistent(l_Lean_Meta_mkHCongrWithArity_mkProof___closed__2); +l_Lean_Meta_mkHCongrWithArity_mkProof___closed__3 = _init_l_Lean_Meta_mkHCongrWithArity_mkProof___closed__3(); +lean_mark_persistent(l_Lean_Meta_mkHCongrWithArity_mkProof___closed__3); +l_Lean_Meta_mkHCongrWithArity_mkProof___closed__4 = _init_l_Lean_Meta_mkHCongrWithArity_mkProof___closed__4(); +lean_mark_persistent(l_Lean_Meta_mkHCongrWithArity_mkProof___closed__4); +l_Lean_Meta_mkHCongrWithArity_mkProof___closed__5 = _init_l_Lean_Meta_mkHCongrWithArity_mkProof___closed__5(); +lean_mark_persistent(l_Lean_Meta_mkHCongrWithArity_mkProof___closed__5); +l_Lean_Meta_mkHCongrWithArity_mkProof___closed__6 = _init_l_Lean_Meta_mkHCongrWithArity_mkProof___closed__6(); +lean_mark_persistent(l_Lean_Meta_mkHCongrWithArity_mkProof___closed__6); +l_Lean_Meta_mkHCongrWithArity___lambda__3___closed__1 = _init_l_Lean_Meta_mkHCongrWithArity___lambda__3___closed__1(); +lean_mark_persistent(l_Lean_Meta_mkHCongrWithArity___lambda__3___closed__1); +l_Lean_Meta_mkHCongrWithArity___lambda__3___closed__2 = _init_l_Lean_Meta_mkHCongrWithArity___lambda__3___closed__2(); +lean_mark_persistent(l_Lean_Meta_mkHCongrWithArity___lambda__3___closed__2); +return lean_io_result_mk_ok(lean_box(0)); +} +#ifdef __cplusplus +} +#endif diff --git a/stage0/stdlib/Lean/Meta/ExprDefEq.c b/stage0/stdlib/Lean/Meta/ExprDefEq.c index 8a37f05377..a2594117cd 100644 --- a/stage0/stdlib/Lean/Meta/ExprDefEq.c +++ b/stage0/stdlib/Lean/Meta/ExprDefEq.c @@ -13972,7 +13972,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_CheckAssignment_check___closed__1; x_2 = l_Lean_Meta_CheckAssignment_check___closed__2; -x_3 = lean_unsigned_to_nat(943u); +x_3 = lean_unsigned_to_nat(949u); x_4 = lean_unsigned_to_nat(19u); x_5 = l_Lean_Meta_CheckAssignment_check___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -14001,7 +14001,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_CheckAssignment_check___closed__1; x_2 = l_Lean_Meta_CheckAssignment_check___closed__5; -x_3 = lean_unsigned_to_nat(948u); +x_3 = lean_unsigned_to_nat(954u); x_4 = lean_unsigned_to_nat(20u); x_5 = l_Lean_Meta_CheckAssignment_check___closed__6; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -14030,7 +14030,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_CheckAssignment_check___closed__1; x_2 = l_Lean_Meta_CheckAssignment_check___closed__8; -x_3 = lean_unsigned_to_nat(976u); +x_3 = lean_unsigned_to_nat(982u); x_4 = lean_unsigned_to_nat(19u); x_5 = l_Lean_Meta_CheckAssignment_check___closed__9; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -14059,7 +14059,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_CheckAssignment_check___closed__1; x_2 = l_Lean_Meta_CheckAssignment_check___closed__11; -x_3 = lean_unsigned_to_nat(962u); +x_3 = lean_unsigned_to_nat(968u); x_4 = lean_unsigned_to_nat(23u); x_5 = l_Lean_Meta_CheckAssignment_check___closed__12; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -14088,7 +14088,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_CheckAssignment_check___closed__1; x_2 = l_Lean_Meta_CheckAssignment_check___closed__14; -x_3 = lean_unsigned_to_nat(985u); +x_3 = lean_unsigned_to_nat(991u); x_4 = lean_unsigned_to_nat(22u); x_5 = l_Lean_Meta_CheckAssignment_check___closed__15; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); diff --git a/stage0/stdlib/Lean/Meta/FunInfo.c b/stage0/stdlib/Lean/Meta/FunInfo.c index 6d46035c6e..6dd5bab947 100644 --- a/stage0/stdlib/Lean/Meta/FunInfo.c +++ b/stage0/stdlib/Lean/Meta/FunInfo.c @@ -64,11 +64,13 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*); lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_whenHasVar(lean_object*); lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps_visit(lean_object*, lean_object*, lean_object*); lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1(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_FunInfo_getArity___boxed(lean_object*); lean_object* l_Array_mapIdxM_map___at___private_Lean_Meta_FunInfo_0__Lean_Meta_updateHasFwdDeps___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_getFunInfoNArgs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*); lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_checkFunInfoCache(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_FunInfo_getArity(lean_object*); lean_object* l_Lean_Meta_getTransparency(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_checkFunInfoCache___closed__1; lean_object* l_Array_qpartition_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -2548,6 +2550,24 @@ x_9 = l___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux(x_1, x_8, x_3, x_ return x_9; } } +lean_object* l_Lean_Meta_FunInfo_getArity(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; +x_2 = lean_ctor_get(x_1, 0); +x_3 = lean_array_get_size(x_2); +return x_3; +} +} +lean_object* l_Lean_Meta_FunInfo_getArity___boxed(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = l_Lean_Meta_FunInfo_getArity(x_1); +lean_dec(x_1); +return x_2; +} +} lean_object* initialize_Init(lean_object*); lean_object* initialize_Lean_Meta_Basic(lean_object*); lean_object* initialize_Lean_Meta_InferType(lean_object*); diff --git a/stage0/stdlib/Lean/Meta/Tactic/Cases.c b/stage0/stdlib/Lean/Meta/Tactic/Cases.c index 23e0b44355..7db3ba3830 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Cases.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Cases.c @@ -248,7 +248,7 @@ lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_Tactic_Cases_0__Lea 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*); uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Meta_Tactic_Cases_0__Lean_Meta_Cases_hasIndepIndices___spec__43(lean_object*, lean_object*, lean_object*, size_t, size_t); static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_Tactic_Cases_0__Lean_Meta_Cases_mkCasesContext_x3f___spec__1___closed__1; -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Cases___hyg_3613_(lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Cases___hyg_3624_(lean_object*); lean_object* l_Lean_LocalDecl_fvarId(lean_object*); uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Meta_Tactic_Cases_0__Lean_Meta_Cases_hasIndepIndices___spec__15(lean_object*, lean_object*, lean_object*, size_t, size_t); static lean_object* l_Lean_Meta_Cases_unifyEqs_substEq___closed__1; @@ -16513,7 +16513,7 @@ lean_dec(x_2); return x_7; } } -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Cases___hyg_3613_(lean_object* x_1) { +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Cases___hyg_3624_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -16691,7 +16691,7 @@ l_Lean_Meta_byCases___closed__4 = _init_l_Lean_Meta_byCases___closed__4(); lean_mark_persistent(l_Lean_Meta_byCases___closed__4); l_Lean_Meta_byCases___closed__5 = _init_l_Lean_Meta_byCases___closed__5(); lean_mark_persistent(l_Lean_Meta_byCases___closed__5); -res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Cases___hyg_3613_(lean_io_mk_world()); +res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Cases___hyg_3624_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); return lean_io_result_mk_ok(lean_box(0)); diff --git a/stage0/stdlib/Lean/Meta/Tactic/Simp/SimpLemmas.c b/stage0/stdlib/Lean/Meta/Tactic/Simp/SimpLemmas.c index 181f7e7281..0d87f0bdc3 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Simp/SimpLemmas.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Simp/SimpLemmas.c @@ -10395,7 +10395,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_SimpLemma_getValue___closed__1; x_2 = l_Lean_Meta_SimpLemma_getValue___closed__2; -x_3 = lean_unsigned_to_nat(917u); +x_3 = lean_unsigned_to_nat(923u); x_4 = lean_unsigned_to_nat(20u); x_5 = l_Lean_Meta_SimpLemma_getValue___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); diff --git a/stage0/stdlib/Lean/Meta/Transform.c b/stage0/stdlib/Lean/Meta/Transform.c index 2cd25a4aa0..be06d33edb 100644 --- a/stage0/stdlib/Lean/Meta/Transform.c +++ b/stage0/stdlib/Lean/Meta/Transform.c @@ -670,7 +670,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_Core_transform_visit___rarg___lambda__2___closed__1; x_2 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__2; -x_3 = lean_unsigned_to_nat(976u); +x_3 = lean_unsigned_to_nat(982u); x_4 = lean_unsigned_to_nat(19u); x_5 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -777,7 +777,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_Core_transform_visit___rarg___lambda__2___closed__1; x_2 = l_Lean_Core_transform_visit___rarg___lambda__4___closed__1; -x_3 = lean_unsigned_to_nat(962u); +x_3 = lean_unsigned_to_nat(968u); x_4 = lean_unsigned_to_nat(23u); x_5 = l_Lean_Core_transform_visit___rarg___lambda__4___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -884,7 +884,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_Core_transform_visit___rarg___lambda__2___closed__1; x_2 = l_Lean_Core_transform_visit___rarg___lambda__6___closed__1; -x_3 = lean_unsigned_to_nat(985u); +x_3 = lean_unsigned_to_nat(991u); x_4 = lean_unsigned_to_nat(22u); x_5 = l_Lean_Core_transform_visit___rarg___lambda__6___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -1022,7 +1022,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_Core_transform_visit___rarg___lambda__2___closed__1; x_2 = l_Lean_Core_transform_visit___rarg___lambda__9___closed__1; -x_3 = lean_unsigned_to_nat(943u); +x_3 = lean_unsigned_to_nat(949u); x_4 = lean_unsigned_to_nat(19u); x_5 = l_Lean_Core_transform_visit___rarg___lambda__9___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -1096,7 +1096,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_Core_transform_visit___rarg___lambda__2___closed__1; x_2 = l_Lean_Core_transform_visit___rarg___lambda__10___closed__1; -x_3 = lean_unsigned_to_nat(948u); +x_3 = lean_unsigned_to_nat(954u); x_4 = lean_unsigned_to_nat(20u); x_5 = l_Lean_Core_transform_visit___rarg___lambda__10___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); diff --git a/stage0/stdlib/Lean/MetavarContext.c b/stage0/stdlib/Lean/MetavarContext.c index a91400b842..6b75ed08a2 100644 --- a/stage0/stdlib/Lean/MetavarContext.c +++ b/stage0/stdlib/Lean/MetavarContext.c @@ -10397,7 +10397,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_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1; x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__2; -x_3 = lean_unsigned_to_nat(926u); +x_3 = lean_unsigned_to_nat(932u); x_4 = lean_unsigned_to_nat(16u); x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10480,7 +10480,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_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1; x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__11___closed__1; -x_3 = lean_unsigned_to_nat(917u); +x_3 = lean_unsigned_to_nat(923u); x_4 = lean_unsigned_to_nat(20u); x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__11___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10566,7 +10566,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_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1; x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__12___closed__1; -x_3 = lean_unsigned_to_nat(976u); +x_3 = lean_unsigned_to_nat(982u); x_4 = lean_unsigned_to_nat(19u); x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__12___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10673,7 +10673,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_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1; x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__14___closed__1; -x_3 = lean_unsigned_to_nat(962u); +x_3 = lean_unsigned_to_nat(968u); x_4 = lean_unsigned_to_nat(23u); x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__14___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10780,7 +10780,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_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1; x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__16___closed__1; -x_3 = lean_unsigned_to_nat(985u); +x_3 = lean_unsigned_to_nat(991u); x_4 = lean_unsigned_to_nat(22u); x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__16___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -10914,7 +10914,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_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1; x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__19___closed__1; -x_3 = lean_unsigned_to_nat(943u); +x_3 = lean_unsigned_to_nat(949u); x_4 = lean_unsigned_to_nat(19u); x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__19___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -11000,7 +11000,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_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1; x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__20___closed__1; -x_3 = lean_unsigned_to_nat(948u); +x_3 = lean_unsigned_to_nat(954u); x_4 = lean_unsigned_to_nat(20u); x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__20___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); diff --git a/stage0/stdlib/Lean/Widget/InteractiveCode.c b/stage0/stdlib/Lean/Widget/InteractiveCode.c index 5fcdc2bee9..fc173dfd7f 100644 --- a/stage0/stdlib/Lean/Widget/InteractiveCode.c +++ b/stage0/stdlib/Lean/Widget/InteractiveCode.c @@ -52,7 +52,6 @@ lean_object* l_Lean_Widget_traverse_go(lean_object*, lean_object*, lean_object*, lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_CodeToken_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveCode___hyg_184_(lean_object*); lean_object* l_Std_RBNode_setBlack___rarg(lean_object*); lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_CodeToken_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveCode___hyg_184____boxed(lean_object*); -lean_object* l_Lean_Meta_withLocalDecl___at_Lean_mkNoConfusionEnum_mkToCtorIdx___spec__11___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_CodeToken_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveCode___hyg_184____closed__1; lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_InfoWithCtx_encode____x40_Lean_Widget_InteractiveCode___hyg_5____rarg___boxed(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Widget_formatExplicitInfos___closed__4; @@ -129,6 +128,7 @@ lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_ static lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_InfoWithCtx_decode____x40_Lean_Widget_InteractiveCode___hyg_5____rarg___closed__1; static lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_InfoWithCtx_encodeUnsafe____x40_Lean_Widget_InteractiveCode___hyg_5____rarg___closed__6; lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Widget_instInhabitedInfoWithCtx___closed__15; static lean_object* l_Lean_Widget_instInhabitedInfoWithCtx___closed__18; static lean_object* l_Lean_Widget_Lean_Widget_InfoWithCtx_instRpcEncodingWithRpcRefInfoWithCtxRpcRef___closed__1; @@ -1226,7 +1226,7 @@ x_36 = (uint8_t)((x_35 << 24) >> 61); x_37 = lean_alloc_closure((void*)(l_Lean_Widget_traverse_go___lambda__1), 8, 2); lean_closure_set(x_37, 0, x_34); lean_closure_set(x_37, 1, x_12); -x_38 = l_Lean_Meta_withLocalDecl___at_Lean_mkNoConfusionEnum_mkToCtorIdx___spec__11___rarg(x_32, x_36, x_33, x_37, x_4, x_5, x_6, x_7, x_8); +x_38 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1___rarg(x_32, x_36, x_33, x_37, x_4, x_5, x_6, x_7, x_8); return x_38; } case 7: @@ -1245,7 +1245,7 @@ x_43 = (uint8_t)((x_42 << 24) >> 61); x_44 = lean_alloc_closure((void*)(l_Lean_Widget_traverse_go___lambda__1), 8, 2); lean_closure_set(x_44, 0, x_41); lean_closure_set(x_44, 1, x_12); -x_45 = l_Lean_Meta_withLocalDecl___at_Lean_mkNoConfusionEnum_mkToCtorIdx___spec__11___rarg(x_39, x_43, x_40, x_44, x_4, x_5, x_6, x_7, x_8); +x_45 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_mkHCongrWithArity_withNewEqs_loop___spec__1___rarg(x_39, x_43, x_40, x_44, x_4, x_5, x_6, x_7, x_8); return x_45; } case 8: