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 2020-11-10 09:54:56 -08:00
parent 2ef9199c56
commit cf0f4c04ed
9 changed files with 148 additions and 80 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
stage0/src/Lean/Compiler/ConstFolding.lean generated
View file

@ -96,10 +96,10 @@ def mkNatEq (a b : Expr) : Expr :=
mkAppN (mkConst `Eq [levelOne]) #[(mkConst `Nat), a, b]
def mkNatLt (a b : Expr) : Expr :=
mkAppN (mkConst `Less.Less [levelZero]) #[mkConst `Nat, mkConst `Nat.less, a, b]
mkAppN (mkConst `HasLess.Less [levelZero]) #[mkConst `Nat, mkConst `Nat.less, a, b]
def mkNatLe (a b : Expr) : Expr :=
mkAppN (mkConst `LessEq.LessEq [levelZero]) #[mkConst `Nat, mkConst `Nat.lessEq, a, b]
mkAppN (mkConst `HasLessEq.LessEq [levelZero]) #[mkConst `Nat, mkConst `Nat.lessEq, a, b]
def toDecidableExpr (beforeErasure : Bool) (pred : Expr) (r : Bool) : Expr :=
match beforeErasure, r with

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

@ -642,16 +642,16 @@ def delabPrefixOp (op : Bool → Syntax → Delab) : Delab := whenPPOption getPP
@[builtinDelab app.ModN.modn] def delabModN : Delab := delabInfixOp fun _ x y => `($x %ₙ $y)
@[builtinDelab app.Pow.pow] def delabPow : Delab := delabInfixOp fun _ x y => `($x ^ $y)
@[builtinDelab app.LessEq.LessEq] def delabLE : Delab := delabInfixOp fun b x y => cond b `($x ≤ $y) `($x <= $y)
@[builtinDelab app.HasLessEq.LessEq] def delabLE : Delab := delabInfixOp fun b x y => cond b `($x ≤ $y) `($x <= $y)
@[builtinDelab app.GreaterEq] def delabGE : Delab := delabInfixOp fun b x y => cond b `($x ≥ $y) `($x >= $y)
@[builtinDelab app.Less.Less] def delabLT : Delab := delabInfixOp fun _ x y => `($x < $y)
@[builtinDelab app.HasLess.Less] def delabLT : Delab := delabInfixOp fun _ x y => `($x < $y)
@[builtinDelab app.Greater] def delabGT : Delab := delabInfixOp fun _ x y => `($x > $y)
@[builtinDelab app.Eq] def delabEq : Delab := delabInfixOp fun _ x y => `($x = $y)
@[builtinDelab app.Ne] def delabNe : Delab := delabInfixOp fun _ x y => `($x ≠ $y)
@[builtinDelab app.BEq.beq] def delabBEq : Delab := delabInfixOp fun _ x y => `($x == $y)
@[builtinDelab app.bne] def delabBNe : Delab := delabInfixOp fun _ x y => `($x != $y)
@[builtinDelab app.HEq] def delabHEq : Delab := delabInfixOp fun b x y => cond b `($x ≅ $y) `($x ~= $y)
@[builtinDelab app.Equiv.Equiv] def delabEquiv : Delab := delabInfixOp fun _ x y => `($x ≈ $y)
@[builtinDelab app.HasEquiv.Equiv] def delabEquiv : Delab := delabInfixOp fun _ x y => `($x ≈ $y)
@[builtinDelab app.And] def delabAnd : Delab := delabInfixOp fun b x y => cond b `($x ∧ $y) `($x /\ $y)
@[builtinDelab app.Or] def delabOr : Delab := delabInfixOp fun b x y => cond b `($x ∨ $y) `($x || $y)

6
stage0/src/Lean/Elab/BuiltinNotation.lean generated
View file

@ -207,16 +207,16 @@ def expandPrefixOp (op : Name) : Macro := fun stx => do
@[builtinMacro Lean.Parser.Term.modN] def expandModN : Macro := expandInfixOp `ModN.modn
@[builtinMacro Lean.Parser.Term.pow] def expandPow : Macro := expandInfixOp `Pow.pow
@[builtinMacro Lean.Parser.Term.le] def expandLE : Macro := expandInfixOp `LessEq.LessEq
@[builtinMacro Lean.Parser.Term.le] def expandLE : Macro := expandInfixOp `HasLessEq.LessEq
@[builtinMacro Lean.Parser.Term.ge] def expandGE : Macro := expandInfixOp `GreaterEq
@[builtinMacro Lean.Parser.Term.lt] def expandLT : Macro := expandInfixOp `Less.Less
@[builtinMacro Lean.Parser.Term.lt] def expandLT : Macro := expandInfixOp `HasLess.Less
@[builtinMacro Lean.Parser.Term.gt] def expandGT : Macro := expandInfixOp `Greater
@[builtinMacro Lean.Parser.Term.eq] def expandEq : Macro := expandInfixOp `Eq
@[builtinMacro Lean.Parser.Term.ne] def expandNe : Macro := expandInfixOp `Ne
@[builtinMacro Lean.Parser.Term.beq] def expandBEq : Macro := expandInfixOp `BEq.beq
@[builtinMacro Lean.Parser.Term.bne] def expandBNe : Macro := expandInfixOp `bne
@[builtinMacro Lean.Parser.Term.heq] def expandHEq : Macro := expandInfixOp `HEq
@[builtinMacro Lean.Parser.Term.equiv] def expandEquiv : Macro := expandInfixOp `Equiv.Equiv
@[builtinMacro Lean.Parser.Term.equiv] def expandEquiv : Macro := expandInfixOp `HasEquiv.Equiv
@[builtinMacro Lean.Parser.Term.and] def expandAnd : Macro := expandInfixOp `And
@[builtinMacro Lean.Parser.Term.or] def expandOr : Macro := expandInfixOp `Or

4
stage0/src/Lean/Meta/AppBuilder.lean generated
View file

@ -410,11 +410,11 @@ def mkDecideProof (p : Expr) : m Expr := liftMetaM do
/-- Return `a < b` -/
def mkLt (a b : Expr) : m Expr :=
mkAppM `Less.Less #[a, b]
mkAppM `HasLess.Less #[a, b]
/-- Return `a <= b` -/
def mkLe (a b : Expr) : m Expr :=
mkAppM `LessEq.LessEq #[a, b]
mkAppM `HasLessEq.LessEq #[a, b]
/-- Return `arbitrary α` -/
def mkArbitrary (α : Expr) : m Expr :=

118
stage0/stdlib/Lean/Compiler/ConstFolding.c generated
View file

@ -101,6 +101,7 @@ lean_object* l_Lean_Compiler_foldNatDecLe___boxed(lean_object*, lean_object*, le
lean_object* l_Lean_Compiler_foldNatDiv(uint8_t);
extern lean_object* l_Lean_levelZero;
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_mkNatLe___closed__9;
lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__19;
lean_object* l_Lean_Compiler_mkUInt32Lit(lean_object*);
lean_object* l_Lean_Compiler_numScalarTypes___closed__17;
@ -305,6 +306,7 @@ extern lean_object* l_Nat_Init_Data_Nat_Basic___instance__5___closed__1;
lean_object* l_Lean_Compiler_mkUInt32Lit___boxed(lean_object*);
lean_object* l_List_foldr___at_Lean_Compiler_isToNat___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_foldNatDecEq___closed__1;
lean_object* l_Lean_Compiler_mkNatLt___closed__11;
lean_object* l_Lean_Compiler_foldBinUInt(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_foldUIntAdd(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_foldBinOp_match__1(lean_object*);
@ -2358,7 +2360,7 @@ static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Less");
x_1 = lean_mk_string("HasLess");
return x_1;
}
}
@ -2375,14 +2377,22 @@ return x_3;
static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Less");
return x_1;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_mkNatLt___closed__2;
x_2 = l_Lean_Compiler_mkNatLt___closed__1;
x_2 = l_Lean_Compiler_mkNatLt___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__4() {
static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -2394,17 +2404,17 @@ lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__5() {
static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_mkNatLt___closed__3;
x_2 = l_Lean_Compiler_mkNatLt___closed__4;
x_1 = l_Lean_Compiler_mkNatLt___closed__4;
x_2 = l_Lean_Compiler_mkNatLt___closed__5;
x_3 = l_Lean_mkConst(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__6() {
static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__7() {
_start:
{
lean_object* x_1;
@ -2412,23 +2422,13 @@ x_1 = lean_mk_string("less");
return x_1;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Literal_type___closed__2;
x_2 = l_Lean_Compiler_mkNatLt___closed__6;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_1 = l_Lean_Literal_type___closed__2;
x_2 = l_Lean_Compiler_mkNatLt___closed__7;
x_3 = l_Lean_mkConst(x_2, x_1);
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
@ -2436,18 +2436,28 @@ static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_mkNatLt___closed__8;
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_PersistentHashMap_mkCollisionNode___rarg___closed__1;
x_2 = l_Lean_Compiler_mkNatEq___closed__5;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__10() {
static lean_object* _init_l_Lean_Compiler_mkNatLt___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_mkNatLt___closed__9;
x_2 = l_Lean_Compiler_mkNatLt___closed__8;
x_1 = l_Lean_Compiler_mkNatLt___closed__10;
x_2 = l_Lean_Compiler_mkNatLt___closed__9;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
@ -2456,10 +2466,10 @@ lean_object* l_Lean_Compiler_mkNatLt(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = l_Lean_Compiler_mkNatLt___closed__10;
x_3 = l_Lean_Compiler_mkNatLt___closed__11;
x_4 = lean_array_push(x_3, x_1);
x_5 = lean_array_push(x_4, x_2);
x_6 = l_Lean_Compiler_mkNatLt___closed__5;
x_6 = l_Lean_Compiler_mkNatLt___closed__6;
x_7 = l_Lean_mkAppN(x_6, x_5);
lean_dec(x_5);
return x_7;
@ -2469,7 +2479,7 @@ static lean_object* _init_l_Lean_Compiler_mkNatLe___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("LessEq");
x_1 = lean_mk_string("HasLessEq");
return x_1;
}
}
@ -2486,48 +2496,46 @@ return x_3;
static lean_object* _init_l_Lean_Compiler_mkNatLe___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_mkNatLe___closed__2;
x_2 = l_Lean_Compiler_mkNatLe___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
lean_object* x_1;
x_1 = lean_mk_string("LessEq");
return x_1;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLe___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_mkNatLe___closed__3;
x_2 = l_Lean_Compiler_mkNatLt___closed__4;
x_3 = l_Lean_mkConst(x_1, x_2);
x_1 = l_Lean_Compiler_mkNatLe___closed__2;
x_2 = l_Lean_Compiler_mkNatLe___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLe___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_mkNatLe___closed__4;
x_2 = l_Lean_Compiler_mkNatLt___closed__5;
x_3 = l_Lean_mkConst(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLe___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lessEq");
return x_1;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLe___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Literal_type___closed__2;
x_2 = l_Lean_Compiler_mkNatLe___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLe___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_1 = l_Lean_Literal_type___closed__2;
x_2 = l_Lean_Compiler_mkNatLe___closed__6;
x_3 = l_Lean_mkConst(x_2, x_1);
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
@ -2535,8 +2543,18 @@ static lean_object* _init_l_Lean_Compiler_mkNatLe___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_mkNatLt___closed__9;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_mkNatLe___closed__7;
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Compiler_mkNatLe___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_mkNatLt___closed__10;
x_2 = l_Lean_Compiler_mkNatLe___closed__8;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
@ -2545,10 +2563,10 @@ lean_object* l_Lean_Compiler_mkNatLe(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = l_Lean_Compiler_mkNatLe___closed__8;
x_3 = l_Lean_Compiler_mkNatLe___closed__9;
x_4 = lean_array_push(x_3, x_1);
x_5 = lean_array_push(x_4, x_2);
x_6 = l_Lean_Compiler_mkNatLe___closed__4;
x_6 = l_Lean_Compiler_mkNatLe___closed__5;
x_7 = l_Lean_mkAppN(x_6, x_5);
lean_dec(x_5);
return x_7;
@ -5308,6 +5326,8 @@ l_Lean_Compiler_mkNatLt___closed__9 = _init_l_Lean_Compiler_mkNatLt___closed__9(
lean_mark_persistent(l_Lean_Compiler_mkNatLt___closed__9);
l_Lean_Compiler_mkNatLt___closed__10 = _init_l_Lean_Compiler_mkNatLt___closed__10();
lean_mark_persistent(l_Lean_Compiler_mkNatLt___closed__10);
l_Lean_Compiler_mkNatLt___closed__11 = _init_l_Lean_Compiler_mkNatLt___closed__11();
lean_mark_persistent(l_Lean_Compiler_mkNatLt___closed__11);
l_Lean_Compiler_mkNatLe___closed__1 = _init_l_Lean_Compiler_mkNatLe___closed__1();
lean_mark_persistent(l_Lean_Compiler_mkNatLe___closed__1);
l_Lean_Compiler_mkNatLe___closed__2 = _init_l_Lean_Compiler_mkNatLe___closed__2();
@ -5324,6 +5344,8 @@ l_Lean_Compiler_mkNatLe___closed__7 = _init_l_Lean_Compiler_mkNatLe___closed__7(
lean_mark_persistent(l_Lean_Compiler_mkNatLe___closed__7);
l_Lean_Compiler_mkNatLe___closed__8 = _init_l_Lean_Compiler_mkNatLe___closed__8();
lean_mark_persistent(l_Lean_Compiler_mkNatLe___closed__8);
l_Lean_Compiler_mkNatLe___closed__9 = _init_l_Lean_Compiler_mkNatLe___closed__9();
lean_mark_persistent(l_Lean_Compiler_mkNatLe___closed__9);
l_Lean_Compiler_toDecidableExpr___closed__1 = _init_l_Lean_Compiler_toDecidableExpr___closed__1();
lean_mark_persistent(l_Lean_Compiler_toDecidableExpr___closed__1);
l_Lean_Compiler_toDecidableExpr___closed__2 = _init_l_Lean_Compiler_toDecidableExpr___closed__2();

27
stage0/stdlib/Lean/Delaborator.c generated
View file

@ -896,6 +896,7 @@ lean_object* l_Lean_Delaborator_delabAppExplicit___lambda__2___closed__2;
lean_object* lean_panic_fn(lean_object*, lean_object*);
extern lean_object* l_Lean_setOptionFromString___closed__1;
lean_object* l_Lean_getPPUniverses___closed__2;
lean_object* l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5;
lean_object* l_Lean_Delaborator_delabLT___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg___closed__1;
extern lean_object* l_Lean_getSanitizeNames___closed__1;
@ -1104,6 +1105,7 @@ lean_object* l_Lean_Delaborator_delabBEq___lambda__1(uint8_t, lean_object*, lean
lean_object* l_Lean_Delaborator_delabEquiv___lambda__1___closed__1;
lean_object* l_Lean_Delaborator_delabLam___lambda__3___closed__3;
lean_object* l___regBuiltin_Lean_Delaborator_delabseqRight___closed__3;
extern lean_object* l_Lean_Meta_mkLe___rarg___closed__3;
extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_955____closed__16;
lean_object* l_Lean_Delaborator_delabAppend___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Delaborator_delabGE___lambda__1___closed__4;
@ -1151,6 +1153,7 @@ lean_object* l_Array_foldrMUnsafe_fold___at_Lean_Delaborator_delabForall___spec_
lean_object* l_Lean_Delaborator_delabMapRev(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Delaborator_delabNe___lambda__1___closed__3;
lean_object* l_Lean_Delaborator_delabBNot(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_mkLt___rarg___closed__3;
uint8_t l_Lean_getPPAll(lean_object*);
lean_object* l_Lean_Delaborator_getExprKind___closed__3;
lean_object* l_Lean_Level_quote___closed__1;
@ -26862,7 +26865,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Delaborator_delabLE___closed__1;
x_2 = l_Lean_Meta_mkLe___rarg___closed__1;
x_2 = l_Lean_Meta_mkLe___rarg___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -27156,7 +27159,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Delaborator_delabLT___closed__1;
x_2 = l_Lean_Meta_mkLt___rarg___closed__1;
x_2 = l_Lean_Meta_mkLt___rarg___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -28039,7 +28042,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__1
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Equiv");
x_1 = lean_mk_string("HasEquiv");
return x_1;
}
}
@ -28056,14 +28059,22 @@ return x_3;
static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Equiv");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__2;
x_2 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__1;
x_2 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4() {
static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5() {
_start:
{
lean_object* x_1;
@ -28076,8 +28087,8 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Delaborator_delabAttribute;
x_3 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3;
x_4 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4;
x_3 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4;
x_4 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
@ -31603,6 +31614,8 @@ l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3 = _init_l___regBuiltin_Le
lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3);
l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4();
lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4);
l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5 = _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5();
lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5);
res = l___regBuiltin_Lean_Delaborator_delabEquiv(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

25
stage0/stdlib/Lean/Elab/BuiltinNotation.c generated
View file

@ -16,6 +16,7 @@ extern "C" {
extern lean_object* l_myMacro____x40_Init_Data_ToString_Macro___hyg_39____lambda__2___closed__3;
lean_object* l_Lean_Elab_Term_expandOrM___closed__2;
lean_object* l_Lean_Elab_Term_expandDbgTrace___closed__9;
extern lean_object* l_Lean_Meta_mkLe___rarg___closed__4;
lean_object* l_Lean_mkCIdentFrom(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__26;
lean_object* l_Lean_Elab_Term_expandNot___closed__1;
@ -333,6 +334,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_expandHave___closed__1;
lean_object* l_Lean_Elab_Term_elabNativeDecide(lean_object*);
lean_object* l_Lean_Elab_Term_expandDbgTrace___closed__6;
extern lean_object* l_Lean_numLitKind;
lean_object* l_Lean_Elab_Term_expandEquiv___closed__4;
lean_object* l_Lean_Elab_Term_elabNativeRefl___lambda__1___closed__2;
lean_object* l_Lean_Elab_Term_elabNativeRefl___closed__1;
lean_object* l_Lean_Elab_Term_expandAppend___closed__3;
@ -513,6 +515,7 @@ lean_object* l_Lean_Elab_Term_elabNativeRefl___lambda__1___closed__8;
lean_object* l___regBuiltin_Lean_Elab_Term_expandBOr___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_expandAnd___closed__3;
uint8_t l_Lean_Expr_isConstOf(lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_mkLt___rarg___closed__4;
lean_object* l_Lean_Elab_Term_elabStateRefT___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_elabPanic___closed__2;
lean_object* l_Lean_Elab_Term_expandAssert___closed__13;
@ -848,7 +851,6 @@ lean_object* l_Lean_Meta_mkArrow___at_Lean_Elab_Term_elabStateRefT___spec__1(lea
lean_object* l___regBuiltin_Lean_Elab_Term_expandBEq(lean_object*);
lean_object* l_Lean_Elab_Term_expandSeqLeft___closed__4;
lean_object* l_Lean_Elab_Term_expandSeq___closed__4;
extern lean_object* l_Lean_Meta_mkLe___rarg___closed__3;
extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_955____closed__16;
lean_object* l_Lean_Elab_Term_expandMapRev___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandAssert___closed__9;
@ -886,7 +888,6 @@ lean_object* l_Lean_Elab_Term_expandAnd(lean_object*, lean_object*, lean_object*
lean_object* l_Lean_Elab_Term_expandSeqRight___closed__4;
lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__1;
lean_object* l_Lean_Elab_Term_expandAssert___closed__17;
extern lean_object* l_Lean_Meta_mkLt___rarg___closed__3;
uint8_t l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_hasCDot(lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabSubst___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -9111,7 +9112,7 @@ lean_object* l_Lean_Elab_Term_expandLE(lean_object* x_1, lean_object* x_2, lean_
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = l_Lean_Meta_mkLe___rarg___closed__3;
x_4 = l_Lean_Meta_mkLe___rarg___closed__4;
x_5 = l_Lean_Elab_Term_expandInfixOp(x_4, x_1, x_2, x_3);
return x_5;
}
@ -9241,7 +9242,7 @@ lean_object* l_Lean_Elab_Term_expandLT(lean_object* x_1, lean_object* x_2, lean_
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = l_Lean_Meta_mkLt___rarg___closed__3;
x_4 = l_Lean_Meta_mkLt___rarg___closed__4;
x_5 = l_Lean_Elab_Term_expandInfixOp(x_4, x_1, x_2, x_3);
return x_5;
}
@ -9671,7 +9672,7 @@ static lean_object* _init_l_Lean_Elab_Term_expandEquiv___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Equiv");
x_1 = lean_mk_string("HasEquiv");
return x_1;
}
}
@ -9688,9 +9689,17 @@ return x_3;
static lean_object* _init_l_Lean_Elab_Term_expandEquiv___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Equiv");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_expandEquiv___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_expandEquiv___closed__2;
x_2 = l_Lean_Elab_Term_expandEquiv___closed__1;
x_2 = l_Lean_Elab_Term_expandEquiv___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -9699,7 +9708,7 @@ lean_object* l_Lean_Elab_Term_expandEquiv(lean_object* x_1, lean_object* x_2, le
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = l_Lean_Elab_Term_expandEquiv___closed__3;
x_4 = l_Lean_Elab_Term_expandEquiv___closed__4;
x_5 = l_Lean_Elab_Term_expandInfixOp(x_4, x_1, x_2, x_3);
return x_5;
}
@ -17906,6 +17915,8 @@ l_Lean_Elab_Term_expandEquiv___closed__2 = _init_l_Lean_Elab_Term_expandEquiv___
lean_mark_persistent(l_Lean_Elab_Term_expandEquiv___closed__2);
l_Lean_Elab_Term_expandEquiv___closed__3 = _init_l_Lean_Elab_Term_expandEquiv___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_expandEquiv___closed__3);
l_Lean_Elab_Term_expandEquiv___closed__4 = _init_l_Lean_Elab_Term_expandEquiv___closed__4();
lean_mark_persistent(l_Lean_Elab_Term_expandEquiv___closed__4);
l___regBuiltin_Lean_Elab_Term_expandEquiv___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_expandEquiv___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_expandEquiv___closed__1);
l___regBuiltin_Lean_Elab_Term_expandEquiv___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_expandEquiv___closed__2();

34
stage0/stdlib/Lean/Meta/AppBuilder.c generated
View file

@ -15,6 +15,7 @@ extern "C" {
#endif
lean_object* l_Lean_Meta_mkAppOptM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppMArgs_loop___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_mkLe___rarg___closed__4;
extern lean_object* l___private_Init_LeanInit_0__Lean_quoteList___rarg___closed__4;
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_throwAppBuilderException___rarg___closed__3;
extern lean_object* l_Lean_mkRecName___closed__1;
@ -264,6 +265,7 @@ lean_object* l_Lean_Meta_mkArrayLit___rarg(lean_object*, lean_object*, lean_obje
lean_object* l_Lean_Meta_mkHEqTrans___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppMFinal___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkLt___rarg___closed__4;
lean_object* l_Lean_mkLambda(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_getLevelImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkId___rarg(lean_object*, lean_object*);
@ -13051,7 +13053,7 @@ static lean_object* _init_l_Lean_Meta_mkLt___rarg___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Less");
x_1 = lean_mk_string("HasLess");
return x_1;
}
}
@ -13068,9 +13070,17 @@ return x_3;
static lean_object* _init_l_Lean_Meta_mkLt___rarg___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Less");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_mkLt___rarg___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_mkLt___rarg___closed__2;
x_2 = l_Lean_Meta_mkLt___rarg___closed__1;
x_2 = l_Lean_Meta_mkLt___rarg___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -13082,7 +13092,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj
x_4 = l_Lean_mkAppStx___closed__9;
x_5 = lean_array_push(x_4, x_2);
x_6 = lean_array_push(x_5, x_3);
x_7 = l_Lean_Meta_mkLt___rarg___closed__3;
x_7 = l_Lean_Meta_mkLt___rarg___closed__4;
x_8 = l_Lean_Meta_mkAppM___rarg(x_1, x_7, x_6);
return x_8;
}
@ -13099,7 +13109,7 @@ static lean_object* _init_l_Lean_Meta_mkLe___rarg___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("LessEq");
x_1 = lean_mk_string("HasLessEq");
return x_1;
}
}
@ -13116,9 +13126,17 @@ return x_3;
static lean_object* _init_l_Lean_Meta_mkLe___rarg___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("LessEq");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_mkLe___rarg___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_mkLe___rarg___closed__2;
x_2 = l_Lean_Meta_mkLe___rarg___closed__1;
x_2 = l_Lean_Meta_mkLe___rarg___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -13130,7 +13148,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj
x_4 = l_Lean_mkAppStx___closed__9;
x_5 = lean_array_push(x_4, x_2);
x_6 = lean_array_push(x_5, x_3);
x_7 = l_Lean_Meta_mkLe___rarg___closed__3;
x_7 = l_Lean_Meta_mkLe___rarg___closed__4;
x_8 = l_Lean_Meta_mkAppM___rarg(x_1, x_7, x_6);
return x_8;
}
@ -13446,12 +13464,16 @@ l_Lean_Meta_mkLt___rarg___closed__2 = _init_l_Lean_Meta_mkLt___rarg___closed__2(
lean_mark_persistent(l_Lean_Meta_mkLt___rarg___closed__2);
l_Lean_Meta_mkLt___rarg___closed__3 = _init_l_Lean_Meta_mkLt___rarg___closed__3();
lean_mark_persistent(l_Lean_Meta_mkLt___rarg___closed__3);
l_Lean_Meta_mkLt___rarg___closed__4 = _init_l_Lean_Meta_mkLt___rarg___closed__4();
lean_mark_persistent(l_Lean_Meta_mkLt___rarg___closed__4);
l_Lean_Meta_mkLe___rarg___closed__1 = _init_l_Lean_Meta_mkLe___rarg___closed__1();
lean_mark_persistent(l_Lean_Meta_mkLe___rarg___closed__1);
l_Lean_Meta_mkLe___rarg___closed__2 = _init_l_Lean_Meta_mkLe___rarg___closed__2();
lean_mark_persistent(l_Lean_Meta_mkLe___rarg___closed__2);
l_Lean_Meta_mkLe___rarg___closed__3 = _init_l_Lean_Meta_mkLe___rarg___closed__3();
lean_mark_persistent(l_Lean_Meta_mkLe___rarg___closed__3);
l_Lean_Meta_mkLe___rarg___closed__4 = _init_l_Lean_Meta_mkLe___rarg___closed__4();
lean_mark_persistent(l_Lean_Meta_mkLe___rarg___closed__4);
l_Lean_Meta_mkArbitrary___rarg___closed__1 = _init_l_Lean_Meta_mkArbitrary___rarg___closed__1();
lean_mark_persistent(l_Lean_Meta_mkArbitrary___rarg___closed__1);
l_Lean_Meta_mkArbitrary___rarg___closed__2 = _init_l_Lean_Meta_mkArbitrary___rarg___closed__2();

4
stage0/stdlib/Lean/Meta/Match/CaseArraySizes.c generated
View file

@ -79,6 +79,7 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_caseArraySizes___spec__1(size
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isAppOfArity(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Init_LeanInit___instance__1;
extern lean_object* l_Lean_Meta_mkLt___rarg___closed__4;
lean_object* l_Lean_Meta_introNCore(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_mkArrayGetLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_caseArraySizes_match__2___rarg(lean_object*, lean_object*);
@ -120,7 +121,6 @@ lean_object* l_Lean_mkNatLit(lean_object*);
lean_object* l_Lean_Meta_mkFreshExprSyntheticOpaqueMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapIdxM_map___at_Lean_Meta_caseArraySizes___spec__3___boxed(lean_object**);
extern lean_object* l_Lean_Meta_mkLt___rarg___closed__3;
lean_object* l_Lean_indentExpr(lean_object*);
lean_object* l_Lean_Meta_mkEqSymm___at_Lean_Meta_substCore___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
@ -371,7 +371,7 @@ lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_o
x_8 = l_Lean_mkAppStx___closed__9;
x_9 = lean_array_push(x_8, x_1);
x_10 = lean_array_push(x_9, x_2);
x_11 = l_Lean_Meta_mkLt___rarg___closed__3;
x_11 = l_Lean_Meta_mkLt___rarg___closed__4;
x_12 = l_Lean_Meta_mkAppM___at_Lean_Meta_mkDecideProof___spec__6(x_11, x_10, x_3, x_4, x_5, x_6, x_7);
return x_12;
}