max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-14 18:55:05 -07:00
parent 3fa54e604d
commit 34853bcbd8
19 changed files with 3596 additions and 613 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
stage0/src/Lean/Elab/Tactic/BuiltinTactic.lean generated
View file

@ -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

6
stage0/src/Lean/Expr.lean generated
View file

@ -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

1
stage0/src/Lean/Meta.lean generated
View file

@ -37,3 +37,4 @@ import Lean.Meta.GeneralizeVars
import Lean.Meta.Injective
import Lean.Meta.Structure
import Lean.Meta.Constructions
import Lean.Meta.CongrTheorems

113
stage0/src/Lean/Meta/CongrTheorems.lean generated Normal file
View file

@ -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

3
stage0/src/Lean/Meta/FunInfo.lean generated
View file

@ -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

10
stage0/src/Lean/Meta/Tactic/Cases.lean generated
View file

@ -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 ·)

2
stage0/src/library/compiler/llnf.cpp generated
View file

@ -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<unsigned> 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))));

1644
stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c generated
View file

File diff suppressed because it is too large Load diff

57
stage0/stdlib/Lean/Expr.c generated
View file

@ -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);

6
stage0/stdlib/Lean/Meta.c generated
View file

@ -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 <lean/lean.h>
#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

12
stage0/stdlib/Lean/Meta/Closure.c generated
View file

@ -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);

2279
stage0/stdlib/Lean/Meta/CongrTheorems.c generated Normal file
View file

File diff suppressed because it is too large Load diff

10
stage0/stdlib/Lean/Meta/ExprDefEq.c generated
View file

@ -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);

20
stage0/stdlib/Lean/Meta/FunInfo.c generated
View file

@ -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*);

6
stage0/stdlib/Lean/Meta/Tactic/Cases.c generated
View file

@ -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));

2
stage0/stdlib/Lean/Meta/Tactic/Simp/SimpLemmas.c generated
View file

@ -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);

10
stage0/stdlib/Lean/Meta/Transform.c generated
View file

@ -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);

14
stage0/stdlib/Lean/MetavarContext.c generated
View file

@ -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);

6
stage0/stdlib/Lean/Widget/InteractiveCode.c generated
View file

@ -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: