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-09-28 16:41:00 -07:00
parent e10edde5cd
commit cb04d66c2f
5 changed files with 16791 additions and 12780 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
stage0/src/Lean/Parser/Term.lean generated
View file

@ -79,9 +79,9 @@ def optIdent : Parser := optional (try (ident >> " : "))
def fromTerm := parser! " from " >> termParser
def haveAssign := parser! " := " >> termParser
def haveDecl := optIdent >> termParser >> (haveAssign <|> fromTerm <|> byTactic)
@[builtinTermParser] def «have» := parser!:leadPrec "have " >> haveDecl >> "; " >> termParser
@[builtinTermParser] def «have» := parser!:leadPrec withPosition ("have " >> haveDecl) >> optional "; " >> termParser
def sufficesDecl := optIdent >> termParser >> fromTerm
@[builtinTermParser] def «suffices» := parser!:leadPrec "suffices " >> sufficesDecl >> "; " >> termParser
@[builtinTermParser] def «suffices» := parser!:leadPrec withPosition ("suffices " >> sufficesDecl) >> optional "; " >> termParser
@[builtinTermParser] def «show» := parser!:leadPrec "show " >> termParser >> (fromTerm <|> byTactic)
def structInstArrayRef := parser! "[" >> termParser >>"]"
def structInstLVal := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
@ -156,14 +156,15 @@ def letPatDecl := node `Lean.Parser.Term.letPatDecl $ try (termParser >> pushN
def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts false
-- Remark: we use `nodeWithAntiquot` here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl`
def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") >> (letIdDecl <|> letPatDecl <|> letEqnsDecl))
@[builtinTermParser] def «let» := parser!:leadPrec "let " >> letDecl >> "; " >> termParser
@[builtinTermParser] def «let!» := parser!:leadPrec "let! " >> letDecl >> "; " >> termParser
@[builtinTermParser] def «let» := parser!:leadPrec withPosition ("let " >> letDecl) >> optional "; " >> termParser
@[builtinTermParser] def «let!» := parser!:leadPrec withPosition ("let! " >> letDecl) >> optional "; " >> termParser
def attrArg : Parser := ident <|> strLit <|> numLit
-- use `rawIdent` because of attribute names such as `instance`
def attrInstance := parser! rawIdent >> many attrArg
def attributes := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
@[builtinTermParser] def «letrec» :=
parser!:leadPrec group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser
parser!:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", ")
>> optional "; " >> termParser
@[builtinTermParser] def nativeRefl := parser! "nativeRefl! " >> termParser maxPrec
@[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser maxPrec
@ -197,6 +198,7 @@ stx.isAntiquot || stx.isIdent
@[builtinTermParser] def dollar := tparser!:0 try (dollarSymbol >> checkWsBefore "expected space") >> termParser 0
@[builtinTermParser] def dollarProj := tparser!:0 " $. " >> (fieldIdx <|> ident)
-- TODO: fix
@[builtinTermParser] def «where» := tparser!:0 " where " >> sepBy1 letDecl (group ("; " >> symbol " where "))
@[builtinTermParser] def fcomp := tparser! infixR " ∘ " 90
@ -249,8 +251,8 @@ stx.isAntiquot || stx.isIdent
@[builtinTermParser] def panic := parser!:leadPrec "panic! " >> termParser
@[builtinTermParser] def unreachable := parser!:leadPrec "unreachable!"
@[builtinTermParser] def dbgTrace := parser!:leadPrec "dbgTrace! " >> termParser >> "; " >> termParser
@[builtinTermParser] def assert := parser!:leadPrec "assert! " >> termParser >> "; " >> termParser
@[builtinTermParser] def dbgTrace := parser!:leadPrec withPosition ("dbgTrace! " >> termParser) >> optional "; " >> termParser
@[builtinTermParser] def assert := parser!:leadPrec withPosition ("assert! " >> termParser) >> optional "; " >> termParser
@[builtinTermParser] def «return» := parser!:leadPrec "return " >> termParser
end Term

19517
stage0/stdlib/Lean/Elab/App.c generated
View file

File diff suppressed because it is too large Load diff

169
stage0/stdlib/Lean/Parser/Do.c generated
View file

@ -24,11 +24,9 @@ lean_object* l_Lean_Parser_Term_liftMethod_parenthesizer(lean_object*, lean_obje
lean_object* l_Lean_Parser_Term_doSeqBracketed_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__9;
lean_object* l_Lean_Parser_many1Indent_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_have_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doPat_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_doElemParser(lean_object*);
lean_object* l_Lean_Parser_Term_doSeqBracketed___closed__1;
lean_object* l_Lean_Parser_Term_doLet___closed__6;
lean_object* l_Lean_Parser_Term_doMatch_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Term_doSeqBracketed___closed__2;
extern lean_object* l_Lean_Parser_manyAux___main___closed__1;
@ -81,6 +79,7 @@ lean_object* l_Lean_Parser_Term_doExpr___closed__4;
extern lean_object* l_Lean_Parser_many1Indent_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_doMatchAlt_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Term_liftMethod(lean_object*);
extern lean_object* l_Lean_Parser_Term_have___closed__2;
extern lean_object* l_Lean_Parser_Term_if_formatter___closed__3;
lean_object* l_Lean_Parser_Term_doExpr_formatter___closed__10;
lean_object* l_Lean_Parser_Term_do___elambda__1___closed__1;
@ -136,7 +135,6 @@ extern lean_object* l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_do___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_doMatch___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_liftMethod___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doLet_formatter___closed__3;
lean_object* l_Lean_Parser_Term_doMatchAlts___elambda__1___closed__3;
lean_object* l___regBuiltinParser_Lean_Parser_Term_do(lean_object*);
lean_object* l_Lean_Parser_Term_doMatchAlt___closed__1;
@ -240,6 +238,7 @@ lean_object* l_Lean_Parser_Term_doMatchAlt___elambda__1(lean_object*, lean_objec
extern lean_object* l_Lean_Parser_Term_if___closed__3;
extern lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute;
lean_object* l_Lean_Parser_Term_liftMethod_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_let___closed__2;
lean_object* l_Lean_Parser_Term_leftArrow_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doSeq_formatter___closed__1;
lean_object* l_Lean_Parser_Term_break___elambda__1(lean_object*, lean_object*);
@ -315,7 +314,6 @@ uint8_t l_Lean_Parser_tryAnti(lean_object*, lean_object*);
lean_object* l_Lean_Parser_optionaInfo(lean_object*);
lean_object* l_Lean_Parser_Term_doSeq;
extern lean_object* l_Lean_Parser_Term_let___elambda__1___closed__6;
extern lean_object* l_Lean_Parser_Term_let_parenthesizer___closed__2;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_sepBy1_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doMatch___closed__3;
lean_object* l_Lean_Parser_Term_do___closed__6;
@ -324,7 +322,6 @@ lean_object* l_Lean_Parser_Term_doHave_formatter___closed__1;
lean_object* l_Lean_Parser_Term_doId___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_doSeqIndent___closed__4;
lean_object* l_Lean_Parser_Term_doLetArrow___closed__6;
extern lean_object* l_Lean_Parser_Term_have_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Term_doId_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__13;
lean_object* l_Lean_PrettyPrinter_Formatter_unicodeSymbol_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -334,14 +331,12 @@ extern lean_object* l_Lean_Parser_many1Indent_formatter___closed__1;
lean_object* l_Lean_Parser_Term_doIf___closed__3;
extern lean_object* l_Lean_Parser_Term_funImplicitBinder_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_doMatchAlts_formatter___closed__4;
lean_object* l_Lean_Parser_Term_doLet_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Term_doFor_formatter___closed__3;
lean_object* l___regBuiltinParser_Lean_Parser_Term_doIf(lean_object*);
lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_doPat_formatter___closed__6;
lean_object* l___regBuiltin_Lean_Parser_Term_break_formatter(lean_object*);
lean_object* l_Lean_Parser_doElemParser_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doHave_parenthesizer___closed__3;
extern lean_object* l_Char_HasRepr___closed__1;
lean_object* l_Lean_Parser_Term_doSeqIndent___closed__5;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__24;
@ -446,7 +441,6 @@ lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_doMatchAlts___elambda__1___spec__1(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doMatch___closed__8;
lean_object* l___regBuiltin_Lean_Parser_Term_doLet_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Term_doHave_formatter___closed__3;
lean_object* l_Lean_Parser_Term_doLetArrow_formatter___closed__3;
lean_object* l_Lean_Parser_Term_doIf___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__15;
@ -488,6 +482,7 @@ lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__7;
extern lean_object* l_Lean_Parser_Term_if___elambda__1___closed__19;
lean_object* l_Lean_Parser_Term_doSeqBracketed_parenthesizer___closed__6;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__22;
extern lean_object* l_Lean_Parser_Term_let_formatter___closed__4;
lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_doFor___closed__6;
lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__16;
@ -523,7 +518,6 @@ lean_object* l_Lean_Parser_Term_doFor___closed__10;
lean_object* l_Lean_Parser_Term_doLetArrow_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Term_doLetArrow_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doLetArrow___closed__7;
extern lean_object* l_Lean_Parser_Term_haveDecl;
extern lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_doHave___closed__4;
lean_object* l_Lean_Parser_Term_liftMethod_parenthesizer___closed__1;
@ -565,7 +559,6 @@ lean_object* l_Lean_Parser_Term_doId___closed__7;
lean_object* l_Lean_Parser_Term_doId_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doSeqBracketed_parenthesizer___closed__4;
extern lean_object* l_Lean_Parser_Term_have___elambda__1___closed__9;
extern lean_object* l_Lean_Parser_Term_have___closed__1;
lean_object* l_Lean_Parser_Term_doExpr_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Term_doMatchAlts___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doExpr_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -584,7 +577,6 @@ lean_object* l_Lean_Parser_Term_continue___closed__1;
lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__5;
extern lean_object* l_Lean_Parser_Term_if___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__11;
extern lean_object* l_Lean_Parser_Term_let_formatter___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Term_doMatch_parenthesizer(lean_object*);
extern lean_object* l_Lean_Parser_Term_matchAlts___closed__9;
lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__3;
@ -656,13 +648,13 @@ lean_object* l_Lean_Parser_Term_doIf___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_doLet___closed__4;
lean_object* l_Lean_Parser_Term_break_formatter___closed__3;
lean_object* l_Lean_Parser_Term_doMatchAlt_formatter___closed__1;
extern lean_object* l_Lean_Parser_Term_let_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Term_doMatch_formatter___closed__3;
lean_object* l_Lean_Parser_Term_leftArrow___closed__2;
lean_object* l_Lean_Parser_Term_doMatchAlt___closed__2;
lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_doIf_formatter___closed__7;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__21;
lean_object* l_Lean_Parser_Term_doHave___closed__6;
extern lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___spec__2___closed__5;
lean_object* l_Lean_Parser_Term_doPat_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Term_doLet___closed__2;
@ -763,6 +755,7 @@ lean_object* l_Lean_Parser_Term_leftArrow___elambda__1(lean_object*, lean_object
lean_object* l_Lean_Parser_Term_continue_formatter___closed__3;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__8;
lean_object* l_Lean_Parser_unicodeSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_have_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Term_doMatchAlts___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_break___closed__2;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__17;
@ -3390,48 +3383,36 @@ return x_76;
lean_object* _init_l_Lean_Parser_Term_doLet___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_letDecl;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_let___closed__1;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_doLet___elambda__1___closed__2;
x_2 = l_Lean_Parser_Term_let___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doLet___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_doLet___elambda__1___closed__2;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Term_doLet___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doLet___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Term_doLet___closed__2;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doLet___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_doLet___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_doLet___closed__3;
x_3 = l_Lean_Parser_Term_doLet___closed__2;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Term_doLet___closed__5() {
lean_object* _init_l_Lean_Parser_Term_doLet___closed__4() {
_start:
{
lean_object* x_1;
@ -3439,12 +3420,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_doLet___elambda__1), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_doLet___closed__6() {
lean_object* _init_l_Lean_Parser_Term_doLet___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_doLet___closed__4;
x_2 = l_Lean_Parser_Term_doLet___closed__5;
x_1 = l_Lean_Parser_Term_doLet___closed__3;
x_2 = l_Lean_Parser_Term_doLet___closed__4;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -3455,7 +3436,7 @@ lean_object* _init_l_Lean_Parser_Term_doLet() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Term_doLet___closed__6;
x_1 = l_Lean_Parser_Term_doLet___closed__5;
return x_1;
}
}
@ -3490,22 +3471,10 @@ return x_5;
lean_object* _init_l_Lean_Parser_Term_doLet_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_let_formatter___closed__2;
x_2 = l_Lean_Parser_Term_let_formatter___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doLet_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_doLet___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_doLet_formatter___closed__2;
x_3 = l_Lean_Parser_Term_let_formatter___closed__4;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -3518,7 +3487,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Term_doLet_formatter___closed__1;
x_7 = l_Lean_Parser_Term_doLet_formatter___closed__3;
x_7 = l_Lean_Parser_Term_doLet_formatter___closed__2;
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -3558,22 +3527,10 @@ return x_4;
lean_object* _init_l_Lean_Parser_Term_doLet_parenthesizer___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Term_let_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doLet_parenthesizer___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_doLet___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_doLet_parenthesizer___closed__2;
x_3 = l_Lean_Parser_Term_let_parenthesizer___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -3586,7 +3543,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Term_doLet_parenthesizer___closed__1;
x_7 = l_Lean_Parser_Term_doLet_parenthesizer___closed__3;
x_7 = l_Lean_Parser_Term_doLet_parenthesizer___closed__2;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -6380,48 +6337,36 @@ return x_74;
lean_object* _init_l_Lean_Parser_Term_doHave___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_haveDecl;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_have___closed__1;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_doHave___elambda__1___closed__2;
x_2 = l_Lean_Parser_Term_have___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doHave___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_doHave___elambda__1___closed__2;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Term_doHave___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doHave___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Term_doHave___closed__2;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doHave___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_doHave___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_doHave___closed__3;
x_3 = l_Lean_Parser_Term_doHave___closed__2;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Term_doHave___closed__5() {
lean_object* _init_l_Lean_Parser_Term_doHave___closed__4() {
_start:
{
lean_object* x_1;
@ -6429,12 +6374,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_doHave___elambda__1), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_doHave___closed__6() {
lean_object* _init_l_Lean_Parser_Term_doHave___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_doHave___closed__4;
x_2 = l_Lean_Parser_Term_doHave___closed__5;
x_1 = l_Lean_Parser_Term_doHave___closed__3;
x_2 = l_Lean_Parser_Term_doHave___closed__4;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -6445,7 +6390,7 @@ lean_object* _init_l_Lean_Parser_Term_doHave() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Term_doHave___closed__6;
x_1 = l_Lean_Parser_Term_doHave___closed__5;
return x_1;
}
}
@ -6480,22 +6425,10 @@ return x_5;
lean_object* _init_l_Lean_Parser_Term_doHave_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_have_formatter___closed__2;
x_2 = l_Lean_Parser_Term_have_formatter___closed__4;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doHave_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_doHave___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_doHave_formatter___closed__2;
x_3 = l_Lean_Parser_Term_have_formatter___closed__4;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -6508,7 +6441,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Term_doHave_formatter___closed__1;
x_7 = l_Lean_Parser_Term_doHave_formatter___closed__3;
x_7 = l_Lean_Parser_Term_doHave_formatter___closed__2;
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -6548,22 +6481,10 @@ return x_4;
lean_object* _init_l_Lean_Parser_Term_doHave_parenthesizer___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Term_have_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doHave_parenthesizer___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_doHave___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_doHave_parenthesizer___closed__2;
x_3 = l_Lean_Parser_Term_have_parenthesizer___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -6576,7 +6497,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Term_doHave_parenthesizer___closed__1;
x_7 = l_Lean_Parser_Term_doHave_parenthesizer___closed__3;
x_7 = l_Lean_Parser_Term_doHave_parenthesizer___closed__2;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -17565,8 +17486,6 @@ l_Lean_Parser_Term_doLet___closed__4 = _init_l_Lean_Parser_Term_doLet___closed__
lean_mark_persistent(l_Lean_Parser_Term_doLet___closed__4);
l_Lean_Parser_Term_doLet___closed__5 = _init_l_Lean_Parser_Term_doLet___closed__5();
lean_mark_persistent(l_Lean_Parser_Term_doLet___closed__5);
l_Lean_Parser_Term_doLet___closed__6 = _init_l_Lean_Parser_Term_doLet___closed__6();
lean_mark_persistent(l_Lean_Parser_Term_doLet___closed__6);
l_Lean_Parser_Term_doLet = _init_l_Lean_Parser_Term_doLet();
lean_mark_persistent(l_Lean_Parser_Term_doLet);
res = l___regBuiltinParser_Lean_Parser_Term_doLet(lean_io_mk_world());
@ -17576,8 +17495,6 @@ l_Lean_Parser_Term_doLet_formatter___closed__1 = _init_l_Lean_Parser_Term_doLet_
lean_mark_persistent(l_Lean_Parser_Term_doLet_formatter___closed__1);
l_Lean_Parser_Term_doLet_formatter___closed__2 = _init_l_Lean_Parser_Term_doLet_formatter___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_doLet_formatter___closed__2);
l_Lean_Parser_Term_doLet_formatter___closed__3 = _init_l_Lean_Parser_Term_doLet_formatter___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_doLet_formatter___closed__3);
l___regBuiltin_Lean_Parser_Term_doLet_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Term_doLet_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_doLet_formatter___closed__1);
res = l___regBuiltin_Lean_Parser_Term_doLet_formatter(lean_io_mk_world());
@ -17587,8 +17504,6 @@ l_Lean_Parser_Term_doLet_parenthesizer___closed__1 = _init_l_Lean_Parser_Term_do
lean_mark_persistent(l_Lean_Parser_Term_doLet_parenthesizer___closed__1);
l_Lean_Parser_Term_doLet_parenthesizer___closed__2 = _init_l_Lean_Parser_Term_doLet_parenthesizer___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_doLet_parenthesizer___closed__2);
l_Lean_Parser_Term_doLet_parenthesizer___closed__3 = _init_l_Lean_Parser_Term_doLet_parenthesizer___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_doLet_parenthesizer___closed__3);
l___regBuiltin_Lean_Parser_Term_doLet_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Term_doLet_parenthesizer___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_doLet_parenthesizer___closed__1);
res = l___regBuiltin_Lean_Parser_Term_doLet_parenthesizer(lean_io_mk_world());
@ -17795,8 +17710,6 @@ l_Lean_Parser_Term_doHave___closed__4 = _init_l_Lean_Parser_Term_doHave___closed
lean_mark_persistent(l_Lean_Parser_Term_doHave___closed__4);
l_Lean_Parser_Term_doHave___closed__5 = _init_l_Lean_Parser_Term_doHave___closed__5();
lean_mark_persistent(l_Lean_Parser_Term_doHave___closed__5);
l_Lean_Parser_Term_doHave___closed__6 = _init_l_Lean_Parser_Term_doHave___closed__6();
lean_mark_persistent(l_Lean_Parser_Term_doHave___closed__6);
l_Lean_Parser_Term_doHave = _init_l_Lean_Parser_Term_doHave();
lean_mark_persistent(l_Lean_Parser_Term_doHave);
res = l___regBuiltinParser_Lean_Parser_Term_doHave(lean_io_mk_world());
@ -17806,8 +17719,6 @@ l_Lean_Parser_Term_doHave_formatter___closed__1 = _init_l_Lean_Parser_Term_doHav
lean_mark_persistent(l_Lean_Parser_Term_doHave_formatter___closed__1);
l_Lean_Parser_Term_doHave_formatter___closed__2 = _init_l_Lean_Parser_Term_doHave_formatter___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_doHave_formatter___closed__2);
l_Lean_Parser_Term_doHave_formatter___closed__3 = _init_l_Lean_Parser_Term_doHave_formatter___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_doHave_formatter___closed__3);
l___regBuiltin_Lean_Parser_Term_doHave_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Term_doHave_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_doHave_formatter___closed__1);
res = l___regBuiltin_Lean_Parser_Term_doHave_formatter(lean_io_mk_world());
@ -17817,8 +17728,6 @@ l_Lean_Parser_Term_doHave_parenthesizer___closed__1 = _init_l_Lean_Parser_Term_d
lean_mark_persistent(l_Lean_Parser_Term_doHave_parenthesizer___closed__1);
l_Lean_Parser_Term_doHave_parenthesizer___closed__2 = _init_l_Lean_Parser_Term_doHave_parenthesizer___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_doHave_parenthesizer___closed__2);
l_Lean_Parser_Term_doHave_parenthesizer___closed__3 = _init_l_Lean_Parser_Term_doHave_parenthesizer___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_doHave_parenthesizer___closed__3);
l___regBuiltin_Lean_Parser_Term_doHave_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Term_doHave_parenthesizer___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_doHave_parenthesizer___closed__1);
res = l___regBuiltin_Lean_Parser_Term_doHave_parenthesizer(lean_io_mk_world());

324
stage0/stdlib/Lean/Parser/Tactic.c generated
View file

@ -17,7 +17,6 @@ lean_object* l_Lean_Parser_Tactic_location___elambda__1___closed__8;
lean_object* l_Lean_Parser_Tactic_locationWildcard___elambda__1___closed__7;
lean_object* l_Lean_Parser_Tactic_orelse___closed__4;
lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__7;
lean_object* l_Lean_Parser_Tactic_let_parenthesizer___closed__3;
extern lean_object* l_Lean_Parser_Term_match___elambda__1___closed__6;
lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__4;
lean_object* l_Lean_Parser_Tactic_rwRuleSeq___closed__1;
@ -50,7 +49,6 @@ lean_object* l_Lean_Parser_Tactic_induction___closed__1;
lean_object* l_Lean_Parser_Tactic_skip_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_intros_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_generalize___closed__8;
extern lean_object* l_Lean_Parser_Term_have_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_cases___closed__6;
lean_object* l___regBuiltin_Lean_Parser_Tactic_allGoals_formatter(lean_object*);
lean_object* l_Lean_Parser_Tactic_rewrite_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -71,7 +69,6 @@ lean_object* l_Lean_Parser_Tactic_withIds___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Tactic_skip_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_revert___closed__2;
lean_object* l_Lean_Parser_Tactic_admit___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Term_suffices___closed__1;
lean_object* l_Lean_Parser_Tactic_changeWith_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_rewrite_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_let___elambda__1(lean_object*, lean_object*);
@ -100,6 +97,7 @@ lean_object* l_Lean_Parser_Tactic_induction_formatter___closed__10;
lean_object* l_Lean_Parser_Tactic_admit_formatter___closed__3;
extern lean_object* l_Lean_Parser_Term_explicit___closed__2;
lean_object* l_Lean_Parser_Tactic_traceState_parenthesizer___closed__1;
extern lean_object* l_Lean_Parser_Term_suffices_parenthesizer___closed__3;
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_have(lean_object*);
extern lean_object* l_Lean_Parser_Term_matchAlt___closed__3;
lean_object* l_Lean_Parser_Tactic_nestedTactic;
@ -130,6 +128,7 @@ lean_object* l_Lean_Parser_Tactic_matchAlts_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_orelse___closed__1;
lean_object* l_Lean_Parser_Tactic_failIfSuccess___closed__6;
lean_object* l___regBuiltin_Lean_Parser_Tactic_orelse_parenthesizer___closed__1;
extern lean_object* l_Lean_Parser_Term_suffices___closed__2;
lean_object* l_Lean_Parser_Tactic_underscore___closed__2;
lean_object* l_Lean_Parser_Tactic_location___closed__7;
lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__9;
@ -164,6 +163,7 @@ lean_object* l_Lean_Parser_Tactic_rwRuleSeq___closed__8;
lean_object* l_Lean_Parser_Tactic_skip___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Tactic_exact_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_matchAlts___closed__5;
extern lean_object* l_Lean_Parser_Term_have___closed__2;
lean_object* l_Lean_Parser_Tactic_induction___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Tactic_apply_parenthesizer___closed__1;
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_admit(lean_object*);
@ -306,7 +306,6 @@ lean_object* l_Lean_Parser_Tactic_inductionAlt_formatter(lean_object*, lean_obje
lean_object* l_Lean_Parser_Tactic_rewrite___elambda__1___closed__5;
lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__7;
lean_object* l___regBuiltin_Lean_Parser_Tactic_rewriteSeq_parenthesizer(lean_object*);
extern lean_object* l_Lean_Parser_Term_let_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_clear___elambda__1___closed__5;
lean_object* l_Lean_Parser_Tactic_change_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_paren___elambda__1(lean_object*, lean_object*);
@ -318,7 +317,6 @@ lean_object* l_Lean_Parser_Tactic_location_formatter___closed__5;
lean_object* l_Lean_Parser_Tactic_rwRuleSeq___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_refine___closed__5;
lean_object* l_Lean_Parser_Tactic_majorPremise___elambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_suffices_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_rwRule_formatter___closed__5;
extern lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___spec__2___closed__2;
lean_object* l_Lean_Parser_Tactic_failIfSuccess___elambda__1___closed__1;
@ -365,7 +363,6 @@ lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Tactic_matchAlt___closed__4;
lean_object* l_Lean_PrettyPrinter_Formatter_try_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_done_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_have___closed__6;
lean_object* l_Lean_Parser_Tactic_location_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_cases___closed__3;
@ -373,7 +370,6 @@ extern lean_object* l_Lean_Parser_Term_eq___elambda__1___closed__3;
lean_object* l_Lean_Parser_Tactic_inductionAlts_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_failIfSuccess___elambda__1___closed__2;
lean_object* l_Lean_Parser_Tactic_clear_formatter___closed__4;
lean_object* l_Lean_Parser_Tactic_suffices___closed__6;
lean_object* l_Lean_Parser_Tactic_change_parenthesizer___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Tactic_orelse_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Tactic_usingRec;
@ -397,6 +393,7 @@ lean_object* l_Lean_Parser_mkAntiquot_formatter___boxed(lean_object*, lean_objec
lean_object* l_Lean_Parser_Tactic_assumption_parenthesizer___closed__1;
lean_object* l_Lean_Parser_leadingNode_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_generalize___closed__3;
extern lean_object* l_Lean_Parser_Term_let_x21_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_orelse___closed__5;
lean_object* l_Lean_Parser_Tactic_withIds;
lean_object* l_Lean_Parser_Tactic_suffices___closed__4;
@ -476,7 +473,6 @@ lean_object* l_Lean_PrettyPrinter_Formatter_optional_formatter(lean_object*, lea
lean_object* l_Lean_Parser_Tactic_change___elambda__1___closed__7;
extern lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__3;
lean_object* l_Lean_Parser_Tactic_cases_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_suffices_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_rwRuleSeq_formatter___closed__5;
lean_object* l_Lean_Parser_Tactic_subst___closed__1;
lean_object* l_Lean_Parser_Tactic_withIds_formatter___closed__1;
@ -527,6 +523,7 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_rewriteSeq_formatter(lean_object*
lean_object* l_Lean_Parser_Tactic_assumption;
lean_object* l_Lean_Parser_Tactic_skip_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_intros___elambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_let___closed__2;
lean_object* l_Lean_Parser_Tactic_cases___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_subst___closed__2;
lean_object* l_Lean_Parser_Tactic_rewrite;
@ -545,7 +542,6 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_injection_parenthesizer___closed_
lean_object* l_Lean_Parser_Tactic_changeWith_formatter___closed__5;
lean_object* l_Lean_Parser_Tactic_refine_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_failIfSuccess_formatter___closed__1;
extern lean_object* l_Lean_Parser_Term_let___closed__1;
lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__8;
lean_object* l_Lean_Parser_Tactic_location_formatter___closed__6;
lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__10;
@ -641,7 +637,6 @@ lean_object* l_Lean_Parser_Tactic_apply___closed__3;
lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Tactic_clear___closed__5;
lean_object* l_Lean_Parser_Tactic_generalizingVars_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_let_x21_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_locationHyp___closed__5;
lean_object* l_Lean_Parser_Tactic_show___closed__6;
lean_object* l_Lean_Parser_Tactic_location_formatter___closed__1;
@ -724,8 +719,6 @@ lean_object* l_Lean_Parser_Tactic_locationHyp_formatter___closed__1;
lean_object* l_Lean_Parser_optionaInfo(lean_object*);
extern lean_object* l_Lean_Parser_Term_let___elambda__1___closed__6;
lean_object* l_Lean_Parser_Tactic_cases___closed__2;
extern lean_object* l_Lean_Parser_Term_let_parenthesizer___closed__2;
extern lean_object* l_Lean_Parser_Term_sufficesDecl;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_sepBy1_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_generalize___elambda__1(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Tactic_suffices_parenthesizer(lean_object*);
@ -739,7 +732,6 @@ lean_object* l_Lean_Parser_Tactic_induction_formatter___closed__7;
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_changeWith(lean_object*);
lean_object* l_Lean_Parser_Tactic_induction___closed__7;
lean_object* l_Lean_Parser_Tactic_revert___closed__5;
extern lean_object* l_Lean_Parser_Term_have_parenthesizer___closed__2;
lean_object* l_Lean_PrettyPrinter_Formatter_node_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_suffices___elambda__1___closed__9;
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
@ -1095,6 +1087,7 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_refine_formatter(lean_object*);
lean_object* l_Lean_Parser_Tactic_intros___closed__9;
lean_object* l_Lean_Parser_Tactic_withIds___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_location___closed__9;
extern lean_object* l_Lean_Parser_Term_let_formatter___closed__4;
lean_object* l_Lean_Parser_Tactic_case_parenthesizer___closed__1;
lean_object* l_Lean_Parser_nodeWithAntiquot_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_injection___elambda__1___closed__1;
@ -1158,7 +1151,6 @@ lean_object* l_Lean_Parser_Tactic_locationTarget_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_matchAlt_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Term_haveDecl;
lean_object* l___regBuiltin_Lean_Parser_Tactic_nestedTactic_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__8;
lean_object* l_Lean_Parser_Tactic_match___closed__5;
@ -1170,7 +1162,6 @@ lean_object* l_Lean_Parser_Tactic_suffices___elambda__1(lean_object*, lean_objec
lean_object* l_Lean_Parser_Tactic_induction___closed__6;
lean_object* l_Lean_Parser_Tactic_admit___closed__6;
lean_object* l_Lean_Parser_Tactic_subst_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_have_formatter___closed__3;
extern lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_tupleTail___elambda__1___spec__2___closed__1;
lean_object* l_Lean_Parser_Tactic_orelse_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_skip_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1198,7 +1189,6 @@ lean_object* l_Lean_Parser_Tactic_injection_formatter(lean_object*, lean_object*
lean_object* l_Lean_Parser_Tactic_cases___elambda__1___closed__3;
lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__12;
lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__4;
lean_object* l_Lean_Parser_Tactic_have_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Tactic_have___elambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_let___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_revert___elambda__1___closed__3;
@ -1219,7 +1209,6 @@ lean_object* l_Lean_Parser_Tactic_generalize_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_revert___closed__7;
lean_object* l_Lean_Parser_Tactic_matchAlt_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Tactic_allGoals___closed__5;
extern lean_object* l_Lean_Parser_Term_suffices_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_match_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_paren___closed__6;
extern lean_object* l_Lean_Parser_Term_match___elambda__1___closed__9;
@ -1233,10 +1222,8 @@ lean_object* l_Lean_Parser_Tactic_show_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_rewriteSeq___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_rwRule_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_refine_x21___elambda__1___closed__7;
lean_object* l_Lean_Parser_Tactic_let___closed__6;
lean_object* l_Lean_Parser_Tactic_cases_parenthesizer___closed__1;
extern lean_object* l_Lean_Parser_Term_have___elambda__1___closed__9;
extern lean_object* l_Lean_Parser_Term_have___closed__1;
extern lean_object* l_Lean_Parser_darrow___closed__2;
lean_object* l_Lean_Parser_Tactic_failIfSuccess___closed__4;
lean_object* l_Lean_Parser_Tactic_assumption_formatter___closed__2;
@ -1262,7 +1249,6 @@ extern lean_object* l_Lean_Parser_Tactic_tacticSeq;
lean_object* l_Lean_Parser_Tactic_revert___elambda__1___closed__5;
lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__6;
lean_object* l_Lean_Parser_Tactic_exact_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_let_x21___closed__6;
lean_object* l_Lean_Parser_Tactic_match___elambda__1___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Tactic_changeWith_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_case___closed__8;
@ -1282,7 +1268,6 @@ lean_object* l_Lean_Parser_Tactic_done___closed__1;
lean_object* l_Lean_Parser_Tactic_locationWildcard___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__7;
lean_object* l___regBuiltin_Lean_Parser_Tactic_show_parenthesizer(lean_object*);
extern lean_object* l_Lean_Parser_Term_let_formatter___closed__3;
lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__2(uint8_t, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__11;
extern lean_object* l_Lean_Parser_Term_matchAlts___closed__9;
@ -1373,7 +1358,6 @@ lean_object* l_Lean_Parser_Tactic_done___closed__4;
lean_object* l_Lean_Parser_Tactic_locationHyp___elambda__1___closed__4;
lean_object* l_String_trim(lean_object*);
lean_object* l_Lean_Parser_Tactic_allGoals_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_let_formatter___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Tactic_traceState_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_withIds_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_change_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1404,6 +1388,7 @@ lean_object* l_Lean_Parser_Tactic_let___elambda__1___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Tactic_intro_formatter(lean_object*);
lean_object* l_Lean_Parser_Tactic_show___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_generalize_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_let_parenthesizer___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Tactic_refine_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_injection_formatter___closed__4;
lean_object* l_Lean_Parser_Tactic_generalize___closed__7;
@ -1447,6 +1432,7 @@ lean_object* l_Lean_Parser_Tactic_generalize_formatter___closed__8;
lean_object* l_Lean_Parser_Tactic_change___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_syntheticHole___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_matchAlt___closed__3;
extern lean_object* l_Lean_Parser_Term_suffices_formatter___closed__4;
extern lean_object* l_Lean_Parser_Term_have_formatter___closed__4;
lean_object* l_Lean_Parser_Tactic_changeWith___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Tactic_intros_formatter(lean_object*);
@ -1517,7 +1503,6 @@ lean_object* l_Lean_Parser_Tactic_refine_x21___closed__5;
lean_object* l_Lean_Parser_Tactic_cases_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Tactic_altRHS___closed__2;
lean_object* l_Lean_Parser_Tactic_clear_formatter___closed__1;
extern lean_object* l_Lean_Parser_Term_let_x21___closed__1;
lean_object* l_Lean_Parser_Tactic_rwRuleSeq_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Tactic_rewrite_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_locationHyp___closed__2;
@ -1557,7 +1542,6 @@ lean_object* l_Lean_Parser_Tactic_rewrite_formatter___closed__9;
lean_object* l_Lean_Parser_Tactic_matchAlts_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__7;
lean_object* l_Lean_Parser_Tactic_rewriteSeq_parenthesizer___closed__2;
extern lean_object* l_Lean_Parser_Term_suffices_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_allGoals_formatter___closed__4;
extern lean_object* l_Lean_Parser_Term_show___elambda__1___closed__9;
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_skip(lean_object*);
@ -1596,7 +1580,6 @@ lean_object* l_Lean_Parser_Tactic_done___elambda__1___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Tactic_introMatch_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Tactic_matchAlt___closed__5;
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
extern lean_object* l_Lean_Parser_Term_let_x21_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_intro_formatter___closed__3;
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_orelse(lean_object*);
lean_object* l_Lean_Parser_Tactic_rwRuleSeq_parenthesizer___closed__3;
@ -1659,6 +1642,7 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_admit_formatter(lean_object*);
lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__4;
lean_object* l___regBuiltin_Lean_Parser_Tactic_apply_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_unicodeSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_have_parenthesizer___closed__3;
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_refine(lean_object*);
lean_object* l_Lean_Parser_Tactic_withAlts_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_inductionAlt_formatter___closed__2;
@ -1684,6 +1668,7 @@ lean_object* l_Lean_Parser_Tactic_refine_x21___closed__3;
lean_object* l_Lean_PrettyPrinter_Formatter_nonReservedSymbol_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_matchAlts_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_rewrite_formatter___closed__4;
extern lean_object* l_Lean_Parser_Term_let_x21___closed__2;
lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__3;
lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__6;
lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1694,7 +1679,6 @@ lean_object* l_Lean_Parser_Tactic_introMatch___elambda__1___closed__4;
lean_object* l_Lean_Parser_Tactic_traceState___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_locationTarget___elambda__1___closed__1;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_try_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_suffices_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Tactic_changeWith___elambda__1___closed__3;
lean_object* l_Lean_Parser_Tactic_paren___closed__7;
lean_object* l___regBuiltin_Lean_Parser_Tactic_clear_formatter(lean_object*);
@ -28459,48 +28443,36 @@ return x_74;
lean_object* _init_l_Lean_Parser_Tactic_have___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_haveDecl;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_have___closed__1;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_have___elambda__1___closed__1;
x_2 = l_Lean_Parser_Term_have___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_have___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_have___elambda__1___closed__1;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Tactic_have___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_have___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Tactic_have___closed__2;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_have___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_have___elambda__1___closed__3;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Tactic_have___closed__3;
x_3 = l_Lean_Parser_Tactic_have___closed__2;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Tactic_have___closed__5() {
lean_object* _init_l_Lean_Parser_Tactic_have___closed__4() {
_start:
{
lean_object* x_1;
@ -28508,12 +28480,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_have___elambda__1), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Tactic_have___closed__6() {
lean_object* _init_l_Lean_Parser_Tactic_have___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_have___closed__4;
x_2 = l_Lean_Parser_Tactic_have___closed__5;
x_1 = l_Lean_Parser_Tactic_have___closed__3;
x_2 = l_Lean_Parser_Tactic_have___closed__4;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -28524,7 +28496,7 @@ lean_object* _init_l_Lean_Parser_Tactic_have() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_have___closed__6;
x_1 = l_Lean_Parser_Tactic_have___closed__5;
return x_1;
}
}
@ -28559,22 +28531,10 @@ return x_5;
lean_object* _init_l_Lean_Parser_Tactic_have_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_have_formatter___closed__2;
x_2 = l_Lean_Parser_Term_have_formatter___closed__4;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_have_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_have___elambda__1___closed__1;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_have_formatter___closed__2;
x_3 = l_Lean_Parser_Term_have_formatter___closed__4;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -28587,7 +28547,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_have_formatter___closed__1;
x_7 = l_Lean_Parser_Tactic_have_formatter___closed__3;
x_7 = l_Lean_Parser_Tactic_have_formatter___closed__2;
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -28627,22 +28587,10 @@ return x_4;
lean_object* _init_l_Lean_Parser_Tactic_have_parenthesizer___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Term_have_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_have_parenthesizer___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_have___elambda__1___closed__1;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_have_parenthesizer___closed__2;
x_3 = l_Lean_Parser_Term_have_parenthesizer___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -28655,7 +28603,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_have_parenthesizer___closed__1;
x_7 = l_Lean_Parser_Tactic_have_parenthesizer___closed__3;
x_7 = l_Lean_Parser_Tactic_have_parenthesizer___closed__2;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -28981,48 +28929,36 @@ return x_74;
lean_object* _init_l_Lean_Parser_Tactic_suffices___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_sufficesDecl;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_suffices___closed__1;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_suffices___elambda__1___closed__1;
x_2 = l_Lean_Parser_Term_suffices___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_suffices___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_suffices___elambda__1___closed__1;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Tactic_suffices___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_suffices___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Tactic_suffices___closed__2;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_suffices___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_suffices___elambda__1___closed__3;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Tactic_suffices___closed__3;
x_3 = l_Lean_Parser_Tactic_suffices___closed__2;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Tactic_suffices___closed__5() {
lean_object* _init_l_Lean_Parser_Tactic_suffices___closed__4() {
_start:
{
lean_object* x_1;
@ -29030,12 +28966,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_suffices___elambda__1), 2,
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Tactic_suffices___closed__6() {
lean_object* _init_l_Lean_Parser_Tactic_suffices___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_suffices___closed__4;
x_2 = l_Lean_Parser_Tactic_suffices___closed__5;
x_1 = l_Lean_Parser_Tactic_suffices___closed__3;
x_2 = l_Lean_Parser_Tactic_suffices___closed__4;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -29046,7 +28982,7 @@ lean_object* _init_l_Lean_Parser_Tactic_suffices() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_suffices___closed__6;
x_1 = l_Lean_Parser_Tactic_suffices___closed__5;
return x_1;
}
}
@ -29081,22 +29017,10 @@ return x_5;
lean_object* _init_l_Lean_Parser_Tactic_suffices_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_suffices_formatter___closed__2;
x_2 = l_Lean_Parser_Term_suffices_formatter___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_suffices_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_suffices___elambda__1___closed__1;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_suffices_formatter___closed__2;
x_3 = l_Lean_Parser_Term_suffices_formatter___closed__4;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -29109,7 +29033,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_suffices_formatter___closed__1;
x_7 = l_Lean_Parser_Tactic_suffices_formatter___closed__3;
x_7 = l_Lean_Parser_Tactic_suffices_formatter___closed__2;
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -29149,22 +29073,10 @@ return x_4;
lean_object* _init_l_Lean_Parser_Tactic_suffices_parenthesizer___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Term_suffices_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_suffices_parenthesizer___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_suffices___elambda__1___closed__1;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_suffices_parenthesizer___closed__2;
x_3 = l_Lean_Parser_Term_suffices_parenthesizer___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -29177,7 +29089,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_suffices_parenthesizer___closed__1;
x_7 = l_Lean_Parser_Tactic_suffices_parenthesizer___closed__3;
x_7 = l_Lean_Parser_Tactic_suffices_parenthesizer___closed__2;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -30026,48 +29938,36 @@ return x_76;
lean_object* _init_l_Lean_Parser_Tactic_let___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_letDecl;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_let___closed__1;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_let___elambda__1___closed__1;
x_2 = l_Lean_Parser_Term_let___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_let___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_let___elambda__1___closed__1;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Tactic_let___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_let___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Tactic_let___closed__2;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_let___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_let___elambda__1___closed__3;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Tactic_let___closed__3;
x_3 = l_Lean_Parser_Tactic_let___closed__2;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Tactic_let___closed__5() {
lean_object* _init_l_Lean_Parser_Tactic_let___closed__4() {
_start:
{
lean_object* x_1;
@ -30075,12 +29975,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_let___elambda__1), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Tactic_let___closed__6() {
lean_object* _init_l_Lean_Parser_Tactic_let___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_let___closed__4;
x_2 = l_Lean_Parser_Tactic_let___closed__5;
x_1 = l_Lean_Parser_Tactic_let___closed__3;
x_2 = l_Lean_Parser_Tactic_let___closed__4;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -30091,7 +29991,7 @@ lean_object* _init_l_Lean_Parser_Tactic_let() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_let___closed__6;
x_1 = l_Lean_Parser_Tactic_let___closed__5;
return x_1;
}
}
@ -30126,22 +30026,10 @@ return x_5;
lean_object* _init_l_Lean_Parser_Tactic_let_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_let_formatter___closed__2;
x_2 = l_Lean_Parser_Term_let_formatter___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_let_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_let___elambda__1___closed__1;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_let_formatter___closed__2;
x_3 = l_Lean_Parser_Term_let_formatter___closed__4;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -30154,7 +30042,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_let_formatter___closed__1;
x_7 = l_Lean_Parser_Tactic_let_formatter___closed__3;
x_7 = l_Lean_Parser_Tactic_let_formatter___closed__2;
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -30194,22 +30082,10 @@ return x_4;
lean_object* _init_l_Lean_Parser_Tactic_let_parenthesizer___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Term_let_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_let_parenthesizer___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_let___elambda__1___closed__1;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_let_parenthesizer___closed__2;
x_3 = l_Lean_Parser_Term_let_parenthesizer___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -30222,7 +30098,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_let_parenthesizer___closed__1;
x_7 = l_Lean_Parser_Tactic_let_parenthesizer___closed__3;
x_7 = l_Lean_Parser_Tactic_let_parenthesizer___closed__2;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -30557,48 +30433,36 @@ return x_76;
lean_object* _init_l_Lean_Parser_Tactic_let_x21___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_letDecl;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_let_x21___closed__1;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_let_x21___elambda__1___closed__1;
x_2 = l_Lean_Parser_Term_let_x21___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_let_x21___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_let_x21___elambda__1___closed__1;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Tactic_let_x21___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_let_x21___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Tactic_let_x21___closed__2;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_let_x21___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_let_x21___elambda__1___closed__3;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Tactic_let_x21___closed__3;
x_3 = l_Lean_Parser_Tactic_let_x21___closed__2;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Tactic_let_x21___closed__5() {
lean_object* _init_l_Lean_Parser_Tactic_let_x21___closed__4() {
_start:
{
lean_object* x_1;
@ -30606,12 +30470,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_let_x21___elambda__1), 2,
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Tactic_let_x21___closed__6() {
lean_object* _init_l_Lean_Parser_Tactic_let_x21___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_let_x21___closed__4;
x_2 = l_Lean_Parser_Tactic_let_x21___closed__5;
x_1 = l_Lean_Parser_Tactic_let_x21___closed__3;
x_2 = l_Lean_Parser_Tactic_let_x21___closed__4;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -30622,7 +30486,7 @@ lean_object* _init_l_Lean_Parser_Tactic_let_x21() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_let_x21___closed__6;
x_1 = l_Lean_Parser_Tactic_let_x21___closed__5;
return x_1;
}
}
@ -30657,22 +30521,10 @@ return x_5;
lean_object* _init_l_Lean_Parser_Tactic_let_x21_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_let_x21_formatter___closed__2;
x_2 = l_Lean_Parser_Term_let_formatter___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_let_x21_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_let_x21___elambda__1___closed__1;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_let_x21_formatter___closed__2;
x_3 = l_Lean_Parser_Term_let_x21_formatter___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -30685,7 +30537,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_let_x21_formatter___closed__1;
x_7 = l_Lean_Parser_Tactic_let_x21_formatter___closed__3;
x_7 = l_Lean_Parser_Tactic_let_x21_formatter___closed__2;
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -30728,7 +30580,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_let_x21___elambda__1___closed__1;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_let_parenthesizer___closed__2;
x_3 = l_Lean_Parser_Term_let_parenthesizer___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -33252,8 +33104,6 @@ l_Lean_Parser_Tactic_have___closed__4 = _init_l_Lean_Parser_Tactic_have___closed
lean_mark_persistent(l_Lean_Parser_Tactic_have___closed__4);
l_Lean_Parser_Tactic_have___closed__5 = _init_l_Lean_Parser_Tactic_have___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_have___closed__5);
l_Lean_Parser_Tactic_have___closed__6 = _init_l_Lean_Parser_Tactic_have___closed__6();
lean_mark_persistent(l_Lean_Parser_Tactic_have___closed__6);
l_Lean_Parser_Tactic_have = _init_l_Lean_Parser_Tactic_have();
lean_mark_persistent(l_Lean_Parser_Tactic_have);
res = l___regBuiltinParser_Lean_Parser_Tactic_have(lean_io_mk_world());
@ -33263,8 +33113,6 @@ l_Lean_Parser_Tactic_have_formatter___closed__1 = _init_l_Lean_Parser_Tactic_hav
lean_mark_persistent(l_Lean_Parser_Tactic_have_formatter___closed__1);
l_Lean_Parser_Tactic_have_formatter___closed__2 = _init_l_Lean_Parser_Tactic_have_formatter___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_have_formatter___closed__2);
l_Lean_Parser_Tactic_have_formatter___closed__3 = _init_l_Lean_Parser_Tactic_have_formatter___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_have_formatter___closed__3);
l___regBuiltin_Lean_Parser_Tactic_have_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_have_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_have_formatter___closed__1);
res = l___regBuiltin_Lean_Parser_Tactic_have_formatter(lean_io_mk_world());
@ -33274,8 +33122,6 @@ l_Lean_Parser_Tactic_have_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic
lean_mark_persistent(l_Lean_Parser_Tactic_have_parenthesizer___closed__1);
l_Lean_Parser_Tactic_have_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_have_parenthesizer___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_have_parenthesizer___closed__2);
l_Lean_Parser_Tactic_have_parenthesizer___closed__3 = _init_l_Lean_Parser_Tactic_have_parenthesizer___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_have_parenthesizer___closed__3);
l___regBuiltin_Lean_Parser_Tactic_have_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_have_parenthesizer___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_have_parenthesizer___closed__1);
res = l___regBuiltin_Lean_Parser_Tactic_have_parenthesizer(lean_io_mk_world());
@ -33297,8 +33143,6 @@ l_Lean_Parser_Tactic_suffices___closed__4 = _init_l_Lean_Parser_Tactic_suffices_
lean_mark_persistent(l_Lean_Parser_Tactic_suffices___closed__4);
l_Lean_Parser_Tactic_suffices___closed__5 = _init_l_Lean_Parser_Tactic_suffices___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_suffices___closed__5);
l_Lean_Parser_Tactic_suffices___closed__6 = _init_l_Lean_Parser_Tactic_suffices___closed__6();
lean_mark_persistent(l_Lean_Parser_Tactic_suffices___closed__6);
l_Lean_Parser_Tactic_suffices = _init_l_Lean_Parser_Tactic_suffices();
lean_mark_persistent(l_Lean_Parser_Tactic_suffices);
res = l___regBuiltinParser_Lean_Parser_Tactic_suffices(lean_io_mk_world());
@ -33308,8 +33152,6 @@ l_Lean_Parser_Tactic_suffices_formatter___closed__1 = _init_l_Lean_Parser_Tactic
lean_mark_persistent(l_Lean_Parser_Tactic_suffices_formatter___closed__1);
l_Lean_Parser_Tactic_suffices_formatter___closed__2 = _init_l_Lean_Parser_Tactic_suffices_formatter___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_suffices_formatter___closed__2);
l_Lean_Parser_Tactic_suffices_formatter___closed__3 = _init_l_Lean_Parser_Tactic_suffices_formatter___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_suffices_formatter___closed__3);
l___regBuiltin_Lean_Parser_Tactic_suffices_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_suffices_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_suffices_formatter___closed__1);
res = l___regBuiltin_Lean_Parser_Tactic_suffices_formatter(lean_io_mk_world());
@ -33319,8 +33161,6 @@ l_Lean_Parser_Tactic_suffices_parenthesizer___closed__1 = _init_l_Lean_Parser_Ta
lean_mark_persistent(l_Lean_Parser_Tactic_suffices_parenthesizer___closed__1);
l_Lean_Parser_Tactic_suffices_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_suffices_parenthesizer___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_suffices_parenthesizer___closed__2);
l_Lean_Parser_Tactic_suffices_parenthesizer___closed__3 = _init_l_Lean_Parser_Tactic_suffices_parenthesizer___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_suffices_parenthesizer___closed__3);
l___regBuiltin_Lean_Parser_Tactic_suffices_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_suffices_parenthesizer___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_suffices_parenthesizer___closed__1);
res = l___regBuiltin_Lean_Parser_Tactic_suffices_parenthesizer(lean_io_mk_world());
@ -33385,8 +33225,6 @@ l_Lean_Parser_Tactic_let___closed__4 = _init_l_Lean_Parser_Tactic_let___closed__
lean_mark_persistent(l_Lean_Parser_Tactic_let___closed__4);
l_Lean_Parser_Tactic_let___closed__5 = _init_l_Lean_Parser_Tactic_let___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_let___closed__5);
l_Lean_Parser_Tactic_let___closed__6 = _init_l_Lean_Parser_Tactic_let___closed__6();
lean_mark_persistent(l_Lean_Parser_Tactic_let___closed__6);
l_Lean_Parser_Tactic_let = _init_l_Lean_Parser_Tactic_let();
lean_mark_persistent(l_Lean_Parser_Tactic_let);
res = l___regBuiltinParser_Lean_Parser_Tactic_let(lean_io_mk_world());
@ -33396,8 +33234,6 @@ l_Lean_Parser_Tactic_let_formatter___closed__1 = _init_l_Lean_Parser_Tactic_let_
lean_mark_persistent(l_Lean_Parser_Tactic_let_formatter___closed__1);
l_Lean_Parser_Tactic_let_formatter___closed__2 = _init_l_Lean_Parser_Tactic_let_formatter___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_let_formatter___closed__2);
l_Lean_Parser_Tactic_let_formatter___closed__3 = _init_l_Lean_Parser_Tactic_let_formatter___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_let_formatter___closed__3);
l___regBuiltin_Lean_Parser_Tactic_let_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_let_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_let_formatter___closed__1);
res = l___regBuiltin_Lean_Parser_Tactic_let_formatter(lean_io_mk_world());
@ -33407,8 +33243,6 @@ l_Lean_Parser_Tactic_let_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_
lean_mark_persistent(l_Lean_Parser_Tactic_let_parenthesizer___closed__1);
l_Lean_Parser_Tactic_let_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_let_parenthesizer___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_let_parenthesizer___closed__2);
l_Lean_Parser_Tactic_let_parenthesizer___closed__3 = _init_l_Lean_Parser_Tactic_let_parenthesizer___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_let_parenthesizer___closed__3);
l___regBuiltin_Lean_Parser_Tactic_let_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_let_parenthesizer___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_let_parenthesizer___closed__1);
res = l___regBuiltin_Lean_Parser_Tactic_let_parenthesizer(lean_io_mk_world());
@ -33430,8 +33264,6 @@ l_Lean_Parser_Tactic_let_x21___closed__4 = _init_l_Lean_Parser_Tactic_let_x21___
lean_mark_persistent(l_Lean_Parser_Tactic_let_x21___closed__4);
l_Lean_Parser_Tactic_let_x21___closed__5 = _init_l_Lean_Parser_Tactic_let_x21___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_let_x21___closed__5);
l_Lean_Parser_Tactic_let_x21___closed__6 = _init_l_Lean_Parser_Tactic_let_x21___closed__6();
lean_mark_persistent(l_Lean_Parser_Tactic_let_x21___closed__6);
l_Lean_Parser_Tactic_let_x21 = _init_l_Lean_Parser_Tactic_let_x21();
lean_mark_persistent(l_Lean_Parser_Tactic_let_x21);
res = l___regBuiltinParser_Lean_Parser_Tactic_let_x21(lean_io_mk_world());
@ -33441,8 +33273,6 @@ l_Lean_Parser_Tactic_let_x21_formatter___closed__1 = _init_l_Lean_Parser_Tactic_
lean_mark_persistent(l_Lean_Parser_Tactic_let_x21_formatter___closed__1);
l_Lean_Parser_Tactic_let_x21_formatter___closed__2 = _init_l_Lean_Parser_Tactic_let_x21_formatter___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_let_x21_formatter___closed__2);
l_Lean_Parser_Tactic_let_x21_formatter___closed__3 = _init_l_Lean_Parser_Tactic_let_x21_formatter___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_let_x21_formatter___closed__3);
l___regBuiltin_Lean_Parser_Tactic_let_x21_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_let_x21_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_let_x21_formatter___closed__1);
res = l___regBuiltin_Lean_Parser_Tactic_let_x21_formatter(lean_io_mk_world());

9545
stage0/stdlib/Lean/Parser/Term.c generated
View file

File diff suppressed because it is too large Load diff