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-06 07:28:10 -07:00
parent fa29428934
commit 5ce97286bb
7 changed files with 1444 additions and 1119 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -77,7 +77,8 @@ abbrev MData.empty : MData := {}
hasLevelParam : 1-bit
nonDepLet : 1-bit
binderInfo : 3-bits
looseBVarRange : 24-bits -/
approxDepth : 8-bits -- the approximate depth is used to minimize the number of hash collisions
looseBVarRange : 16-bits -/
def Expr.Data := UInt64
instance: Inhabited Expr.Data :=
@ -89,8 +90,11 @@ def Expr.Data.hash (c : Expr.Data) : UInt64 :=
instance : BEq Expr.Data where
beq (a b : UInt64) := a == b
def Expr.Data.approxDepth (c : Expr.Data) : UInt8 :=
((c.shiftRight 40).land 255).toUInt8
def Expr.Data.looseBVarRange (c : Expr.Data) : UInt32 :=
(c.shiftRight 40).toUInt32
(c.shiftRight 48).toUInt32
def Expr.Data.hasFVar (c : Expr.Data) : Bool :=
((c.shiftRight 32).land 1) == 1
@ -125,7 +129,7 @@ def BinderInfo.toUInt64 : BinderInfo → UInt64
| BinderInfo.auxDecl => 4
@[inline] private def Expr.mkDataCore
(h : UInt64) (looseBVarRange : Nat)
(h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8)
(hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) (bi : BinderInfo)
: Expr.Data :=
if looseBVarRange > Nat.pow 2 24 - 1 then panic! "bound variable index is too big"
@ -138,17 +142,18 @@ def BinderInfo.toUInt64 : BinderInfo → UInt64
hasLevelParam.toUInt64.shiftLeft 35 +
nonDepLet.toUInt64.shiftLeft 36 +
bi.toUInt64.shiftLeft 37 +
looseBVarRange.toUInt64.shiftLeft 40
approxDepth.toUInt64.shiftLeft 40 +
looseBVarRange.toUInt64.shiftLeft 48
r
def Expr.mkData (h : UInt64) (looseBVarRange : Nat := 0) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) : Expr.Data :=
Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam false BinderInfo.default
def Expr.mkData (h : UInt64) (looseBVarRange : Nat := 0) (approxDepth : UInt8 := 0) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) : Expr.Data :=
Expr.mkDataCore h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam false BinderInfo.default
def Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) (bi : BinderInfo) : Expr.Data :=
Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam false bi
def Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) (bi : BinderInfo) : Expr.Data :=
Expr.mkDataCore h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam false bi
def Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) : Expr.Data :=
Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet BinderInfo.default
def Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8) (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) : Expr.Data :=
Expr.mkDataCore h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet BinderInfo.default
open Expr
@ -223,6 +228,9 @@ def hasMVar (e : Expr) : Bool :=
def hasLevelParam (e : Expr) : Bool :=
e.data.hasLevelParam
def approxDepth (e : Expr) : UInt8 :=
e.data.approxDepth
def looseBVarRange (e : Expr) : Nat :=
e.data.looseBVarRange.toNat
@ -241,7 +249,7 @@ def binderInfo (e : Expr) : BinderInfo :=
end Expr
def mkConst (n : Name) (lvls : List Level := []) : Expr :=
Expr.const n lvls $ mkData (mixHash 5 $ mixHash (hash n) (hash lvls)) 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam)
Expr.const n lvls $ mkData (mixHash 5 $ mixHash (hash n) (hash lvls)) 0 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam)
def Literal.type : Literal → Expr
| Literal.natVal _ => mkConst `Nat
@ -254,24 +262,25 @@ def mkBVar (idx : Nat) : Expr :=
Expr.bvar idx $ mkData (mixHash 7 $ hash idx) (idx+1)
def mkSort (lvl : Level) : Expr :=
Expr.sort lvl $ mkData (mixHash 11 $ hash lvl) 0 false false lvl.hasMVar lvl.hasParam
Expr.sort lvl $ mkData (mixHash 11 $ hash lvl) 0 0 false false lvl.hasMVar lvl.hasParam
def mkFVar (fvarId : FVarId) : Expr :=
Expr.fvar fvarId $ mkData (mixHash 13 $ hash fvarId) 0 true
Expr.fvar fvarId $ mkData (mixHash 13 $ hash fvarId) 0 0 true
def mkMVar (fvarId : MVarId) : Expr :=
Expr.mvar fvarId $ mkData (mixHash 17 $ hash fvarId) 0 false true
Expr.mvar fvarId $ mkData (mixHash 17 $ hash fvarId) 0 0 false true
def mkMData (d : MData) (e : Expr) : Expr :=
Expr.mdata d e $ mkData (mixHash 19 $ hash e) e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
Expr.mdata d e $ mkData (mixHash 19 $ hash e) e.looseBVarRange (e.approxDepth+1) e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
def mkProj (s : Name) (i : Nat) (e : Expr) : Expr :=
Expr.proj s i e $ mkData (mixHash 23 $ mixHash (hash s) $ mixHash (hash i) (hash e))
e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
e.looseBVarRange (e.approxDepth+1) e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
def mkApp (f a : Expr) : Expr :=
Expr.app f a $ mkData (mixHash 29 $ mixHash (hash f) (hash a))
(Nat.max f.looseBVarRange a.looseBVarRange)
(max f.looseBVarRange a.looseBVarRange)
((max f.approxDepth a.approxDepth) + 1)
(f.hasFVar || a.hasFVar)
(f.hasExprMVar || a.hasExprMVar)
(f.hasLevelMVar || a.hasLevelMVar)
@ -280,7 +289,8 @@ def mkApp (f a : Expr) : Expr :=
def mkLambda (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr :=
-- let x := x.eraseMacroScopes
Expr.lam x t b $ mkDataForBinder (mixHash 31 $ mixHash (hash t) (hash b))
(Nat.max t.looseBVarRange (b.looseBVarRange - 1))
(max t.looseBVarRange (b.looseBVarRange - 1))
((max t.approxDepth b.approxDepth) + 1)
(t.hasFVar || b.hasFVar)
(t.hasExprMVar || b.hasExprMVar)
(t.hasLevelMVar || b.hasLevelMVar)
@ -290,7 +300,8 @@ def mkLambda (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr :=
def mkForall (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr :=
-- let x := x.eraseMacroScopes
Expr.forallE x t b $ mkDataForBinder (mixHash 37 $ mixHash (hash t) (hash b))
(Nat.max t.looseBVarRange (b.looseBVarRange - 1))
(max t.looseBVarRange (b.looseBVarRange - 1))
((max t.approxDepth b.approxDepth) + 1)
(t.hasFVar || b.hasFVar)
(t.hasExprMVar || b.hasExprMVar)
(t.hasLevelMVar || b.hasLevelMVar)
@ -308,7 +319,8 @@ def mkSimpleThunk (type : Expr) : Expr :=
def mkLet (x : Name) (t : Expr) (v : Expr) (b : Expr) (nonDep : Bool := false) : Expr :=
-- let x := x.eraseMacroScopes
Expr.letE x t v b $ mkDataForLet (mixHash 41 $ mixHash (hash t) $ mixHash (hash v) (hash b))
(Nat.max (Nat.max t.looseBVarRange v.looseBVarRange) (b.looseBVarRange - 1))
(max (max t.looseBVarRange v.looseBVarRange) (b.looseBVarRange - 1))
((max (max t.approxDepth v.approxDepth) b.approxDepth) + 1)
(t.hasFVar || v.hasFVar || b.hasFVar)
(t.hasExprMVar || v.hasExprMVar || b.hasExprMVar)
(t.hasLevelMVar || v.hasLevelMVar || b.hasLevelMVar)

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

File diff suppressed because it is too large Load diff

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

@ -4154,7 +4154,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(906u);
x_3 = lean_unsigned_to_nat(918u);
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);
@ -4183,7 +4183,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(911u);
x_3 = lean_unsigned_to_nat(923u);
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);
@ -4212,7 +4212,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(871u);
x_3 = lean_unsigned_to_nat(883u);
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);
@ -4241,7 +4241,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(939u);
x_3 = lean_unsigned_to_nat(951u);
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);
@ -4270,7 +4270,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(925u);
x_3 = lean_unsigned_to_nat(937u);
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);
@ -4299,7 +4299,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(948u);
x_3 = lean_unsigned_to_nat(960u);
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);

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

@ -14778,7 +14778,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(906u);
x_3 = lean_unsigned_to_nat(918u);
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);
@ -14807,7 +14807,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(911u);
x_3 = lean_unsigned_to_nat(923u);
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);
@ -14836,7 +14836,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(939u);
x_3 = lean_unsigned_to_nat(951u);
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);
@ -14865,7 +14865,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(925u);
x_3 = lean_unsigned_to_nat(937u);
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);
@ -14894,7 +14894,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(948u);
x_3 = lean_unsigned_to_nat(960u);
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);

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

@ -11126,7 +11126,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(880u);
x_3 = lean_unsigned_to_nat(892u);
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

@ -870,7 +870,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(939u);
x_3 = lean_unsigned_to_nat(951u);
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);
@ -977,7 +977,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(925u);
x_3 = lean_unsigned_to_nat(937u);
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);
@ -1084,7 +1084,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(948u);
x_3 = lean_unsigned_to_nat(960u);
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);
@ -1222,7 +1222,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(906u);
x_3 = lean_unsigned_to_nat(918u);
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);
@ -1296,7 +1296,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(911u);
x_3 = lean_unsigned_to_nat(923u);
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

@ -11543,7 +11543,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(889u);
x_3 = lean_unsigned_to_nat(901u);
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);
@ -11626,7 +11626,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(880u);
x_3 = lean_unsigned_to_nat(892u);
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);
@ -11712,7 +11712,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(939u);
x_3 = lean_unsigned_to_nat(951u);
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);
@ -11819,7 +11819,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(925u);
x_3 = lean_unsigned_to_nat(937u);
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);
@ -11926,7 +11926,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(948u);
x_3 = lean_unsigned_to_nat(960u);
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);
@ -12060,7 +12060,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(906u);
x_3 = lean_unsigned_to_nat(918u);
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);
@ -12146,7 +12146,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(911u);
x_3 = lean_unsigned_to_nat(923u);
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);