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-14 08:36:57 -08:00
parent 17fb995348
commit 1a8dafccc5
10 changed files with 491 additions and 225 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
stage0/src/Init/NotationExtra.lean generated
View file

@ -60,8 +60,9 @@ end Lean
open Lean
macro "∃" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Exists xs b
macro "Σ" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Sigma xs b
macro "∃" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Exists xs b
macro "exists" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Exists xs b
macro "Σ" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Sigma xs b
macro "Σ'" xs:explicitBinders ", " b:term : term => expandExplicitBinders `PSigma xs b
macro:25 xs:bracketedExplicitBinders "×" b:term : term => expandBrackedBinders `Sigma xs b
macro:25 xs:bracketedExplicitBinders "×'" b:term : term => expandBrackedBinders `PSigma xs b

13
stage0/src/Lean/Level.lean generated
View file

@ -418,14 +418,14 @@ instance : ToString Level := ⟨Format.pretty ∘ Level.format⟩
end Level
/- Similar to `mkLevelMax`, but applies cheap simplifications -/
@[export lean_level_mk_max_simp]
def mkLevelMax' (u v : Level) : Level :=
let subsumes (u v : Level) : Bool :=
match u with
| Level.max u₁ u₂ _ => v == u₁ || v == u₂
| _ => false
if u.isExplicit && v.isExplicit then
if u.getOffset ≥ v.getOffset then u else v
else if u == v then u
if v.isExplicit && u.getOffset ≥ v.getOffset then true
else match u with
| Level.max u₁ u₂ _ => v == u₁ || v == u₂
| _ => false
if u == v then u
else if u.isZero then v
else if v.isZero then u
else if subsumes u v then u
@ -436,6 +436,7 @@ def mkLevelMax' (u v : Level) : Level :=
mkLevelMax u v
/- Similar to `mkLevelIMax`, but applies cheap simplifications -/
@[export lean_level_mk_imax_simp]
def mkLevelIMax' (u v : Level) : Level :=
if v.isNeverZero then mkLevelMax' u v
else if v.isZero then v

6
stage0/src/kernel/level.cpp generated
View file

@ -29,6 +29,8 @@ extern "C" object * lean_level_mk_mvar(obj_arg);
extern "C" object * lean_level_mk_param(obj_arg);
extern "C" object * lean_level_mk_max(obj_arg, obj_arg);
extern "C" object * lean_level_mk_imax(obj_arg, obj_arg);
extern "C" object * lean_level_mk_max_simp(obj_arg, obj_arg);
extern "C" object * lean_level_mk_imax_simp(obj_arg, obj_arg);
level mk_succ(level const & l) { return level(lean_level_mk_succ(l.to_obj_arg())); }
level mk_max_core(level const & l1, level const & l2) { return level(lean_level_mk_max(l1.to_obj_arg(), l2.to_obj_arg())); }
@ -305,7 +307,7 @@ extern "C" object * lean_level_update_max(obj_arg l, obj_arg new_lhs, obj_arg ne
return l;
} else {
lean_dec_ref(l);
return lean_level_mk_max(new_lhs, new_rhs);
return lean_level_mk_max_simp(new_lhs, new_rhs);
}
}
@ -315,7 +317,7 @@ extern "C" object * lean_level_update_imax(obj_arg l, obj_arg new_lhs, obj_arg n
return l;
} else {
lean_dec_ref(l);
return lean_level_mk_imax(new_lhs, new_rhs);
return lean_level_mk_imax_simp(new_lhs, new_rhs);
}
}

353
stage0/stdlib/Init/NotationExtra.c generated
View file

@ -14,11 +14,9 @@
extern "C" {
#endif
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_901____closed__1;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__4;
size_t l_USize_add(size_t, size_t);
lean_object* l_Lean_expandExplicitBindersAux_loop___closed__5;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__4;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__2;
lean_object* l_Lean_unbracktedExplicitBinders;
lean_object* l_Lean_explicitBinders___closed__4;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__10;
@ -33,11 +31,13 @@ lean_object* l_Lean_expandExplicitBindersAux(lean_object*, lean_object*, lean_ob
lean_object* l_Lean_expandBrackedBindersAux_loop_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_901____boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l___kind_term____x40_Init_Notation___hyg_3____closed__13;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__6;
extern lean_object* l_Array_empty___closed__1;
lean_object* l_Lean_expandExplicitBindersAux_loop___closed__12;
lean_object* l_Lean_explicitBinders___closed__2;
lean_object* l_Lean_expandExplicitBindersAux_loop_match__1(lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_5787____closed__11;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__2;
lean_object* l_Lean_bracketedExplicitBinders___closed__7;
lean_object* l_Lean_unbracktedExplicitBinders___closed__4;
uint8_t lean_name_eq(lean_object*, lean_object*);
@ -49,19 +49,20 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_6031____closed__4;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__5;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__5;
lean_object* l_Lean_expandExplicitBindersAux_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_bracketedExplicitBinders___closed__3;
lean_object* l_Lean_explicitBinders___closed__1;
lean_object* l_Lean_expandExplicitBindersAux_loop_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_expandExplicitBindersAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1393____boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_bracketedExplicitBinders___closed__5;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__3;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__3;
lean_object* l_Lean_expandExplicitBindersAux_loop___closed__13;
lean_object* l_Lean_expandExplicitBindersAux_loop___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__6;
lean_object* l_Lean_expandExplicitBindersAux_loop___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__2;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__7;
lean_object* l_Lean_expandBrackedBindersAux_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_expandBrackedBindersAux_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_expandBrackedBindersAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -71,23 +72,29 @@ lean_object* l_Lean_binderIdent;
lean_object* l_Lean_expandBrackedBinders(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
extern lean_object* l_Lean_Name_appendIndexAfter___closed__1;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__3;
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__5;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__5;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__1;
lean_object* l_Lean_Syntax_copyInfo(lean_object*, lean_object*);
lean_object* l_Lean_bracketedExplicitBinders___closed__6;
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_explicitBinders___closed__5;
lean_object* l_Array_anyMUnsafe_any___at_Lean_expandExplicitBinders___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1507____boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_expandExplicitBindersAux_loop___closed__7;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_983____closed__7;
lean_object* l_Lean_expandExplicitBinders(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_6360____closed__17;
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1273____boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Util_0__mkPanicMessage___closed__2;
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1269____boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_6360____closed__15;
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2;
lean_object* l_Lean_expandBrackedBindersAux_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Init_Prelude___instance__72___closed__1;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__4;
lean_object* l_Lean_bracketedExplicitBinders;
lean_object* l_Lean_unbracktedExplicitBinders___closed__6;
lean_object* l_Lean_bracketedExplicitBinders___closed__2;
@ -95,7 +102,6 @@ lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1025____boxed(lean_object
extern lean_object* l_myMacro____x40_Init_Notation___hyg_38____closed__8;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_983____closed__4;
lean_object* l_Lean_expandExplicitBindersAux_loop___closed__11;
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__6;
uint8_t l_Array_anyMUnsafe_any___at_Lean_expandExplicitBinders___spec__1(lean_object*, lean_object*, size_t, size_t);
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__6;
@ -104,13 +110,13 @@ lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__3;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_6360____closed__13;
size_t lean_usize_of_nat(lean_object*);
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__5;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_38____closed__6;
lean_object* l_Lean_bracketedExplicitBinders___closed__1;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__8;
lean_object* l_Lean_bracketedExplicitBinders___closed__8;
extern lean_object* l_Lean_nullKind___closed__2;
lean_object* l_Lean_bracketedExplicitBinders___closed__9;
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__1;
lean_object* l_Lean_bracketedExplicitBinders___closed__4;
lean_object* l_Lean_expandExplicitBindersAux_loop_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_expandBrackedBindersAux_loop_match__1(lean_object*);
@ -121,8 +127,9 @@ lean_object* l_Lean_expandExplicitBindersAux_loop_match__1___rarg___boxed(lean_o
lean_object* l_Lean_expandExplicitBindersAux_loop___closed__6;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_983____closed__6;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1469_;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859_;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345_;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355_;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231_;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1107_;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_983_;
@ -133,17 +140,19 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_38____closed__2;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_983____closed__5;
lean_object* l_Lean_unbracktedExplicitBinders___closed__7;
extern lean_object* l_Lean_Name_hasMacroScopes___closed__1;
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1383_(lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1393_(lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1507_(lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_901_(lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1025_(lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1149_(lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1269_(lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1273_(lean_object*, lean_object*, lean_object*);
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__3;
lean_object* l_Lean_expandExplicitBindersAux_loop_match__2(lean_object*);
uint8_t l_Lean_Syntax_isNone(lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__7;
lean_object* l_Lean_expandBrackedBindersAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__3;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__2;
lean_object* l_Lean_expandBrackedBinders___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_binderIdent___closed__4;
@ -154,6 +163,7 @@ uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_5787____closed__8;
lean_object* l_Lean_expandExplicitBindersAux_loop___closed__1;
extern lean_object* l___kind_term____x40_Init_Notation___hyg_6910____closed__7;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__5;
lean_object* l_Lean_expandExplicitBindersAux_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkHole___closed__2;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__1;
@ -178,11 +188,11 @@ lean_object* l_Lean_unbracktedExplicitBinders___closed__3;
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1149____closed__2;
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1149____boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_901____closed__2;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__6;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__4;
lean_object* l_Lean_unbracktedExplicitBinders___closed__2;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1;
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1383____boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_6360____closed__11;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1;
lean_object* l_Lean_expandExplicitBindersAux_loop___closed__3;
lean_object* l___kind_term____x40_Init_NotationExtra___hyg_859____closed__9;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
@ -1573,7 +1583,7 @@ static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_983____c
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Σ");
x_1 = lean_mk_string("exists");
return x_1;
}
}
@ -1651,24 +1661,6 @@ x_1 = l___kind_term____x40_Init_NotationExtra___hyg_983____closed__7;
return x_1;
}
}
static lean_object* _init_l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Sigma");
return x_1;
}
}
static lean_object* _init_l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1025_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -1713,7 +1705,7 @@ x_15 = l_Lean_Syntax_getArg(x_1, x_14);
x_16 = lean_unsigned_to_nat(3u);
x_17 = l_Lean_Syntax_getArg(x_1, x_16);
lean_dec(x_1);
x_18 = l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2;
x_18 = l_myMacro____x40_Init_NotationExtra___hyg_901____closed__2;
x_19 = l_Lean_expandExplicitBinders(x_18, x_15, x_17, x_2, x_3);
lean_dec(x_15);
return x_19;
@ -1744,7 +1736,7 @@ static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1107____
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Σ'");
x_1 = lean_mk_string("Σ");
return x_1;
}
}
@ -1826,7 +1818,7 @@ static lean_object* _init_l_myMacro____x40_Init_NotationExtra___hyg_1149____clos
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("PSigma");
x_1 = lean_mk_string("Sigma");
return x_1;
}
}
@ -1915,7 +1907,7 @@ static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1231____
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("×");
x_1 = lean_mk_string("Σ'");
return x_1;
}
}
@ -1934,8 +1926,8 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
x_2 = l_Lean_bracketedExplicitBinders;
x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__3;
x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__3;
x_3 = l_Lean_explicitBinders;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -1949,7 +1941,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__4;
x_3 = l___kind_term____x40_Init_Notation___hyg_6293____closed__9;
x_3 = l___kind_term____x40_Init_Notation___hyg_6910____closed__7;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -1961,9 +1953,23 @@ static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1231____
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__5;
x_3 = l___kind_term____x40_Init_Notation___hyg_6293____closed__9;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__1;
x_2 = lean_unsigned_to_nat(25u);
x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__5;
x_2 = lean_unsigned_to_nat(1023u);
x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__6;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -1975,11 +1981,29 @@ static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1231_()
_start:
{
lean_object* x_1;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__6;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__7;
return x_1;
}
}
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1269_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
static lean_object* _init_l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("PSigma");
return x_1;
}
}
static lean_object* _init_l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1273_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
@ -2002,7 +2026,7 @@ lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_8 = l_Lean_Syntax_getArgs(x_1);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = lean_unsigned_to_nat(3u);
x_10 = lean_unsigned_to_nat(4u);
x_11 = lean_nat_dec_eq(x_9, x_10);
lean_dec(x_9);
if (x_11 == 0)
@ -2018,62 +2042,63 @@ return x_13;
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_14 = lean_unsigned_to_nat(0u);
x_14 = lean_unsigned_to_nat(1u);
x_15 = l_Lean_Syntax_getArg(x_1, x_14);
x_16 = lean_unsigned_to_nat(2u);
x_16 = lean_unsigned_to_nat(3u);
x_17 = l_Lean_Syntax_getArg(x_1, x_16);
lean_dec(x_1);
x_18 = l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2;
x_19 = l_Lean_expandBrackedBinders(x_18, x_15, x_17, x_2, x_3);
x_18 = l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2;
x_19 = l_Lean_expandExplicitBinders(x_18, x_15, x_17, x_2, x_3);
lean_dec(x_15);
return x_19;
}
}
}
}
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1269____boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1273____boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_myMacro____x40_Init_NotationExtra___hyg_1269_(x_1, x_2, x_3);
x_4 = l_myMacro____x40_Init_NotationExtra___hyg_1273_(x_1, x_2, x_3);
lean_dec(x_2);
return x_4;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1() {
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_859____closed__3;
x_2 = lean_unsigned_to_nat(1345u);
x_2 = lean_unsigned_to_nat(1355u);
x_3 = lean_name_mk_numeral(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__2() {
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("×'");
x_1 = lean_mk_string("×");
return x_1;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__3() {
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__2;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__4() {
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
x_2 = l_Lean_bracketedExplicitBinders;
x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__3;
x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__3;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -2081,12 +2106,12 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__5() {
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__4;
x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__4;
x_3 = l___kind_term____x40_Init_Notation___hyg_6293____closed__9;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
@ -2095,13 +2120,13 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__6() {
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1;
x_2 = lean_unsigned_to_nat(25u);
x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__5;
x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__5;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -2109,19 +2134,19 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1345_() {
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1355_() {
_start:
{
lean_object* x_1;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__6;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__6;
return x_1;
}
}
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1383_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1393_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1;
x_4 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1;
lean_inc(x_1);
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
@ -2168,11 +2193,149 @@ return x_19;
}
}
}
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1383____boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1393____boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_myMacro____x40_Init_NotationExtra___hyg_1383_(x_1, x_2, x_3);
x_4 = l_myMacro____x40_Init_NotationExtra___hyg_1393_(x_1, x_2, x_3);
lean_dec(x_2);
return x_4;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_859____closed__3;
x_2 = lean_unsigned_to_nat(1469u);
x_3 = lean_name_mk_numeral(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("×'");
return x_1;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__2;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
x_2 = l_Lean_bracketedExplicitBinders;
x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__3;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__4;
x_3 = l___kind_term____x40_Init_Notation___hyg_6293____closed__9;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1;
x_2 = lean_unsigned_to_nat(25u);
x_3 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__5;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l___kind_term____x40_Init_NotationExtra___hyg_1469_() {
_start:
{
lean_object* x_1;
x_1 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__6;
return x_1;
}
}
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1507_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1;
lean_inc(x_1);
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_1);
x_6 = lean_box(1);
x_7 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_3);
return x_7;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_8 = l_Lean_Syntax_getArgs(x_1);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = lean_unsigned_to_nat(3u);
x_11 = lean_nat_dec_eq(x_9, x_10);
lean_dec(x_9);
if (x_11 == 0)
{
lean_object* x_12; lean_object* x_13;
lean_dec(x_1);
x_12 = lean_box(1);
x_13 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_3);
return x_13;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_14 = lean_unsigned_to_nat(0u);
x_15 = l_Lean_Syntax_getArg(x_1, x_14);
x_16 = lean_unsigned_to_nat(2u);
x_17 = l_Lean_Syntax_getArg(x_1, x_16);
lean_dec(x_1);
x_18 = l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2;
x_19 = l_Lean_expandBrackedBinders(x_18, x_15, x_17, x_2, x_3);
return x_19;
}
}
}
}
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_1507____boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_myMacro____x40_Init_NotationExtra___hyg_1507_(x_1, x_2, x_3);
lean_dec(x_2);
return x_4;
}
@ -2316,10 +2479,6 @@ l___kind_term____x40_Init_NotationExtra___hyg_983____closed__7 = _init_l___kind_
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_983____closed__7);
l___kind_term____x40_Init_NotationExtra___hyg_983_ = _init_l___kind_term____x40_Init_NotationExtra___hyg_983_();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_983_);
l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__1 = _init_l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__1();
lean_mark_persistent(l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__1);
l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2 = _init_l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2();
lean_mark_persistent(l_myMacro____x40_Init_NotationExtra___hyg_1025____closed__2);
l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__1 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__1();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__1);
l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__2 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1107____closed__2();
@ -2352,22 +2511,42 @@ l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__5 = _init_l___kind
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__5);
l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__6 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__6();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__6);
l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__7 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__7();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__7);
l___kind_term____x40_Init_NotationExtra___hyg_1231_ = _init_l___kind_term____x40_Init_NotationExtra___hyg_1231_();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1231_);
l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__1);
l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__2 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__2();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__2);
l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__3 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__3();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__3);
l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__4 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__4();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__4);
l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__5 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__5();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__5);
l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__6 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__6();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345____closed__6);
l___kind_term____x40_Init_NotationExtra___hyg_1345_ = _init_l___kind_term____x40_Init_NotationExtra___hyg_1345_();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1345_);
l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__1 = _init_l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__1();
lean_mark_persistent(l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__1);
l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2 = _init_l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2();
lean_mark_persistent(l_myMacro____x40_Init_NotationExtra___hyg_1273____closed__2);
l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__1);
l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2);
l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__3 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__3();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__3);
l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__4 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__4();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__4);
l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__5 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__5();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__5);
l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__6 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__6();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__6);
l___kind_term____x40_Init_NotationExtra___hyg_1355_ = _init_l___kind_term____x40_Init_NotationExtra___hyg_1355_();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1355_);
l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__1);
l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__2 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__2();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__2);
l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__3 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__3();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__3);
l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__4 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__4();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__4);
l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__5 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__5();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__5);
l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__6 = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__6();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469____closed__6);
l___kind_term____x40_Init_NotationExtra___hyg_1469_ = _init_l___kind_term____x40_Init_NotationExtra___hyg_1469_();
lean_mark_persistent(l___kind_term____x40_Init_NotationExtra___hyg_1469_);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

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

@ -1108,7 +1108,6 @@ lean_object* l_Lean_Delaborator_delabInfixOp(lean_object*, lean_object*, lean_ob
lean_object* l_Lean_Delaborator_delabMul___closed__1;
extern lean_object* l_Lean_mkOptionalNode___closed__1;
extern lean_object* l_Array_Init_Data_Array_Basic___instance__3___rarg___closed__1;
extern lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__2;
extern lean_object* l___kind_term____x40_Init_Notation___hyg_4833____closed__1;
extern lean_object* l_Lean_Meta_evalNat___closed__1;
lean_object* l_Lean_getPPNotation___closed__2;
@ -1352,6 +1351,7 @@ lean_object* l_Lean_Delaborator_mkDelabAttribute___closed__9;
lean_object* l_Lean_Level_quote___closed__2;
lean_object* l_Lean_Delaborator_delabIff___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Delaborator_Lean_Delaborator___instance__4___closed__1;
extern lean_object* l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_6360____closed__11;
lean_object* l_Array_zipWithAux___at_Lean_Delaborator_delabAppMatch___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyMUnsafe_any___at_Lean_Delaborator_delabLam___spec__1(lean_object*, lean_object*, size_t, size_t);
@ -27884,7 +27884,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Init_Prelude___instance__72___closed__1;
x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1231____closed__2;
x_2 = l___kind_term____x40_Init_NotationExtra___hyg_1355____closed__2;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);

8
stage0/stdlib/Lean/Elab/Level.c generated
View file

@ -50,10 +50,10 @@ extern lean_object* l_Lean_numLitKind;
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_mkFreshLevelMVar(lean_object*, lean_object*);
extern lean_object* l_Lean_Level_LevelToFormat_Result_format___closed__2;
lean_object* l_Lean_mkLevelMax_x27(lean_object*, lean_object*);
lean_object* lean_level_mk_max_simp(lean_object*, lean_object*);
lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_Lean_Elab_Level___instance__3___closed__4;
lean_object* l_Lean_mkLevelIMax_x27(lean_object*, lean_object*);
lean_object* lean_level_mk_imax_simp(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_elabLevel___closed__12;
lean_object* l_Lean_Elab_Level_elabLevel_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_elabLevel_match__1(lean_object*);
@ -728,7 +728,7 @@ lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l_Lean_mkLevelIMax_x27(x_4, x_12);
x_14 = lean_level_mk_imax_simp(x_4, x_12);
x_15 = 1;
x_16 = x_3 + x_15;
x_3 = x_16;
@ -792,7 +792,7 @@ lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l_Lean_mkLevelMax_x27(x_4, x_12);
x_14 = lean_level_mk_max_simp(x_4, x_12);
x_15 = 1;
x_16 = x_3 + x_15;
x_3 = x_16;

297
stage0/stdlib/Lean/Level.c generated
View file

@ -134,7 +134,7 @@ lean_object* l_Lean_Level_LevelToFormat_Result_format___closed__2;
uint64_t l_Lean_Level_mkData(size_t, lean_object*, uint8_t, uint8_t);
lean_object* l_Lean_Level_getLevelOffset_match__1(lean_object*);
lean_object* lean_level_update_max(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelMax_x27(lean_object*, lean_object*);
lean_object* lean_level_mk_max_simp(lean_object*, lean_object*);
lean_object* l_Lean_Level_normalize___closed__1;
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
uint32_t l_UInt64_toUInt32(uint64_t);
@ -145,7 +145,7 @@ lean_object* l_Lean_Level_ofNat_match__1___rarg___boxed(lean_object*, lean_objec
lean_object* l___private_Lean_Level_0__Lean_Level_LevelToFormat_formatLst___at_Lean_Level_LevelToFormat_Result_format___spec__2(lean_object*);
lean_object* l_Lean_Level_occurs_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Level_depth___boxed(lean_object*);
lean_object* l_Lean_mkLevelIMax_x27(lean_object*, lean_object*);
lean_object* lean_level_mk_imax_simp(lean_object*, lean_object*);
lean_object* l_Lean_Level_toNat(lean_object*);
lean_object* l_Lean_Level_LevelToFormat_Result_max(lean_object*, lean_object*);
lean_object* l_Lean_Level_normLtAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -5847,42 +5847,45 @@ x_2 = lean_alloc_closure((void*)(l_Lean_mkLevelMax_x27_match__1___rarg), 3, 0);
return x_2;
}
}
lean_object* l_Lean_mkLevelMax_x27(lean_object* x_1, lean_object* x_2) {
lean_object* lean_level_mk_max_simp(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_13; lean_object* x_21; uint8_t x_32;
x_32 = l_Lean_Level_isExplicit(x_1);
lean_object* x_3; lean_object* x_13; uint8_t x_32;
x_32 = lean_level_eq(x_1, x_2);
if (x_32 == 0)
{
lean_object* x_33;
x_33 = lean_box(0);
x_21 = x_33;
goto block_31;
}
else
uint8_t x_33;
x_33 = l_Lean_Level_isZero(x_1);
if (x_33 == 0)
{
uint8_t x_34;
x_34 = l_Lean_Level_isExplicit(x_2);
x_34 = l_Lean_Level_isZero(x_2);
if (x_34 == 0)
{
lean_object* x_35;
x_35 = lean_box(0);
x_21 = x_35;
goto block_31;
}
else
uint8_t x_35;
x_35 = l_Lean_Level_isExplicit(x_2);
if (x_35 == 0)
{
lean_object* x_36; lean_object* x_37; lean_object* x_38; uint8_t x_39;
x_36 = lean_unsigned_to_nat(0u);
x_37 = l_Lean_Level_getOffsetAux(x_2, x_36);
x_38 = l_Lean_Level_getOffsetAux(x_1, x_36);
x_39 = lean_nat_dec_le(x_37, x_38);
lean_dec(x_38);
if (lean_obj_tag(x_1) == 2)
{
lean_object* x_36; lean_object* x_37; uint8_t x_38;
x_36 = lean_ctor_get(x_1, 0);
lean_inc(x_36);
x_37 = lean_ctor_get(x_1, 1);
lean_inc(x_37);
x_38 = lean_level_eq(x_2, x_36);
lean_dec(x_36);
if (x_38 == 0)
{
uint8_t x_39;
x_39 = lean_level_eq(x_2, x_37);
lean_dec(x_37);
if (x_39 == 0)
{
lean_dec(x_1);
return x_2;
lean_object* x_40;
x_40 = lean_box(0);
x_13 = x_40;
goto block_31;
}
else
{
@ -5890,6 +5893,97 @@ lean_dec(x_2);
return x_1;
}
}
else
{
lean_dec(x_37);
lean_dec(x_2);
return x_1;
}
}
else
{
lean_object* x_41;
x_41 = lean_box(0);
x_13 = x_41;
goto block_31;
}
}
else
{
lean_object* x_42; lean_object* x_43; lean_object* x_44; uint8_t x_45;
x_42 = lean_unsigned_to_nat(0u);
x_43 = l_Lean_Level_getOffsetAux(x_2, x_42);
x_44 = l_Lean_Level_getOffsetAux(x_1, x_42);
x_45 = lean_nat_dec_le(x_43, x_44);
lean_dec(x_44);
lean_dec(x_43);
if (x_45 == 0)
{
if (lean_obj_tag(x_1) == 2)
{
lean_object* x_46; lean_object* x_47; uint8_t x_48;
x_46 = lean_ctor_get(x_1, 0);
lean_inc(x_46);
x_47 = lean_ctor_get(x_1, 1);
lean_inc(x_47);
x_48 = lean_level_eq(x_2, x_46);
lean_dec(x_46);
if (x_48 == 0)
{
uint8_t x_49;
x_49 = lean_level_eq(x_2, x_47);
lean_dec(x_47);
if (x_49 == 0)
{
lean_object* x_50;
x_50 = lean_box(0);
x_13 = x_50;
goto block_31;
}
else
{
lean_dec(x_2);
return x_1;
}
}
else
{
lean_dec(x_47);
lean_dec(x_2);
return x_1;
}
}
else
{
lean_object* x_51;
x_51 = lean_box(0);
x_13 = x_51;
goto block_31;
}
}
else
{
lean_dec(x_2);
return x_1;
}
}
}
else
{
lean_dec(x_2);
return x_1;
}
}
else
{
lean_dec(x_1);
return x_2;
}
}
else
{
lean_dec(x_2);
return x_1;
}
block_12:
{
@ -5927,113 +6021,86 @@ return x_1;
}
}
}
block_20:
block_31:
{
uint8_t x_14;
lean_dec(x_13);
x_14 = l_Lean_Level_isExplicit(x_1);
if (x_14 == 0)
{
if (lean_obj_tag(x_2) == 2)
{
lean_object* x_14; lean_object* x_15; uint8_t x_16;
x_14 = lean_ctor_get(x_2, 0);
lean_inc(x_14);
x_15 = lean_ctor_get(x_2, 1);
lean_object* x_15; lean_object* x_16; uint8_t x_17;
x_15 = lean_ctor_get(x_2, 0);
lean_inc(x_15);
x_16 = lean_level_eq(x_1, x_14);
lean_dec(x_14);
if (x_16 == 0)
{
uint8_t x_17;
x_16 = lean_ctor_get(x_2, 1);
lean_inc(x_16);
x_17 = lean_level_eq(x_1, x_15);
lean_dec(x_15);
if (x_17 == 0)
{
lean_object* x_18;
x_18 = lean_box(0);
x_3 = x_18;
goto block_12;
}
else
{
lean_dec(x_1);
return x_2;
}
}
else
{
lean_dec(x_15);
lean_dec(x_1);
return x_2;
}
}
else
uint8_t x_18;
x_18 = lean_level_eq(x_1, x_16);
lean_dec(x_16);
if (x_18 == 0)
{
lean_object* x_19;
x_19 = lean_box(0);
x_3 = x_19;
goto block_12;
}
else
{
lean_dec(x_1);
return x_2;
}
block_31:
}
else
{
uint8_t x_22;
lean_dec(x_21);
x_22 = lean_level_eq(x_1, x_2);
if (x_22 == 0)
lean_dec(x_16);
lean_dec(x_1);
return x_2;
}
}
else
{
uint8_t x_23;
x_23 = l_Lean_Level_isZero(x_1);
if (x_23 == 0)
lean_object* x_20;
x_20 = lean_box(0);
x_3 = x_20;
goto block_12;
}
}
else
{
uint8_t x_24;
x_24 = l_Lean_Level_isZero(x_2);
lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_21 = lean_unsigned_to_nat(0u);
x_22 = l_Lean_Level_getOffsetAux(x_1, x_21);
x_23 = l_Lean_Level_getOffsetAux(x_2, x_21);
x_24 = lean_nat_dec_le(x_22, x_23);
lean_dec(x_23);
lean_dec(x_22);
if (x_24 == 0)
{
if (lean_obj_tag(x_1) == 2)
if (lean_obj_tag(x_2) == 2)
{
lean_object* x_25; lean_object* x_26; uint8_t x_27;
x_25 = lean_ctor_get(x_1, 0);
x_25 = lean_ctor_get(x_2, 0);
lean_inc(x_25);
x_26 = lean_ctor_get(x_1, 1);
x_26 = lean_ctor_get(x_2, 1);
lean_inc(x_26);
x_27 = lean_level_eq(x_2, x_25);
x_27 = lean_level_eq(x_1, x_25);
lean_dec(x_25);
if (x_27 == 0)
{
uint8_t x_28;
x_28 = lean_level_eq(x_2, x_26);
x_28 = lean_level_eq(x_1, x_26);
lean_dec(x_26);
if (x_28 == 0)
{
lean_object* x_29;
x_29 = lean_box(0);
x_13 = x_29;
goto block_20;
}
else
{
lean_dec(x_2);
return x_1;
}
}
else
{
lean_dec(x_26);
lean_dec(x_2);
return x_1;
}
}
else
{
lean_object* x_30;
x_30 = lean_box(0);
x_13 = x_30;
goto block_20;
}
}
else
{
lean_dec(x_2);
return x_1;
}
x_3 = x_29;
goto block_12;
}
else
{
@ -6043,13 +6110,29 @@ return x_2;
}
else
{
lean_dec(x_2);
return x_1;
lean_dec(x_26);
lean_dec(x_1);
return x_2;
}
}
else
{
lean_object* x_30;
x_30 = lean_box(0);
x_3 = x_30;
goto block_12;
}
}
else
{
lean_dec(x_1);
return x_2;
}
}
}
}
lean_object* l_Lean_mkLevelIMax_x27(lean_object* x_1, lean_object* x_2) {
}
lean_object* lean_level_mk_imax_simp(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
@ -6093,7 +6176,7 @@ return x_2;
else
{
lean_object* x_8;
x_8 = l_Lean_mkLevelMax_x27(x_1, x_2);
x_8 = lean_level_mk_max_simp(x_1, x_2);
return x_8;
}
}
@ -6160,7 +6243,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_Level_mkData___closed__2;
x_2 = l_Lean_Level_updateSucc_x21___closed__1;
x_3 = lean_unsigned_to_nat(464u);
x_3 = lean_unsigned_to_nat(465u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Level_updateSucc_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -6270,7 +6353,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_Level_mkData___closed__2;
x_2 = l_Lean_Level_updateMax_x21___closed__1;
x_3 = lean_unsigned_to_nat(473u);
x_3 = lean_unsigned_to_nat(474u);
x_4 = lean_unsigned_to_nat(21u);
x_5 = l_Lean_Level_updateMax_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -6384,7 +6467,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_Level_mkData___closed__2;
x_2 = l_Lean_Level_updateIMax_x21___closed__1;
x_3 = lean_unsigned_to_nat(482u);
x_3 = lean_unsigned_to_nat(483u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Level_updateIMax_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -6512,7 +6595,7 @@ x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
lean_dec(x_1);
x_6 = l_Lean_Level_mkNaryMax(x_3);
x_7 = l_Lean_mkLevelMax_x27(x_5, x_6);
x_7 = lean_level_mk_max_simp(x_5, x_6);
return x_7;
}
}

4
stage0/stdlib/Lean/Meta/InferType.c generated
View file

@ -114,7 +114,7 @@ lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at___private_Lea
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_whnf___at___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_isTypeImp(lean_object*);
lean_object* l_Lean_mkLevelIMax_x27(lean_object*, lean_object*);
lean_object* lean_level_mk_imax_simp(lean_object*, lean_object*);
lean_object* lean_instantiate_type_lparams(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_isArrowType_match__1(lean_object*);
lean_object* l_Lean_Meta_isProofQuick_match__1(lean_object*);
@ -2924,7 +2924,7 @@ lean_inc(x_18);
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_17);
x_20 = l_Lean_mkLevelIMax_x27(x_18, x_4);
x_20 = lean_level_mk_imax_simp(x_18, x_4);
x_2 = x_12;
x_4 = x_20;
x_9 = x_19;

18
stage0/stdlib/Lean/Meta/LevelDefEq.c generated
View file

@ -145,7 +145,7 @@ lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solve(lean_object*, l
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_869____closed__1;
lean_object* l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelMax_x27(lean_object*, lean_object*);
lean_object* lean_level_mk_max_simp(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_decAux_x3f_match__4(lean_object*);
lean_object* l_Lean_Meta_isLevelDefEqAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_mkMaxArgsDiff___boxed(lean_object*, lean_object*, lean_object*);
@ -875,7 +875,7 @@ if (x_32 == 0)
{
lean_object* x_33; lean_object* x_34;
x_33 = lean_ctor_get(x_23, 0);
x_34 = l_Lean_mkLevelMax_x27(x_21, x_33);
x_34 = lean_level_mk_max_simp(x_21, x_33);
lean_ctor_set(x_23, 0, x_34);
return x_22;
}
@ -885,7 +885,7 @@ lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_35 = lean_ctor_get(x_23, 0);
lean_inc(x_35);
lean_dec(x_23);
x_36 = l_Lean_mkLevelMax_x27(x_21, x_35);
x_36 = lean_level_mk_max_simp(x_21, x_35);
x_37 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_37, 0, x_36);
lean_ctor_set(x_22, 0, x_37);
@ -907,7 +907,7 @@ if (lean_is_exclusive(x_23)) {
lean_dec_ref(x_23);
x_40 = lean_box(0);
}
x_41 = l_Lean_mkLevelMax_x27(x_21, x_39);
x_41 = lean_level_mk_max_simp(x_21, x_39);
if (lean_is_scalar(x_40)) {
x_42 = lean_alloc_ctor(1, 1, 0);
} else {
@ -1067,7 +1067,7 @@ if (x_74 == 0)
{
lean_object* x_75; lean_object* x_76;
x_75 = lean_ctor_get(x_65, 0);
x_76 = l_Lean_mkLevelMax_x27(x_63, x_75);
x_76 = lean_level_mk_max_simp(x_63, x_75);
lean_ctor_set(x_65, 0, x_76);
return x_64;
}
@ -1077,7 +1077,7 @@ lean_object* x_77; lean_object* x_78; lean_object* x_79;
x_77 = lean_ctor_get(x_65, 0);
lean_inc(x_77);
lean_dec(x_65);
x_78 = l_Lean_mkLevelMax_x27(x_63, x_77);
x_78 = lean_level_mk_max_simp(x_63, x_77);
x_79 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_79, 0, x_78);
lean_ctor_set(x_64, 0, x_79);
@ -1099,7 +1099,7 @@ if (lean_is_exclusive(x_65)) {
lean_dec_ref(x_65);
x_82 = lean_box(0);
}
x_83 = l_Lean_mkLevelMax_x27(x_63, x_81);
x_83 = lean_level_mk_max_simp(x_63, x_81);
if (lean_is_scalar(x_82)) {
x_84 = lean_alloc_ctor(1, 1, 0);
} else {
@ -2104,7 +2104,7 @@ lean_dec(x_8);
if (x_9 == 0)
{
lean_object* x_10;
x_10 = l_Lean_mkLevelMax_x27(x_3, x_2);
x_10 = lean_level_mk_max_simp(x_3, x_2);
return x_10;
}
else
@ -2116,7 +2116,7 @@ return x_3;
default:
{
lean_object* x_11;
x_11 = l_Lean_mkLevelMax_x27(x_3, x_2);
x_11 = lean_level_mk_max_simp(x_3, x_2);
return x_11;
}
}

8
stage0/stdlib/Lean/Util/ReplaceLevel.c generated
View file

@ -33,8 +33,8 @@ lean_object* l_List_map___at_Lean_Expr_replaceLevel___spec__1(lean_object*, lean
lean_object* l_List_map___at_Lean_Expr_ReplaceLevelImpl_replaceUnsafeM_visit___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Level_replace_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_ReplaceLevelImpl_replaceUnsafeM_visit_match__1(lean_object*);
lean_object* l_Lean_mkLevelMax_x27(lean_object*, lean_object*);
lean_object* l_Lean_mkLevelIMax_x27(lean_object*, lean_object*);
lean_object* lean_level_mk_max_simp(lean_object*, lean_object*);
lean_object* lean_level_mk_imax_simp(lean_object*, lean_object*);
lean_object* l_Lean_Expr_ReplaceLevelImpl_replaceUnsafe(lean_object*, lean_object*);
lean_object* l_Lean_Expr_ReplaceLevelImpl_initCache___closed__1;
lean_object* lean_expr_update_let(lean_object*, lean_object*, lean_object*, lean_object*);
@ -188,7 +188,7 @@ lean_dec(x_2);
lean_inc(x_1);
x_9 = l_Lean_Level_replace(x_1, x_7);
x_10 = l_Lean_Level_replace(x_1, x_8);
x_11 = l_Lean_mkLevelMax_x27(x_9, x_10);
x_11 = lean_level_mk_max_simp(x_9, x_10);
return x_11;
}
case 3:
@ -202,7 +202,7 @@ lean_dec(x_2);
lean_inc(x_1);
x_14 = l_Lean_Level_replace(x_1, x_12);
x_15 = l_Lean_Level_replace(x_1, x_13);
x_16 = l_Lean_mkLevelIMax_x27(x_14, x_15);
x_16 = lean_level_mk_imax_simp(x_14, x_15);
return x_16;
}
default: