chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
6631f1d5b3
commit
35d25dfaaf
8 changed files with 421 additions and 59 deletions
2
stage0/src/Lean/Elab/Match.lean
generated
2
stage0/src/Lean/Elab/Match.lean
generated
|
|
@ -494,7 +494,7 @@ partial def main (e : Expr) : M Pattern := do
|
|||
return Pattern.arrayLit α (← lits.mapM main)
|
||||
| none =>
|
||||
-- TODO: namedPattern will have 4 arguments
|
||||
if e.isAppOfArity ``_root_.namedPattern 3 then
|
||||
if e.isAppOfArity ``_root_.namedPatternOld 3 then
|
||||
let p ← main <| e.getArg! 2
|
||||
match e.getArg! 1 with
|
||||
| Expr.fvar fvarId _ => return Pattern.as fvarId p
|
||||
|
|
|
|||
2
stage0/src/Lean/Elab/PatternVar.lean
generated
2
stage0/src/Lean/Elab/PatternVar.lean
generated
|
|
@ -210,7 +210,7 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
|
|||
discard <| processVar id
|
||||
let pat := stx[3]
|
||||
let pat ← collect pat
|
||||
`(_root_.namedPattern $id $pat)
|
||||
``(_root_.namedPatternOld $id $pat)
|
||||
else if k == ``Lean.Parser.Term.binop then
|
||||
let lhs ← collect stx[2]
|
||||
let rhs ← collect stx[3]
|
||||
|
|
|
|||
4
stage0/src/Lean/Meta/Match/Basic.lean
generated
4
stage0/src/Lean/Meta/Match/Basic.lean
generated
|
|
@ -45,7 +45,7 @@ where
|
|||
| as fvarId p =>
|
||||
-- TODO
|
||||
if annotate then
|
||||
mkAppM `namedPattern #[mkFVar fvarId, (← visit p)]
|
||||
mkAppM ``namedPatternOld #[mkFVar fvarId, (← visit p)]
|
||||
else
|
||||
visit p
|
||||
| arrayLit type xs =>
|
||||
|
|
@ -278,7 +278,7 @@ partial def toPattern (e : Expr) : MetaM Pattern := do
|
|||
return Pattern.arrayLit α (← lits.mapM toPattern)
|
||||
| none =>
|
||||
-- TODO: `namedPattern` will have 4 arguments
|
||||
if e.isAppOfArity ``namedPattern 3 then
|
||||
if e.isAppOfArity ``namedPatternOld 3 then
|
||||
let p ← toPattern <| e.getArg! 2
|
||||
match e.getArg! 1 with
|
||||
| Expr.fvar fvarId _ => return Pattern.as fvarId p
|
||||
|
|
|
|||
|
|
@ -685,6 +685,16 @@ where
|
|||
| none => withBindingBodyUnusedName fun h => do
|
||||
return (← delab, h.getId)
|
||||
|
||||
@[builtinDelab app.namedPatternOld]
|
||||
def delabNamedPatternOld : Delab := do
|
||||
-- Note: we keep this as a delaborator because it accesses the DelabM context
|
||||
guard (← read).inPattern
|
||||
guard $ (← getExpr).getAppNumArgs == 3
|
||||
let x ← withAppFn $ withAppArg delab
|
||||
let p ← withAppArg delab
|
||||
guard x.isIdent
|
||||
`($x:ident@$p:term)
|
||||
|
||||
@[builtinDelab app.namedPattern]
|
||||
def delabNamedPattern : Delab := do
|
||||
-- Note: we keep this as a delaborator because it accesses the DelabM context
|
||||
|
|
|
|||
2
stage0/stdlib/Lean/Elab/Match.c
generated
2
stage0/stdlib/Lean/Elab/Match.c
generated
|
|
@ -16346,7 +16346,7 @@ static lean_object* _init_l_Lean_Elab_Term_ToDepElimPattern_main___closed__1() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("namedPattern");
|
||||
x_1 = lean_mk_string("namedPatternOld");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
91
stage0/stdlib/Lean/Elab/PatternVar.c
generated
91
stage0/stdlib/Lean/Elab/PatternVar.c
generated
|
|
@ -275,6 +275,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_CollectPatternVars_collect___lambda__4
|
|||
lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___closed__12;
|
||||
static lean_object* l_Lean_Elab_Term_CollectPatternVars_collect___closed__16;
|
||||
static lean_object* l_Lean_Elab_Term_CollectPatternVars_collect___closed__24;
|
||||
size_t lean_usize_of_nat(lean_object*);
|
||||
extern lean_object* l_Lean_NameSet_empty;
|
||||
lean_object* l_Lean_ConstantInfo_type(lean_object*);
|
||||
|
|
@ -6323,7 +6324,7 @@ static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___lambda__
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("_root_.namedPattern");
|
||||
x_1 = lean_mk_string("_root_.namedPatternOld");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
|
|
@ -6372,7 +6373,7 @@ static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___lambda__
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("namedPattern");
|
||||
x_1 = lean_mk_string("namedPatternOld");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
|
|
@ -7020,14 +7021,22 @@ return x_3;
|
|||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__9() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("namedPattern");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__10() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___closed__8;
|
||||
x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___lambda__3___closed__6;
|
||||
x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__9;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__10() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__11() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -7035,17 +7044,17 @@ x_1 = lean_mk_string("binop");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__11() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__12() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___closed__8;
|
||||
x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__10;
|
||||
x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__11;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__12() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__13() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -7053,17 +7062,17 @@ x_1 = lean_mk_string("inaccessible");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__13() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__14() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___closed__8;
|
||||
x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__12;
|
||||
x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__13;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__14() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__15() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -7071,17 +7080,17 @@ x_1 = lean_mk_string("quotedName");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__15() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__16() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___closed__8;
|
||||
x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__14;
|
||||
x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__15;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__16() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__17() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -7089,17 +7098,17 @@ x_1 = lean_mk_string("doubleQuotedName");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__17() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__18() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___closed__8;
|
||||
x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__16;
|
||||
x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__17;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__18() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__19() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -7107,16 +7116,16 @@ x_1 = lean_mk_string("invalid pattern, notation is ambiguous");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__19() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__20() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__18;
|
||||
x_1 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__19;
|
||||
x_2 = l_Lean_stringToMessageData(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__20() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__21() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -7124,17 +7133,17 @@ x_1 = lean_mk_string("typeAscription");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__21() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__22() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___closed__8;
|
||||
x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__20;
|
||||
x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__21;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__22() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__23() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -7142,11 +7151,11 @@ x_1 = lean_mk_string("invalid struct instance pattern, 'with' is not allowed in
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__23() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__24() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__22;
|
||||
x_1 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__23;
|
||||
x_2 = l_Lean_stringToMessageData(x_1);
|
||||
return x_2;
|
||||
}
|
||||
|
|
@ -7200,17 +7209,17 @@ x_27 = lean_name_eq(x_10, x_26);
|
|||
if (x_27 == 0)
|
||||
{
|
||||
lean_object* x_28; uint8_t x_29;
|
||||
x_28 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__9;
|
||||
x_28 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__10;
|
||||
x_29 = lean_name_eq(x_10, x_28);
|
||||
if (x_29 == 0)
|
||||
{
|
||||
lean_object* x_30; uint8_t x_31;
|
||||
x_30 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__11;
|
||||
x_30 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__12;
|
||||
x_31 = lean_name_eq(x_10, x_30);
|
||||
if (x_31 == 0)
|
||||
{
|
||||
lean_object* x_32; uint8_t x_33;
|
||||
x_32 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__13;
|
||||
x_32 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__14;
|
||||
x_33 = lean_name_eq(x_10, x_32);
|
||||
if (x_33 == 0)
|
||||
{
|
||||
|
|
@ -7235,12 +7244,12 @@ x_41 = lean_name_eq(x_10, x_40);
|
|||
if (x_41 == 0)
|
||||
{
|
||||
lean_object* x_42; uint8_t x_43;
|
||||
x_42 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__15;
|
||||
x_42 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__16;
|
||||
x_43 = lean_name_eq(x_10, x_42);
|
||||
if (x_43 == 0)
|
||||
{
|
||||
lean_object* x_44; uint8_t x_45;
|
||||
x_44 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__17;
|
||||
x_44 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__18;
|
||||
x_45 = lean_name_eq(x_10, x_44);
|
||||
if (x_45 == 0)
|
||||
{
|
||||
|
|
@ -7260,7 +7269,7 @@ return x_49;
|
|||
else
|
||||
{
|
||||
lean_object* x_50; lean_object* x_51; lean_object* x_52;
|
||||
x_50 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__19;
|
||||
x_50 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__20;
|
||||
x_51 = lean_alloc_closure((void*)(l_Lean_throwError___at___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___spec__1___boxed), 9, 2);
|
||||
lean_closure_set(x_51, 0, x_50);
|
||||
lean_closure_set(x_51, 1, x_2);
|
||||
|
|
@ -7408,7 +7417,7 @@ lean_object* x_86; lean_object* x_87; lean_object* x_88; uint8_t x_89;
|
|||
x_86 = l_Lean_Syntax_getArg(x_84, x_82);
|
||||
lean_dec(x_84);
|
||||
x_87 = l_Lean_Syntax_getKind(x_86);
|
||||
x_88 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__21;
|
||||
x_88 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__22;
|
||||
x_89 = lean_name_eq(x_87, x_88);
|
||||
lean_dec(x_87);
|
||||
if (x_89 == 0)
|
||||
|
|
@ -7484,7 +7493,7 @@ if (x_103 == 0)
|
|||
{
|
||||
lean_object* x_104; lean_object* x_105; lean_object* x_106;
|
||||
lean_dec(x_1);
|
||||
x_104 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__23;
|
||||
x_104 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__24;
|
||||
x_105 = lean_alloc_closure((void*)(l_Lean_Elab_Term_CollectPatternVars_collect___lambda__7___boxed), 11, 4);
|
||||
lean_closure_set(x_105, 0, x_101);
|
||||
lean_closure_set(x_105, 1, x_104);
|
||||
|
|
@ -7610,17 +7619,17 @@ x_140 = lean_name_eq(x_10, x_139);
|
|||
if (x_140 == 0)
|
||||
{
|
||||
lean_object* x_141; uint8_t x_142;
|
||||
x_141 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__9;
|
||||
x_141 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__10;
|
||||
x_142 = lean_name_eq(x_10, x_141);
|
||||
if (x_142 == 0)
|
||||
{
|
||||
lean_object* x_143; uint8_t x_144;
|
||||
x_143 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__11;
|
||||
x_143 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__12;
|
||||
x_144 = lean_name_eq(x_10, x_143);
|
||||
if (x_144 == 0)
|
||||
{
|
||||
lean_object* x_145; uint8_t x_146;
|
||||
x_145 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__13;
|
||||
x_145 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__14;
|
||||
x_146 = lean_name_eq(x_10, x_145);
|
||||
if (x_146 == 0)
|
||||
{
|
||||
|
|
@ -7645,12 +7654,12 @@ x_154 = lean_name_eq(x_10, x_153);
|
|||
if (x_154 == 0)
|
||||
{
|
||||
lean_object* x_155; uint8_t x_156;
|
||||
x_155 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__15;
|
||||
x_155 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__16;
|
||||
x_156 = lean_name_eq(x_10, x_155);
|
||||
if (x_156 == 0)
|
||||
{
|
||||
lean_object* x_157; uint8_t x_158;
|
||||
x_157 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__17;
|
||||
x_157 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__18;
|
||||
x_158 = lean_name_eq(x_10, x_157);
|
||||
if (x_158 == 0)
|
||||
{
|
||||
|
|
@ -7670,7 +7679,7 @@ return x_162;
|
|||
else
|
||||
{
|
||||
lean_object* x_163; lean_object* x_164; lean_object* x_165;
|
||||
x_163 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__19;
|
||||
x_163 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__20;
|
||||
x_164 = lean_alloc_closure((void*)(l_Lean_throwError___at___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___spec__1___boxed), 9, 2);
|
||||
lean_closure_set(x_164, 0, x_163);
|
||||
lean_closure_set(x_164, 1, x_2);
|
||||
|
|
@ -7818,7 +7827,7 @@ lean_object* x_199; lean_object* x_200; lean_object* x_201; uint8_t x_202;
|
|||
x_199 = l_Lean_Syntax_getArg(x_197, x_195);
|
||||
lean_dec(x_197);
|
||||
x_200 = l_Lean_Syntax_getKind(x_199);
|
||||
x_201 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__21;
|
||||
x_201 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__22;
|
||||
x_202 = lean_name_eq(x_200, x_201);
|
||||
lean_dec(x_200);
|
||||
if (x_202 == 0)
|
||||
|
|
@ -7894,7 +7903,7 @@ if (x_216 == 0)
|
|||
{
|
||||
lean_object* x_217; lean_object* x_218; lean_object* x_219;
|
||||
lean_dec(x_1);
|
||||
x_217 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__23;
|
||||
x_217 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__24;
|
||||
x_218 = lean_alloc_closure((void*)(l_Lean_Elab_Term_CollectPatternVars_collect___lambda__7___boxed), 11, 4);
|
||||
lean_closure_set(x_218, 0, x_214);
|
||||
lean_closure_set(x_218, 1, x_217);
|
||||
|
|
@ -10991,6 +11000,8 @@ l_Lean_Elab_Term_CollectPatternVars_collect___closed__22 = _init_l_Lean_Elab_Ter
|
|||
lean_mark_persistent(l_Lean_Elab_Term_CollectPatternVars_collect___closed__22);
|
||||
l_Lean_Elab_Term_CollectPatternVars_collect___closed__23 = _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__23();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_CollectPatternVars_collect___closed__23);
|
||||
l_Lean_Elab_Term_CollectPatternVars_collect___closed__24 = _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__24();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_CollectPatternVars_collect___closed__24);
|
||||
l_Lean_addTrace___at_Lean_Elab_Term_CollectPatternVars_main___spec__1___closed__1 = _init_l_Lean_addTrace___at_Lean_Elab_Term_CollectPatternVars_main___spec__1___closed__1();
|
||||
lean_mark_persistent(l_Lean_addTrace___at_Lean_Elab_Term_CollectPatternVars_main___spec__1___closed__1);
|
||||
l_Lean_addTrace___at_Lean_Elab_Term_CollectPatternVars_main___spec__1___closed__2 = _init_l_Lean_addTrace___at_Lean_Elab_Term_CollectPatternVars_main___spec__1___closed__2();
|
||||
|
|
|
|||
2
stage0/stdlib/Lean/Meta/Match/Basic.c
generated
2
stage0/stdlib/Lean/Meta/Match/Basic.c
generated
|
|
@ -1154,7 +1154,7 @@ static lean_object* _init_l_Lean_Meta_Match_Pattern_toExpr_visit___closed__1() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("namedPattern");
|
||||
x_1 = lean_mk_string("namedPatternOld");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
367
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c
generated
367
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c
generated
|
|
@ -190,6 +190,7 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_withMDataOptions(lean_
|
|||
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar___closed__8;
|
||||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetE(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabLit(lean_object*);
|
||||
LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld(lean_object*);
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__4;
|
||||
lean_object* lean_private_to_user_name(lean_object*);
|
||||
|
|
@ -270,7 +271,6 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabDo___lambda__1___
|
|||
lean_object* l_Lean_Expr_appArg_x21(lean_object*);
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabDo___lambda__1___closed__4;
|
||||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withBindingBody___at_Lean_PrettyPrinter_Delaborator_delabLetFun___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabConst___spec__1(size_t, size_t, lean_object*);
|
||||
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_PrettyPrinter_Delaborator_delabForall___spec__6(lean_object*, lean_object*, size_t, size_t);
|
||||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit___lambda__4(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -296,7 +296,6 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_reifyName___closed__4;
|
|||
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabLam___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___spec__7(lean_object*, lean_object*, size_t, size_t, lean_object*);
|
||||
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabPSigma___closed__3;
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1;
|
||||
LEAN_EXPORT lean_object* l_panic___at_Lean_PrettyPrinter_Delaborator_withMDataOptions___spec__12(lean_object*);
|
||||
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppImplicit___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_nextExtraPos___at_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -588,6 +587,7 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetFun___lambda__1___c
|
|||
extern lean_object* l_Lean_instInhabitedSyntax;
|
||||
uint8_t l_Lean_Expr_isConstOf(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_getUnusedName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__5;
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___spec__5(lean_object*, lean_object*, size_t, size_t, lean_object*);
|
||||
uint8_t l_Lean_isLetFun(lean_object*);
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabSigmaCore___lambda__1___closed__10;
|
||||
|
|
@ -597,6 +597,7 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_delabMData___closed__3;
|
|||
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppExplicit___closed__4;
|
||||
LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabForall(lean_object*);
|
||||
lean_object* l_Lean_mkSepArray(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2;
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit___lambda__2___closed__2;
|
||||
LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabSort(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withBindingBody___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_skippingBinders_loop_visitLambda___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -604,6 +605,7 @@ LEAN_EXPORT lean_object* l_panic___at_Lean_PrettyPrinter_Delaborator_withMDataOp
|
|||
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabForall___closed__1;
|
||||
lean_object* l_Lean_Expr_consumeMData(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_returnsPi___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__3;
|
||||
extern lean_object* l_Lean_Meta_instMonadMetaM;
|
||||
LEAN_EXPORT lean_object* l_panic___at_Lean_PrettyPrinter_Delaborator_withMDataOptions___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -644,6 +646,7 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar
|
|||
lean_object* l_Lean_PrettyPrinter_Delaborator_withBindingBodyUnusedName___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetFun___lambda__1___closed__7;
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1;
|
||||
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabLam___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabSigma(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_maybeAddBlockImplicit___closed__8;
|
||||
|
|
@ -711,6 +714,7 @@ LEAN_EXPORT uint8_t l_Lean_PrettyPrinter_Delaborator_hasIdent(lean_object*, lean
|
|||
LEAN_EXPORT lean_object* l_Array_mapIdxM_map___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabPatterns___spec__5___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*, lean_object*);
|
||||
lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
|
||||
static lean_object* l_Array_foldrMUnsafe_fold___at_Lean_PrettyPrinter_Delaborator_delabForall___spec__1___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabSigmaCore___lambda__1___closed__7;
|
||||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_withMDatasOptions(lean_object*);
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabMVar___closed__2;
|
||||
|
|
@ -747,6 +751,7 @@ static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfNat___c
|
|||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetFun___lambda__1___closed__9;
|
||||
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabSort___closed__13;
|
||||
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__4;
|
||||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit___lambda__1___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* l_Lean_mkApp(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -766,6 +771,7 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___lambda__6__
|
|||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabDIte_delabBranch___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNameMkStr___closed__2;
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfScientific___lambda__1___closed__4;
|
||||
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1;
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetFun___lambda__1___closed__4;
|
||||
uint8_t l_Lean_BinderInfo_isExplicit(uint8_t);
|
||||
lean_object* l_Lean_Syntax_getKind(lean_object*);
|
||||
|
|
@ -800,6 +806,7 @@ static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNameMkNum
|
|||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetFun(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_getPPMotivesAll(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2;
|
||||
lean_object* l_Lean_getPPMatch___boxed(lean_object*);
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetE___closed__2;
|
||||
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfScientific___lambda__1___closed__2;
|
||||
|
|
@ -27791,7 +27798,7 @@ x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
|
|||
return x_6;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1() {
|
||||
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -27799,16 +27806,337 @@ x_1 = lean_mk_string("namedPattern");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2() {
|
||||
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_PrettyPrinter_Delaborator_maybeAddBlockImplicit___closed__7;
|
||||
x_2 = l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1;
|
||||
x_2 = l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_8; lean_object* x_9;
|
||||
x_8 = lean_ctor_get_uint8(x_1, sizeof(void*)*5);
|
||||
if (x_8 == 0)
|
||||
{
|
||||
lean_object* x_75; uint8_t x_76;
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_75 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_7);
|
||||
x_76 = !lean_is_exclusive(x_75);
|
||||
if (x_76 == 0)
|
||||
{
|
||||
return x_75;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_77; lean_object* x_78; lean_object* x_79;
|
||||
x_77 = lean_ctor_get(x_75, 0);
|
||||
x_78 = lean_ctor_get(x_75, 1);
|
||||
lean_inc(x_78);
|
||||
lean_inc(x_77);
|
||||
lean_dec(x_75);
|
||||
x_79 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_79, 0, x_77);
|
||||
lean_ctor_set(x_79, 1, x_78);
|
||||
return x_79;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
x_9 = x_7;
|
||||
goto block_74;
|
||||
}
|
||||
block_74:
|
||||
{
|
||||
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17;
|
||||
x_10 = l_Lean_PrettyPrinter_Delaborator_SubExpr_getExpr___at_Lean_PrettyPrinter_Delaborator_getExprKind___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_9);
|
||||
x_11 = lean_ctor_get(x_10, 0);
|
||||
lean_inc(x_11);
|
||||
x_12 = lean_ctor_get(x_10, 1);
|
||||
lean_inc(x_12);
|
||||
lean_dec(x_10);
|
||||
x_13 = lean_unsigned_to_nat(0u);
|
||||
x_14 = l_Lean_Expr_getAppNumArgsAux(x_11, x_13);
|
||||
lean_dec(x_11);
|
||||
x_15 = lean_unsigned_to_nat(3u);
|
||||
x_16 = lean_nat_dec_eq(x_14, x_15);
|
||||
lean_dec(x_14);
|
||||
if (x_16 == 0)
|
||||
{
|
||||
lean_object* x_69; uint8_t x_70;
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_69 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_12);
|
||||
x_70 = !lean_is_exclusive(x_69);
|
||||
if (x_70 == 0)
|
||||
{
|
||||
return x_69;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_71; lean_object* x_72; lean_object* x_73;
|
||||
x_71 = lean_ctor_get(x_69, 0);
|
||||
x_72 = lean_ctor_get(x_69, 1);
|
||||
lean_inc(x_72);
|
||||
lean_inc(x_71);
|
||||
lean_dec(x_69);
|
||||
x_73 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_73, 0, x_71);
|
||||
lean_ctor_set(x_73, 1, x_72);
|
||||
return x_73;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
x_17 = x_12;
|
||||
goto block_68;
|
||||
}
|
||||
block_68:
|
||||
{
|
||||
lean_object* x_18; lean_object* x_19;
|
||||
x_18 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__1;
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc(x_4);
|
||||
lean_inc(x_3);
|
||||
lean_inc(x_2);
|
||||
lean_inc(x_1);
|
||||
x_19 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabLetFun___spec__4(x_18, x_1, x_2, x_3, x_4, x_5, x_6, x_17);
|
||||
if (lean_obj_tag(x_19) == 0)
|
||||
{
|
||||
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
|
||||
x_20 = lean_ctor_get(x_19, 0);
|
||||
lean_inc(x_20);
|
||||
x_21 = lean_ctor_get(x_19, 1);
|
||||
lean_inc(x_21);
|
||||
lean_dec(x_19);
|
||||
x_22 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__4___closed__2;
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
x_23 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabLetFun___spec__1(x_22, x_1, x_2, x_3, x_4, x_5, x_6, x_21);
|
||||
if (lean_obj_tag(x_23) == 0)
|
||||
{
|
||||
lean_object* x_24; lean_object* x_25; uint8_t x_26;
|
||||
x_24 = lean_ctor_get(x_23, 0);
|
||||
lean_inc(x_24);
|
||||
x_25 = lean_ctor_get(x_23, 1);
|
||||
lean_inc(x_25);
|
||||
lean_dec(x_23);
|
||||
x_26 = l_Lean_Syntax_isIdent(x_20);
|
||||
if (x_26 == 0)
|
||||
{
|
||||
lean_object* x_27; uint8_t x_28;
|
||||
lean_dec(x_24);
|
||||
lean_dec(x_20);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
x_27 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_25);
|
||||
x_28 = !lean_is_exclusive(x_27);
|
||||
if (x_28 == 0)
|
||||
{
|
||||
return x_27;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_29; lean_object* x_30; lean_object* x_31;
|
||||
x_29 = lean_ctor_get(x_27, 0);
|
||||
x_30 = lean_ctor_get(x_27, 1);
|
||||
lean_inc(x_30);
|
||||
lean_inc(x_29);
|
||||
lean_dec(x_27);
|
||||
x_31 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_31, 0, x_29);
|
||||
lean_ctor_set(x_31, 1, x_30);
|
||||
return x_31;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_32; uint8_t x_33;
|
||||
x_32 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_PrettyPrinter_Delaborator_delab___spec__3___rarg(x_5, x_6, x_25);
|
||||
lean_dec(x_6);
|
||||
x_33 = !lean_is_exclusive(x_32);
|
||||
if (x_33 == 0)
|
||||
{
|
||||
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45;
|
||||
x_34 = lean_ctor_get(x_32, 0);
|
||||
x_35 = l_Lean_PrettyPrinter_Delaborator_maybeAddBlockImplicit___closed__10;
|
||||
x_36 = lean_alloc_ctor(2, 2, 0);
|
||||
lean_ctor_set(x_36, 0, x_34);
|
||||
lean_ctor_set(x_36, 1, x_35);
|
||||
x_37 = l_Lean_PrettyPrinter_Delaborator_delabConst___closed__14;
|
||||
x_38 = lean_array_push(x_37, x_20);
|
||||
x_39 = lean_array_push(x_38, x_36);
|
||||
x_40 = l_Lean_PrettyPrinter_Delaborator_delabSort___closed__13;
|
||||
x_41 = lean_array_push(x_39, x_40);
|
||||
x_42 = lean_array_push(x_41, x_24);
|
||||
x_43 = lean_box(2);
|
||||
x_44 = l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2;
|
||||
x_45 = lean_alloc_ctor(1, 3, 0);
|
||||
lean_ctor_set(x_45, 0, x_43);
|
||||
lean_ctor_set(x_45, 1, x_44);
|
||||
lean_ctor_set(x_45, 2, x_42);
|
||||
lean_ctor_set(x_32, 0, x_45);
|
||||
return x_32;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59;
|
||||
x_46 = lean_ctor_get(x_32, 0);
|
||||
x_47 = lean_ctor_get(x_32, 1);
|
||||
lean_inc(x_47);
|
||||
lean_inc(x_46);
|
||||
lean_dec(x_32);
|
||||
x_48 = l_Lean_PrettyPrinter_Delaborator_maybeAddBlockImplicit___closed__10;
|
||||
x_49 = lean_alloc_ctor(2, 2, 0);
|
||||
lean_ctor_set(x_49, 0, x_46);
|
||||
lean_ctor_set(x_49, 1, x_48);
|
||||
x_50 = l_Lean_PrettyPrinter_Delaborator_delabConst___closed__14;
|
||||
x_51 = lean_array_push(x_50, x_20);
|
||||
x_52 = lean_array_push(x_51, x_49);
|
||||
x_53 = l_Lean_PrettyPrinter_Delaborator_delabSort___closed__13;
|
||||
x_54 = lean_array_push(x_52, x_53);
|
||||
x_55 = lean_array_push(x_54, x_24);
|
||||
x_56 = lean_box(2);
|
||||
x_57 = l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2;
|
||||
x_58 = lean_alloc_ctor(1, 3, 0);
|
||||
lean_ctor_set(x_58, 0, x_56);
|
||||
lean_ctor_set(x_58, 1, x_57);
|
||||
lean_ctor_set(x_58, 2, x_55);
|
||||
x_59 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_59, 0, x_58);
|
||||
lean_ctor_set(x_59, 1, x_47);
|
||||
return x_59;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_60;
|
||||
lean_dec(x_20);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
x_60 = !lean_is_exclusive(x_23);
|
||||
if (x_60 == 0)
|
||||
{
|
||||
return x_23;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_61; lean_object* x_62; lean_object* x_63;
|
||||
x_61 = lean_ctor_get(x_23, 0);
|
||||
x_62 = lean_ctor_get(x_23, 1);
|
||||
lean_inc(x_62);
|
||||
lean_inc(x_61);
|
||||
lean_dec(x_23);
|
||||
x_63 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_63, 0, x_61);
|
||||
lean_ctor_set(x_63, 1, x_62);
|
||||
return x_63;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_64;
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_64 = !lean_is_exclusive(x_19);
|
||||
if (x_64 == 0)
|
||||
{
|
||||
return x_19;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_65; lean_object* x_66; lean_object* x_67;
|
||||
x_65 = lean_ctor_get(x_19, 0);
|
||||
x_66 = lean_ctor_get(x_19, 1);
|
||||
lean_inc(x_66);
|
||||
lean_inc(x_65);
|
||||
lean_dec(x_19);
|
||||
x_67 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_67, 0, x_65);
|
||||
lean_ctor_set(x_67, 1, x_66);
|
||||
return x_67;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("namedPatternOld");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppExplicit___closed__2;
|
||||
x_2 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("delabNamedPatternOld");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar___closed__6;
|
||||
x_2 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__3;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld), 7, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_2 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar___closed__9;
|
||||
x_3 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2;
|
||||
x_4 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__4;
|
||||
x_5 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__5;
|
||||
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPattern(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -27977,7 +28305,7 @@ x_40 = l_Lean_PrettyPrinter_Delaborator_delabSort___closed__13;
|
|||
x_41 = lean_array_push(x_39, x_40);
|
||||
x_42 = lean_array_push(x_41, x_24);
|
||||
x_43 = lean_box(2);
|
||||
x_44 = l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2;
|
||||
x_44 = l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2;
|
||||
x_45 = lean_alloc_ctor(1, 3, 0);
|
||||
lean_ctor_set(x_45, 0, x_43);
|
||||
lean_ctor_set(x_45, 1, x_44);
|
||||
|
|
@ -28004,7 +28332,7 @@ x_53 = l_Lean_PrettyPrinter_Delaborator_delabSort___closed__13;
|
|||
x_54 = lean_array_push(x_52, x_53);
|
||||
x_55 = lean_array_push(x_54, x_24);
|
||||
x_56 = lean_box(2);
|
||||
x_57 = l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2;
|
||||
x_57 = l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2;
|
||||
x_58 = lean_alloc_ctor(1, 3, 0);
|
||||
lean_ctor_set(x_58, 0, x_56);
|
||||
lean_ctor_set(x_58, 1, x_57);
|
||||
|
|
@ -28079,7 +28407,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppExplicit___closed__2;
|
||||
x_2 = l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1;
|
||||
x_2 = l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -29808,7 +30136,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_PrettyPrinter_Delaborator_delabFVar___closed__1;
|
||||
x_2 = l_Lean_PrettyPrinter_Delaborator_delabDoElems___closed__5;
|
||||
x_3 = lean_unsigned_to_nat(736u);
|
||||
x_3 = lean_unsigned_to_nat(746u);
|
||||
x_4 = lean_unsigned_to_nat(40u);
|
||||
x_5 = l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__3;
|
||||
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
|
||||
|
|
@ -32239,10 +32567,23 @@ lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabDIte___c
|
|||
res = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabDIte(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1 = _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1();
|
||||
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1);
|
||||
l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2 = _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2();
|
||||
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2);
|
||||
l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1 = _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1();
|
||||
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1);
|
||||
l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2 = _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2();
|
||||
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2);
|
||||
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1);
|
||||
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2);
|
||||
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__3 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__3();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__3);
|
||||
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__4 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__4();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__4);
|
||||
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__5 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__5();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__5);
|
||||
res = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1);
|
||||
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2();
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue