diff --git a/stage0/src/Lean/Compiler/ConstFolding.lean b/stage0/src/Lean/Compiler/ConstFolding.lean index f9e0623ac5..f60b246512 100644 --- a/stage0/src/Lean/Compiler/ConstFolding.lean +++ b/stage0/src/Lean/Compiler/ConstFolding.lean @@ -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 diff --git a/stage0/src/Lean/Delaborator.lean b/stage0/src/Lean/Delaborator.lean index 1c0cd012b7..0d6499c19d 100644 --- a/stage0/src/Lean/Delaborator.lean +++ b/stage0/src/Lean/Delaborator.lean @@ -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) diff --git a/stage0/src/Lean/Elab/BuiltinNotation.lean b/stage0/src/Lean/Elab/BuiltinNotation.lean index 289f140108..c4422a7c21 100644 --- a/stage0/src/Lean/Elab/BuiltinNotation.lean +++ b/stage0/src/Lean/Elab/BuiltinNotation.lean @@ -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 diff --git a/stage0/src/Lean/Meta/AppBuilder.lean b/stage0/src/Lean/Meta/AppBuilder.lean index b44c2e2965..3e7ed61ee4 100644 --- a/stage0/src/Lean/Meta/AppBuilder.lean +++ b/stage0/src/Lean/Meta/AppBuilder.lean @@ -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 := diff --git a/stage0/stdlib/Lean/Compiler/ConstFolding.c b/stage0/stdlib/Lean/Compiler/ConstFolding.c index 9e7caaddee..e2b15802b1 100644 --- a/stage0/stdlib/Lean/Compiler/ConstFolding.c +++ b/stage0/stdlib/Lean/Compiler/ConstFolding.c @@ -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(); diff --git a/stage0/stdlib/Lean/Delaborator.c b/stage0/stdlib/Lean/Delaborator.c index 813beeea5a..07e0f182a5 100644 --- a/stage0/stdlib/Lean/Delaborator.c +++ b/stage0/stdlib/Lean/Delaborator.c @@ -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); diff --git a/stage0/stdlib/Lean/Elab/BuiltinNotation.c b/stage0/stdlib/Lean/Elab/BuiltinNotation.c index baf5e183ff..120a5eba86 100644 --- a/stage0/stdlib/Lean/Elab/BuiltinNotation.c +++ b/stage0/stdlib/Lean/Elab/BuiltinNotation.c @@ -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(); diff --git a/stage0/stdlib/Lean/Meta/AppBuilder.c b/stage0/stdlib/Lean/Meta/AppBuilder.c index f3979d7f64..37498cf0b6 100644 --- a/stage0/stdlib/Lean/Meta/AppBuilder.c +++ b/stage0/stdlib/Lean/Meta/AppBuilder.c @@ -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(); diff --git a/stage0/stdlib/Lean/Meta/Match/CaseArraySizes.c b/stage0/stdlib/Lean/Meta/Match/CaseArraySizes.c index 1bcd439929..9b7a893b67 100644 --- a/stage0/stdlib/Lean/Meta/Match/CaseArraySizes.c +++ b/stage0/stdlib/Lean/Meta/Match/CaseArraySizes.c @@ -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; }