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 13:28:04 -07:00
parent 93090baa82
commit 5aafaa51ff
7 changed files with 3797 additions and 2357 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
stage0/src/Lean/Parser/Tactic.lean generated
View file

@ -9,9 +9,6 @@ namespace Lean
namespace Parser
namespace Tactic
def seq := node `Lean.Parser.Tactic.seq $ sepBy tacticParser "; " true
def seq1 := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
def underscoreFn : ParserFn :=
fun c s =>
let s := symbolFn "_" c s;
@ -38,13 +35,13 @@ def ident' : Parser := ident <|> underscore
@[builtinTacticParser] def «exact» := parser! nonReservedSymbol "exact " >> termParser
@[builtinTacticParser] def «refine» := parser! nonReservedSymbol "refine " >> termParser
@[builtinTacticParser] def «refine!» := parser! nonReservedSymbol "refine! " >> termParser
@[builtinTacticParser] def «case» := parser! nonReservedSymbol "case " >> ident >> darrow >> indentedNonEmptySeq
@[builtinTacticParser] def «allGoals» := parser! nonReservedSymbol "allGoals " >> indentedNonEmptySeq
@[builtinTacticParser] def «case» := parser! nonReservedSymbol "case " >> ident >> darrow >> tacticSeq1
@[builtinTacticParser] def «allGoals» := parser! nonReservedSymbol "allGoals " >> tacticSeq1
@[builtinTacticParser] def «skip» := parser! nonReservedSymbol "skip"
@[builtinTacticParser] def «done» := parser! nonReservedSymbol "done"
@[builtinTacticParser] def «admit» := parser! nonReservedSymbol "admit"
@[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
@[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> indentedNonEmptySeq
@[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> tacticSeq1
@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize " >> optional (try (ident >> " : ")) >> termParser 51 >> " = " >> ident
def locationWildcard := parser! "*"
@ -61,7 +58,7 @@ def rwRuleSeq := parser! "[" >> sepBy1 rwRule ", " true >> "]"
@[builtinTacticParser] def «rewriteSeq» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> rwRuleSeq >> optional location
def majorPremise := parser! optional (try (ident >> " : ")) >> termParser
def altRHS := Term.hole <|> Term.syntheticHole <|> indentedNonEmptySeq
def altRHS := Term.hole <|> Term.syntheticHole <|> tacticSeq1
def inductionAlt : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> altRHS
def inductionAlts : Parser := withPosition $ "|" >> sepBy1 inductionAlt (checkColGe "alternatives must be indented" >> "|")
def withAlts : Parser := optional (" with " >> inductionAlts)
@ -77,8 +74,10 @@ def matchAlts : Parser := group $ withPosition $ (optional "| ") >> sepBy1 match
def withIds : Parser := optional (" with " >> many1 ident')
@[builtinTacticParser] def «injection» := parser! nonReservedSymbol "injection " >> termParser >> withIds
def seq := node `Lean.Parser.Tactic.seq $ sepBy tacticParser "; " true
def seq1 := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
@[builtinTacticParser] def paren := parser! "(" >> seq1 >> ")"
@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"
@[builtinTacticParser] def nestedTactic := parser! "{" >> seq >> "}"
@[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1
/- Term binders as tactics. They are all implemented as macros using the triad: named holes, hygiene, and `refine` tactic. -/

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

@ -19,9 +19,19 @@ registerBuiltinDynamicParserAttribute `tacticParser `tactic
@[inline] def tacticParser (rbp : Nat := 0) : Parser :=
categoryParser `tactic rbp
def Tactic.indentedNonEmptySeq : Parser :=
namespace Tactic
def tacticSeq1Indented : Parser :=
nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.seq $ withPosition $
sepBy1 tacticParser (try ("; " >> checkColGe "tatic must be indented"))
def tacticSeq1Bracketed : Parser :=
parser! "{" >> sepBy1 tacticParser "; " true >> "}"
def tacticSeq1 := tacticSeq1Bracketed <|> tacticSeq1Indented
def tacticSeqBracketed : Parser :=
parser! "{" >> sepBy tacticParser "; " true >> "}"
end Tactic
def darrow : Parser := " => "
@ -43,7 +53,7 @@ checkPrec prec >> symbol sym >> termParser (prec+1)
/- Built-in parsers -/
@[builtinTermParser] def byTactic := parser!:leadPrec "by " >> Tactic.indentedNonEmptySeq
@[builtinTermParser] def byTactic := parser!:leadPrec "by " >> Tactic.tacticSeq1
-- `checkPrec` necessary for the pretty printer
@[builtinTermParser] def ident := checkPrec maxPrec >> Parser.ident
@ -85,7 +95,7 @@ def optType : Parser := optional typeSpec
@[builtinTermParser] def inaccessible := parser! ".(" >> termParser >> ")"
def binderIdent : Parser := ident <|> hole
def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)
def binderTactic := parser! try (" := " >> " by ") >> Tactic.indentedNonEmptySeq
def binderTactic := parser! try (" := " >> " by ") >> Tactic.tacticSeq1
def binderDefault := parser! " := " >> termParser
def explicitBinder (requireType := false) := ppGroup $ parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
def implicitBinder (requireType := false) := ppGroup $ parser! "{" >> many1 binderIdent >> binderType requireType >> "}"

112
stage0/stdlib/Lean/Parser/Command.c generated
View file

@ -71,6 +71,7 @@ lean_object* l_Lean_Parser_Command_extends___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_ctor;
lean_object* l_Lean_Parser_Command_structure___closed__3;
lean_object* l_Lean_Parser_Command_declSig_parenthesizer___closed__2;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_instance_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_def___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_exit_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -155,7 +156,6 @@ lean_object* l_Lean_Parser_Command_structure_parenthesizer___closed__6;
lean_object* l_Lean_Parser_Term_quot___closed__2;
lean_object* l_Lean_Parser_Command_attribute___closed__7;
lean_object* l_Lean_Parser_Command_protected___elambda__1___closed__8;
extern lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
lean_object* l_Lean_Parser_Command_attribute_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_noncomputable;
lean_object* l_Lean_Parser_Command_section___elambda__1___closed__9;
@ -233,6 +233,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(lean_object
lean_object* l_Lean_Parser_Command_export___closed__7;
lean_object* l_Lean_Parser_Command_open___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_declId_formatter___closed__6;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_structFields_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_abbrev_formatter___closed__8;
@ -283,6 +284,7 @@ lean_object* l_Lean_Parser_Command_structure_formatter___closed__8;
lean_object* l_Lean_Parser_Command_structInstBinder___closed__3;
lean_object* l_Lean_Parser_Command_declModifiers_parenthesizer___closed__16;
lean_object* l_Lean_Parser_Command_export___elambda__1___closed__3;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed___closed__1;
lean_object* l_Lean_Parser_Command_structFields_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__12;
lean_object* l_Lean_Parser_Term_quot_formatter___closed__4;
@ -633,6 +635,7 @@ lean_object* l_Lean_Parser_Command_theorem_formatter___closed__6;
lean_object* l_Lean_Parser_Command_initialize___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Command_universes_formatter(lean_object*);
lean_object* l_Lean_Parser_Command_abbrev_parenthesizer___closed__6;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_openRenaming___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_theorem___closed__6;
lean_object* l_Lean_Parser_Command_openHiding___closed__4;
@ -943,6 +946,7 @@ lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__15;
lean_object* l_Lean_Parser_Command_section_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_inductive_formatter___closed__1;
lean_object* l_Lean_Parser_Command_attribute_formatter___closed__4;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed___closed__3;
lean_object* l_Lean_Parser_Command_declId_formatter___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Command_init__quot_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_openSimple___closed__3;
@ -1181,6 +1185,7 @@ lean_object* l_Lean_Parser_Command_partial___closed__1;
lean_object* l_Lean_Parser_Command_constant_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_abbrev___elambda__1___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Command_synth_parenthesizer___closed__1;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
lean_object* l_Lean_Parser_Command_private___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_classInductive___closed__4;
lean_object* l_Lean_Parser_Command_constant___closed__5;
@ -1258,6 +1263,7 @@ extern lean_object* l_Lean_Parser_Term_structInstArrayRef_formatter___closed__3;
lean_object* l_Lean_Parser_Command_noncomputable_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_declSig___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_declModifiers_formatter___closed__8;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed_formatter___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Command_declaration_formatter___closed__1;
extern lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_ctor___elambda__1(lean_object*, lean_object*);
@ -1282,7 +1288,6 @@ lean_object* l___regBuiltin_Lean_Parser_Command_check_parenthesizer(lean_object*
lean_object* l_Lean_Parser_Command_optDeclSig___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_variable___closed__6;
lean_object* l_Lean_Parser_Command_resolve__name_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
lean_object* l_Lean_Parser_Term_quot___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_openRenaming_parenthesizer___closed__2;
extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__3;
@ -1408,7 +1413,6 @@ lean_object* l_Lean_Parser_Command_check___elambda__1___closed__9;
lean_object* l___regBuiltin_Lean_Parser_Command_universes_formatter___closed__1;
lean_object* l_Lean_Parser_Command_synth___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_unsafe_formatter___closed__3;
extern lean_object* l_Lean_Parser_Term_emptyC___closed__4;
lean_object* l___regBuiltin_Lean_Parser_Command_initialize_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_structCtor___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_declId_parenthesizer___closed__7;
@ -1483,7 +1487,6 @@ lean_object* l_Lean_Parser_Command_openSimple___closed__4;
lean_object* l___regBuiltin_Lean_Parser_Command_synth_formatter___closed__1;
lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__8;
extern lean_object* l_Lean_Parser_Term_haveAssign___closed__1;
extern lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_structure_parenthesizer___closed__10;
lean_object* l_Lean_Parser_Command_example_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_in___closed__4;
@ -1543,7 +1546,6 @@ lean_object* l_Lean_Parser_Command_attribute___closed__2;
lean_object* l_Lean_Parser_Command_synth___closed__4;
lean_object* l_Lean_Parser_Command_inductive_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Command_in_formatter___closed__1;
extern lean_object* l_Lean_Parser_Term_emptyC_formatter___closed__5;
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_Command_exit___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_resolve__name___closed__6;
@ -1636,7 +1638,6 @@ lean_object* l___regBuiltin_Lean_Parser_Command_mutual_parenthesizer___closed__1
lean_object* l_Lean_Parser_Command_declValSimple___closed__4;
lean_object* l_Lean_Parser_Command_noncomputable_formatter___closed__2;
lean_object* l_Lean_Parser_Command_ctor___closed__8;
extern lean_object* l_Lean_Parser_Term_emptyC___closed__3;
lean_object* l_Lean_Parser_Command_declaration_formatter___closed__21;
lean_object* l_Lean_Parser_Command_theorem___closed__1;
lean_object* l_Lean_Parser_Command_classInductive___elambda__1___closed__8;
@ -1985,6 +1986,7 @@ lean_object* l_Lean_Parser_Command_set__option_formatter___closed__5;
lean_object* l_Lean_Parser_Command_check___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_quot_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_namespace_formatter___closed__1;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed_formatter___closed__6;
lean_object* l_Lean_Parser_Command_mutual___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_openHiding_formatter___closed__1;
lean_object* l_Lean_Parser_Command_declaration___closed__15;
@ -2177,7 +2179,6 @@ extern lean_object* l_Lean_Parser_Term_str_formatter___closed__1;
lean_object* l_Lean_Parser_Command_classInductive_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_export___closed__10;
lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_initialize___closed__6;
lean_object* l_Lean_Parser_unicodeSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_ctor___closed__7;
@ -2192,7 +2193,6 @@ lean_object* l_Lean_Parser_Command_partial_formatter___closed__1;
lean_object* l_Lean_Parser_Command_openHiding_formatter___closed__4;
lean_object* l___regBuiltin_Lean_Parser_Command_initialize_parenthesizer(lean_object*);
extern lean_object* l_Lean_Parser_Term_haveAssign_formatter___closed__2;
extern lean_object* l_Lean_Parser_Term_emptyC_formatter___closed__4;
lean_object* l_Lean_Parser_Command_universes___closed__3;
lean_object* l_Lean_Parser_Command_structInstBinder_formatter___closed__4;
lean_object* l_Lean_Parser_Command_attribute_formatter___closed__3;
@ -7314,13 +7314,13 @@ lean_object* x_44; lean_object* x_45; uint8_t x_46;
x_44 = lean_ctor_get(x_43, 1);
lean_inc(x_44);
lean_dec(x_43);
x_45 = l_Lean_Parser_Term_emptyC___elambda__1___closed__8;
x_45 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__6;
x_46 = lean_string_dec_eq(x_44, x_45);
lean_dec(x_44);
if (x_46 == 0)
{
lean_object* x_47; lean_object* x_48;
x_47 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_47 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_48 = l_Lean_Parser_ParserState_mkErrorsAt(x_40, x_47, x_39);
x_16 = x_48;
goto block_33;
@ -7336,7 +7336,7 @@ else
{
lean_object* x_49; lean_object* x_50;
lean_dec(x_43);
x_49 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_49 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_50 = l_Lean_Parser_ParserState_mkErrorsAt(x_40, x_49, x_39);
x_16 = x_50;
goto block_33;
@ -7346,7 +7346,7 @@ else
{
lean_object* x_51; lean_object* x_52;
lean_dec(x_41);
x_51 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_51 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_52 = l_Lean_Parser_ParserState_mkErrorsAt(x_40, x_51, x_39);
x_16 = x_52;
goto block_33;
@ -7598,13 +7598,13 @@ lean_object* x_122; lean_object* x_123; uint8_t x_124;
x_122 = lean_ctor_get(x_121, 1);
lean_inc(x_122);
lean_dec(x_121);
x_123 = l_Lean_Parser_Term_emptyC___elambda__1___closed__8;
x_123 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__6;
x_124 = lean_string_dec_eq(x_122, x_123);
lean_dec(x_122);
if (x_124 == 0)
{
lean_object* x_125; lean_object* x_126;
x_125 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_125 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_126 = l_Lean_Parser_ParserState_mkErrorsAt(x_118, x_125, x_117);
x_88 = x_126;
goto block_111;
@ -7620,7 +7620,7 @@ else
{
lean_object* x_127; lean_object* x_128;
lean_dec(x_121);
x_127 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_127 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_128 = l_Lean_Parser_ParserState_mkErrorsAt(x_118, x_127, x_117);
x_88 = x_128;
goto block_111;
@ -7630,7 +7630,7 @@ else
{
lean_object* x_129; lean_object* x_130;
lean_dec(x_119);
x_129 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_129 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_130 = l_Lean_Parser_ParserState_mkErrorsAt(x_118, x_129, x_117);
x_88 = x_130;
goto block_111;
@ -7698,7 +7698,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_declId___closed__1;
x_2 = l_Lean_Parser_Term_emptyC___closed__3;
x_2 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___closed__3;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
@ -13095,13 +13095,13 @@ lean_object* x_59; lean_object* x_60; uint8_t x_61;
x_59 = lean_ctor_get(x_58, 1);
lean_inc(x_59);
lean_dec(x_58);
x_60 = l_Lean_Parser_Term_emptyC___elambda__1___closed__7;
x_60 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__5;
x_61 = lean_string_dec_eq(x_59, x_60);
lean_dec(x_59);
if (x_61 == 0)
{
lean_object* x_62; lean_object* x_63;
x_62 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_62 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
lean_inc(x_10);
x_63 = l_Lean_Parser_ParserState_mkErrorsAt(x_55, x_62, x_10);
x_23 = x_63;
@ -13117,7 +13117,7 @@ else
{
lean_object* x_64; lean_object* x_65;
lean_dec(x_58);
x_64 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_64 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
lean_inc(x_10);
x_65 = l_Lean_Parser_ParserState_mkErrorsAt(x_55, x_64, x_10);
x_23 = x_65;
@ -13128,7 +13128,7 @@ else
{
lean_object* x_66; lean_object* x_67;
lean_dec(x_56);
x_66 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_66 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
lean_inc(x_10);
x_67 = l_Lean_Parser_ParserState_mkErrorsAt(x_55, x_66, x_10);
x_23 = x_67;
@ -13187,13 +13187,13 @@ lean_object* x_30; lean_object* x_31; uint8_t x_32;
x_30 = lean_ctor_get(x_29, 1);
lean_inc(x_30);
lean_dec(x_29);
x_31 = l_Lean_Parser_Term_emptyC___elambda__1___closed__8;
x_31 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__6;
x_32 = lean_string_dec_eq(x_30, x_31);
lean_dec(x_30);
if (x_32 == 0)
{
lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_33 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_33 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_34 = l_Lean_Parser_ParserState_mkErrorsAt(x_26, x_33, x_25);
x_35 = lean_ctor_get(x_34, 0);
lean_inc(x_35);
@ -13228,7 +13228,7 @@ else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45;
lean_dec(x_29);
x_41 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_41 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_42 = l_Lean_Parser_ParserState_mkErrorsAt(x_26, x_41, x_25);
x_43 = lean_ctor_get(x_42, 0);
lean_inc(x_43);
@ -13247,7 +13247,7 @@ else
{
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50;
lean_dec(x_27);
x_46 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_46 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_47 = l_Lean_Parser_ParserState_mkErrorsAt(x_26, x_46, x_25);
x_48 = lean_ctor_get(x_47, 0);
lean_inc(x_48);
@ -13362,13 +13362,13 @@ lean_object* x_134; lean_object* x_135; uint8_t x_136;
x_134 = lean_ctor_get(x_133, 1);
lean_inc(x_134);
lean_dec(x_133);
x_135 = l_Lean_Parser_Term_emptyC___elambda__1___closed__7;
x_135 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__5;
x_136 = lean_string_dec_eq(x_134, x_135);
lean_dec(x_134);
if (x_136 == 0)
{
lean_object* x_137; lean_object* x_138;
x_137 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_137 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
lean_inc(x_81);
x_138 = l_Lean_Parser_ParserState_mkErrorsAt(x_130, x_137, x_81);
x_98 = x_138;
@ -13384,7 +13384,7 @@ else
{
lean_object* x_139; lean_object* x_140;
lean_dec(x_133);
x_139 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_139 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
lean_inc(x_81);
x_140 = l_Lean_Parser_ParserState_mkErrorsAt(x_130, x_139, x_81);
x_98 = x_140;
@ -13395,7 +13395,7 @@ else
{
lean_object* x_141; lean_object* x_142;
lean_dec(x_131);
x_141 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_141 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
lean_inc(x_81);
x_142 = l_Lean_Parser_ParserState_mkErrorsAt(x_130, x_141, x_81);
x_98 = x_142;
@ -13460,13 +13460,13 @@ lean_object* x_105; lean_object* x_106; uint8_t x_107;
x_105 = lean_ctor_get(x_104, 1);
lean_inc(x_105);
lean_dec(x_104);
x_106 = l_Lean_Parser_Term_emptyC___elambda__1___closed__8;
x_106 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__6;
x_107 = lean_string_dec_eq(x_105, x_106);
lean_dec(x_105);
if (x_107 == 0)
{
lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112;
x_108 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_108 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_109 = l_Lean_Parser_ParserState_mkErrorsAt(x_101, x_108, x_100);
x_110 = lean_ctor_get(x_109, 0);
lean_inc(x_110);
@ -13501,7 +13501,7 @@ else
{
lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120;
lean_dec(x_104);
x_116 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_116 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_117 = l_Lean_Parser_ParserState_mkErrorsAt(x_101, x_116, x_100);
x_118 = lean_ctor_get(x_117, 0);
lean_inc(x_118);
@ -13520,7 +13520,7 @@ else
{
lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125;
lean_dec(x_102);
x_121 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_121 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_122 = l_Lean_Parser_ParserState_mkErrorsAt(x_101, x_121, x_100);
x_123 = lean_ctor_get(x_122, 0);
lean_inc(x_123);
@ -13574,7 +13574,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_inferMod___elambda__1___closed__2;
x_2 = l_Lean_Parser_Term_emptyC___closed__4;
x_2 = l_Lean_Parser_Term_emptyC___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
@ -17152,13 +17152,13 @@ lean_object* x_99; lean_object* x_100; uint8_t x_101;
x_99 = lean_ctor_get(x_98, 1);
lean_inc(x_99);
lean_dec(x_98);
x_100 = l_Lean_Parser_Term_emptyC___elambda__1___closed__7;
x_100 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__5;
x_101 = lean_string_dec_eq(x_99, x_100);
lean_dec(x_99);
if (x_101 == 0)
{
lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106;
x_102 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_102 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
x_103 = l_Lean_Parser_ParserState_mkErrorsAt(x_95, x_102, x_94);
x_104 = lean_ctor_get(x_103, 0);
lean_inc(x_104);
@ -17193,7 +17193,7 @@ else
{
lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114;
lean_dec(x_98);
x_110 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_110 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
x_111 = l_Lean_Parser_ParserState_mkErrorsAt(x_95, x_110, x_94);
x_112 = lean_ctor_get(x_111, 0);
lean_inc(x_112);
@ -17212,7 +17212,7 @@ else
{
lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119;
lean_dec(x_96);
x_115 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_115 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
x_116 = l_Lean_Parser_ParserState_mkErrorsAt(x_95, x_115, x_94);
x_117 = lean_ctor_get(x_116, 0);
lean_inc(x_117);
@ -17276,13 +17276,13 @@ lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_21 = lean_ctor_get(x_20, 1);
lean_inc(x_21);
lean_dec(x_20);
x_22 = l_Lean_Parser_Term_emptyC___elambda__1___closed__8;
x_22 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__6;
x_23 = lean_string_dec_eq(x_21, x_22);
lean_dec(x_21);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_24 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_24 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_24, x_16);
x_26 = l_Lean_Parser_Command_structImplicitBinder___elambda__1___closed__2;
x_27 = l_Lean_Parser_ParserState_mkNode(x_25, x_26, x_11);
@ -17301,7 +17301,7 @@ else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
lean_dec(x_20);
x_30 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_30 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_31 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_30, x_16);
x_32 = l_Lean_Parser_Command_structImplicitBinder___elambda__1___closed__2;
x_33 = l_Lean_Parser_ParserState_mkNode(x_31, x_32, x_11);
@ -17312,7 +17312,7 @@ else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37;
lean_dec(x_18);
x_34 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_34 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_35 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_34, x_16);
x_36 = l_Lean_Parser_Command_structImplicitBinder___elambda__1___closed__2;
x_37 = l_Lean_Parser_ParserState_mkNode(x_35, x_36, x_11);
@ -17612,13 +17612,13 @@ lean_object* x_243; lean_object* x_244; uint8_t x_245;
x_243 = lean_ctor_get(x_242, 1);
lean_inc(x_243);
lean_dec(x_242);
x_244 = l_Lean_Parser_Term_emptyC___elambda__1___closed__7;
x_244 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__5;
x_245 = lean_string_dec_eq(x_243, x_244);
lean_dec(x_243);
if (x_245 == 0)
{
lean_object* x_246; lean_object* x_247; lean_object* x_248; lean_object* x_249; lean_object* x_250;
x_246 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_246 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
x_247 = l_Lean_Parser_ParserState_mkErrorsAt(x_239, x_246, x_238);
x_248 = lean_ctor_get(x_247, 0);
lean_inc(x_248);
@ -17653,7 +17653,7 @@ else
{
lean_object* x_254; lean_object* x_255; lean_object* x_256; lean_object* x_257; lean_object* x_258;
lean_dec(x_242);
x_254 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_254 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
x_255 = l_Lean_Parser_ParserState_mkErrorsAt(x_239, x_254, x_238);
x_256 = lean_ctor_get(x_255, 0);
lean_inc(x_256);
@ -17672,7 +17672,7 @@ else
{
lean_object* x_259; lean_object* x_260; lean_object* x_261; lean_object* x_262; lean_object* x_263;
lean_dec(x_240);
x_259 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_259 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
x_260 = l_Lean_Parser_ParserState_mkErrorsAt(x_239, x_259, x_238);
x_261 = lean_ctor_get(x_260, 0);
lean_inc(x_261);
@ -17736,13 +17736,13 @@ lean_object* x_147; lean_object* x_148; uint8_t x_149;
x_147 = lean_ctor_get(x_146, 1);
lean_inc(x_147);
lean_dec(x_146);
x_148 = l_Lean_Parser_Term_emptyC___elambda__1___closed__8;
x_148 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__6;
x_149 = lean_string_dec_eq(x_147, x_148);
lean_dec(x_147);
if (x_149 == 0)
{
lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; uint8_t x_154; lean_object* x_155;
x_150 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_150 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_151 = l_Lean_Parser_ParserState_mkErrorsAt(x_143, x_150, x_142);
x_152 = l_Lean_Parser_Command_structImplicitBinder___elambda__1___closed__2;
x_153 = l_Lean_Parser_ParserState_mkNode(x_151, x_152, x_137);
@ -17767,7 +17767,7 @@ else
{
lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; uint8_t x_164; lean_object* x_165;
lean_dec(x_146);
x_160 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_160 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_161 = l_Lean_Parser_ParserState_mkErrorsAt(x_143, x_160, x_142);
x_162 = l_Lean_Parser_Command_structImplicitBinder___elambda__1___closed__2;
x_163 = l_Lean_Parser_ParserState_mkNode(x_161, x_162, x_137);
@ -17781,7 +17781,7 @@ else
{
lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; uint8_t x_170; lean_object* x_171;
lean_dec(x_144);
x_166 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_166 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_167 = l_Lean_Parser_ParserState_mkErrorsAt(x_143, x_166, x_142);
x_168 = l_Lean_Parser_Command_structImplicitBinder___elambda__1___closed__2;
x_169 = l_Lean_Parser_ParserState_mkNode(x_167, x_168, x_137);
@ -18031,7 +18031,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_declModifiers;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_emptyC___closed__2;
x_3 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___closed__1;
x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
return x_4;
}
@ -18043,7 +18043,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_declSig;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_emptyC___closed__3;
x_3 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___closed__3;
x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
return x_4;
}
@ -24669,7 +24669,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_declId_formatter___closed__2;
x_2 = l_Lean_Parser_Term_emptyC_formatter___closed__4;
x_2 = l_Lean_Parser_Tactic_tacticSeq1Bracketed_formatter___closed__6;
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);
@ -25544,7 +25544,7 @@ lean_object* _init_l_Lean_Parser_Command_inferMod_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Term_emptyC_formatter___closed__5;
x_1 = l_Lean_Parser_Term_emptyC_formatter___closed__3;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_try_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -26278,7 +26278,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_ctor_formatter___closed__6;
x_2 = l_Lean_Parser_Term_emptyC_formatter___closed__3;
x_2 = l_Lean_Parser_Tactic_tacticSeq1Bracketed_formatter___closed__2;
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);
@ -26300,7 +26300,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_theorem_formatter___closed__3;
x_2 = l_Lean_Parser_Term_emptyC_formatter___closed__4;
x_2 = l_Lean_Parser_Tactic_tacticSeq1Bracketed_formatter___closed__6;
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);

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

@ -31,9 +31,11 @@ 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;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__6;
lean_object* l_Lean_Parser_Term_doIf___closed__12;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_doIf___elambda__1___spec__1___closed__1;
lean_object* l_Lean_Parser_Term_doId___closed__3;
extern lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__5;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_categoryParser_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doPat_parenthesizer___closed__2;
lean_object* l_Lean_Parser_andthenInfo(lean_object*, lean_object*);
@ -54,6 +56,7 @@ lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser
lean_object* l_Lean_Parser_Term_doExpr_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_leftArrow_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doMatch_parenthesizer___closed__3;
extern lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__1;
lean_object* l_Lean_Parser_Term_continue___elambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_notFollowedByFn___closed__1;
lean_object* l_Lean_Parser_Term_doIf_formatter___closed__20;
@ -61,7 +64,6 @@ lean_object* l_Lean_Parser_Term_do___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_do_formatter___closed__3;
extern lean_object* l_Lean_nullKind;
lean_object* l_Lean_Parser_Term_doMatch_formatter___closed__6;
extern lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
lean_object* l_Lean_Parser_Term_continue_formatter___closed__1;
lean_object* l___regBuiltinParser_Lean_Parser_Term_doHave(lean_object*);
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_doIf___elambda__1___spec__1___closed__2;
@ -74,6 +76,7 @@ lean_object* l_Lean_Parser_Term_doHave_formatter(lean_object*, lean_object*, lea
lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__11;
lean_object* l_Lean_PrettyPrinter_Formatter_many_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented_formatter___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Term_doFor_parenthesizer(lean_object*);
lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_doSeqBracketed___elambda__1___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__4;
@ -92,6 +95,7 @@ lean_object* l_Lean_Parser_Term_doIf_formatter___closed__12;
lean_object* l_Lean_Parser_Term_doMatchAlts___closed__1;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__8;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_doMatchAlts;
lean_object* l_Lean_Parser_Term_doSeq___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doMatch_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -106,6 +110,7 @@ extern lean_object* l_Lean_Parser_Term_binderTactic_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Term_doMatch___closed__5;
lean_object* l_Lean_Parser_Term_doMatchAlts___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__4;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed___closed__1;
lean_object* l_Lean_Parser_Term_continue___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_doSeqBracketed___closed__8;
lean_object* l_Lean_Parser_Term_doId___closed__5;
@ -200,10 +205,10 @@ lean_object* l_Lean_Parser_Term_break___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_liftMethod___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_doId___closed__4;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_break___closed__5;
lean_object* l_Lean_Parser_Term_liftMethod_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Term_doMatch___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Tactic_indentedNonEmptySeq_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__12;
lean_object* l___regBuiltin_Lean_Parser_Term_break_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_doIf___closed__2;
@ -214,9 +219,9 @@ lean_object* l_Lean_Parser_Term_liftMethod___closed__5;
lean_object* l_Lean_Parser_Term_doIf;
lean_object* l_Lean_Parser_checkPrecFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__12;
extern lean_object* l_Lean_Parser_Tactic_indentedNonEmptySeq_formatter___closed__1;
lean_object* l_Lean_Parser_Term_doIf___closed__4;
lean_object* l_Lean_Parser_Term_doLetArrow_parenthesizer___closed__4;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_doPat___closed__6;
lean_object* l_Lean_PrettyPrinter_Formatter_optional_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doSeqIndent___closed__1;
@ -327,6 +332,7 @@ 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;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed___closed__3;
lean_object* l_Lean_PrettyPrinter_Formatter_unicodeSymbol_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Term_doHave_formatter___closed__1;
lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__2;
@ -342,7 +348,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;
extern lean_object* l_Lean_Parser_Term_emptyC___closed__2;
lean_object* l_Lean_Parser_Term_doSeqIndent___closed__5;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__24;
lean_object* l_Lean_Parser_Term_doFor_formatter___closed__5;
@ -402,6 +407,7 @@ lean_object* l_Lean_Parser_Term_do___elambda__1___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Term_doMatch_formatter(lean_object*);
lean_object* l_Lean_Parser_Term_doFor___closed__5;
lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___closed__4;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
lean_object* l_Lean_Parser_Term_doExpr_formatter___closed__8;
lean_object* l_Lean_Parser_Term_do;
lean_object* l_Lean_Parser_Term_doMatchAlts___closed__5;
@ -420,7 +426,6 @@ lean_object* l_Lean_Parser_regBuiltinDoElemParserAttr(lean_object*);
lean_object* l_Lean_Parser_Term_doMatchAlts_formatter___closed__5;
lean_object* l_Lean_Parser_Term_doPat_formatter___closed__1;
lean_object* l___regBuiltinParser_Lean_Parser_Term_doFor(lean_object*);
extern lean_object* l_Lean_Parser_Tactic_indentedNonEmptySeq_parenthesizer___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Term_doIf_formatter___closed__1;
extern lean_object* l_Lean_Parser_Term_match_formatter___closed__4;
lean_object* l_Lean_Parser_Term_doLetArrow_formatter___closed__6;
@ -433,6 +438,7 @@ lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__25;
lean_object* l_Lean_Parser_Term_doPat_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doSeqIndent___closed__3;
lean_object* l_Lean_Parser_Term_liftMethod___closed__6;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doSeqBracketed___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_liftMethod___closed__3;
@ -440,7 +446,6 @@ lean_object* l_Lean_Parser_Term_doPat___closed__9;
lean_object* l_Lean_Parser_Term_doId;
lean_object* l_Lean_Parser_Term_continue;
lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
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*);
@ -501,10 +506,8 @@ lean_object* l_Lean_Parser_Term_leftArrow;
lean_object* l_Lean_Parser_Term_doPat_formatter___closed__9;
extern lean_object* l_Lean_Parser_Term_matchAlt_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_ident___elambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__8;
extern lean_object* l_Lean_Parser_Term_match_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doPat___closed__10;
extern lean_object* l_Lean_Parser_Tactic_indentedNonEmptySeq___closed__2;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doIf_formatter___closed__17;
lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__7;
@ -514,6 +517,7 @@ lean_object* l___regBuiltin_Lean_Parser_Term_do_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_liftMethod_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_doSeqIndent_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Term_continue_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed_formatter___closed__3;
lean_object* l_Lean_Parser_Term_doPat_formatter___closed__4;
lean_object* l_Lean_Parser_Term_do___closed__7;
lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___closed__3;
@ -522,7 +526,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_emptyC_formatter___closed__3;
extern lean_object* l_Lean_Parser_Term_haveDecl;
lean_object* l_Lean_Parser_Term_doHave___closed__4;
lean_object* l_Lean_Parser_Term_liftMethod_parenthesizer___closed__1;
@ -565,7 +568,6 @@ lean_object* l_Lean_Parser_Term_doId_formatter(lean_object*, lean_object*, lean_
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;
extern lean_object* l_Lean_Parser_Term_emptyC___closed__3;
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*);
@ -670,7 +672,6 @@ lean_object* l_Lean_Parser_regBuiltinDoElemParserAttr___closed__2;
lean_object* l_Lean_Parser_Term_doId_formatter___closed__1;
lean_object* l_Lean_Parser_Term_doPat_formatter___closed__8;
lean_object* l_Lean_Parser_Term_doSeqBracketed_parenthesizer___closed__5;
extern lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__1;
extern lean_object* l_Lean_Parser_Term_have_formatter___closed__4;
extern lean_object* l_Lean_Parser_Term_if_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__13;
@ -695,6 +696,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_doMatch(lean_object*);
lean_object* l_Lean_Parser_Term_doSeqIndent_formatter___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Term_continue_formatter(lean_object*);
lean_object* l_Lean_Parser_Term_doLet_parenthesizer___closed__1;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented___closed__2;
lean_object* l_Lean_Parser_Term_doFor_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doLet_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doFor___closed__7;
@ -702,6 +704,7 @@ lean_object* l_Lean_Parser_Term_liftMethod;
lean_object* l_Lean_PrettyPrinter_Formatter_symbol_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__10;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Bracketed_formatter___closed__6;
lean_object* l___regBuiltin_Lean_Parser_Term_liftMethod_formatter___closed__1;
lean_object* l_Lean_Parser_Term_liftMethod_formatter___closed__3;
lean_object* l_Lean_Parser_Term_doLetArrow___closed__4;
@ -751,7 +754,6 @@ extern lean_object* l_Lean_Parser_Parser_inhabited___closed__1;
lean_object* l_Lean_Parser_Term_liftMethod_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doSeqBracketed;
lean_object* l_Lean_Parser_Term_doLet;
extern lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__5;
lean_object* l_Lean_Parser_Term_doMatchAlt;
lean_object* l_Lean_Parser_Term_doExpr;
lean_object* l_Lean_Parser_Term_doHave___elambda__1___closed__3;
@ -759,11 +761,9 @@ lean_object* l_Lean_Parser_Term_doExpr___closed__3;
lean_object* l_Lean_Parser_Term_doId___closed__6;
lean_object* l_Lean_Parser_Term_leftArrow___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_continue_formatter___closed__3;
extern lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__7;
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*);
lean_object* l_Lean_Parser_Term_doMatchAlts___elambda__1___closed__4;
extern lean_object* l_Lean_Parser_Term_emptyC_formatter___closed__4;
lean_object* l_Lean_Parser_Term_break___closed__2;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__17;
lean_object* l_Lean_Parser_Term_doMatchAlts_parenthesizer___closed__1;
@ -1665,13 +1665,13 @@ lean_object* x_42; lean_object* x_43; uint8_t x_44;
x_42 = lean_ctor_get(x_41, 1);
lean_inc(x_42);
lean_dec(x_41);
x_43 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__1;
x_43 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__1;
x_44 = lean_string_dec_eq(x_42, x_43);
lean_dec(x_42);
if (x_44 == 0)
{
lean_object* x_45; lean_object* x_46;
x_45 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__5;
x_45 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__5;
lean_inc(x_25);
x_46 = l_Lean_Parser_ParserState_mkErrorsAt(x_38, x_45, x_25);
x_26 = x_46;
@ -1687,7 +1687,7 @@ else
{
lean_object* x_47; lean_object* x_48;
lean_dec(x_41);
x_47 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__5;
x_47 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__5;
lean_inc(x_25);
x_48 = l_Lean_Parser_ParserState_mkErrorsAt(x_38, x_47, x_25);
x_26 = x_48;
@ -1698,7 +1698,7 @@ else
{
lean_object* x_49; lean_object* x_50;
lean_dec(x_39);
x_49 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__5;
x_49 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__5;
lean_inc(x_25);
x_50 = l_Lean_Parser_ParserState_mkErrorsAt(x_38, x_49, x_25);
x_26 = x_50;
@ -1869,13 +1869,13 @@ lean_object* x_45; lean_object* x_46; uint8_t x_47;
x_45 = lean_ctor_get(x_44, 1);
lean_inc(x_45);
lean_dec(x_44);
x_46 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__1;
x_46 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__1;
x_47 = lean_string_dec_eq(x_45, x_46);
lean_dec(x_45);
if (x_47 == 0)
{
lean_object* x_48; lean_object* x_49;
x_48 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__5;
x_48 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__5;
lean_inc(x_28);
x_49 = l_Lean_Parser_ParserState_mkErrorsAt(x_41, x_48, x_28);
x_29 = x_49;
@ -1891,7 +1891,7 @@ else
{
lean_object* x_50; lean_object* x_51;
lean_dec(x_44);
x_50 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__5;
x_50 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__5;
lean_inc(x_28);
x_51 = l_Lean_Parser_ParserState_mkErrorsAt(x_41, x_50, x_28);
x_29 = x_51;
@ -1902,7 +1902,7 @@ else
{
lean_object* x_52; lean_object* x_53;
lean_dec(x_42);
x_52 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__5;
x_52 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__5;
lean_inc(x_28);
x_53 = l_Lean_Parser_ParserState_mkErrorsAt(x_41, x_52, x_28);
x_29 = x_53;
@ -2080,13 +2080,13 @@ lean_object* x_104; lean_object* x_105; uint8_t x_106;
x_104 = lean_ctor_get(x_103, 1);
lean_inc(x_104);
lean_dec(x_103);
x_105 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__1;
x_105 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__1;
x_106 = lean_string_dec_eq(x_104, x_105);
lean_dec(x_104);
if (x_106 == 0)
{
lean_object* x_107; lean_object* x_108;
x_107 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__5;
x_107 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__5;
lean_inc(x_87);
x_108 = l_Lean_Parser_ParserState_mkErrorsAt(x_100, x_107, x_87);
x_88 = x_108;
@ -2102,7 +2102,7 @@ else
{
lean_object* x_109; lean_object* x_110;
lean_dec(x_103);
x_109 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__5;
x_109 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__5;
lean_inc(x_87);
x_110 = l_Lean_Parser_ParserState_mkErrorsAt(x_100, x_109, x_87);
x_88 = x_110;
@ -2113,7 +2113,7 @@ else
{
lean_object* x_111; lean_object* x_112;
lean_dec(x_101);
x_111 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__5;
x_111 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__5;
lean_inc(x_87);
x_112 = l_Lean_Parser_ParserState_mkErrorsAt(x_100, x_111, x_87);
x_88 = x_112;
@ -2193,7 +2193,7 @@ lean_object* _init_l_Lean_Parser_Term_doSeqIndent___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_indentedNonEmptySeq___closed__2;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__2;
x_2 = l_Lean_Parser_optionaInfo(x_1);
return x_2;
}
@ -2292,13 +2292,13 @@ lean_object* x_27; lean_object* x_28; uint8_t x_29;
x_27 = lean_ctor_get(x_26, 1);
lean_inc(x_27);
lean_dec(x_26);
x_28 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__1;
x_28 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__1;
x_29 = lean_string_dec_eq(x_27, x_28);
lean_dec(x_27);
if (x_29 == 0)
{
lean_object* x_30; lean_object* x_31;
x_30 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__5;
x_30 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__5;
lean_inc(x_15);
x_31 = l_Lean_Parser_ParserState_mkErrorsAt(x_23, x_30, x_15);
x_16 = x_31;
@ -2314,7 +2314,7 @@ else
{
lean_object* x_32; lean_object* x_33;
lean_dec(x_26);
x_32 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__5;
x_32 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__5;
lean_inc(x_15);
x_33 = l_Lean_Parser_ParserState_mkErrorsAt(x_23, x_32, x_15);
x_16 = x_33;
@ -2325,7 +2325,7 @@ else
{
lean_object* x_34; lean_object* x_35;
lean_dec(x_24);
x_34 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_indentedNonEmptySeq___spec__2___closed__5;
x_34 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___spec__2___closed__5;
lean_inc(x_15);
x_35 = l_Lean_Parser_ParserState_mkErrorsAt(x_23, x_34, x_15);
x_16 = x_35;
@ -2499,13 +2499,13 @@ lean_object* x_48; lean_object* x_49; uint8_t x_50;
x_48 = lean_ctor_get(x_47, 1);
lean_inc(x_48);
lean_dec(x_47);
x_49 = l_Lean_Parser_Term_emptyC___elambda__1___closed__7;
x_49 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__5;
x_50 = lean_string_dec_eq(x_48, x_49);
lean_dec(x_48);
if (x_50 == 0)
{
lean_object* x_51; lean_object* x_52;
x_51 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_51 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
x_52 = l_Lean_Parser_ParserState_mkErrorsAt(x_44, x_51, x_43);
x_11 = x_52;
goto block_42;
@ -2521,7 +2521,7 @@ else
{
lean_object* x_53; lean_object* x_54;
lean_dec(x_47);
x_53 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_53 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
x_54 = l_Lean_Parser_ParserState_mkErrorsAt(x_44, x_53, x_43);
x_11 = x_54;
goto block_42;
@ -2531,7 +2531,7 @@ else
{
lean_object* x_55; lean_object* x_56;
lean_dec(x_45);
x_55 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_55 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
x_56 = l_Lean_Parser_ParserState_mkErrorsAt(x_44, x_55, x_43);
x_11 = x_56;
goto block_42;
@ -2570,13 +2570,13 @@ lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_21 = lean_ctor_get(x_20, 1);
lean_inc(x_21);
lean_dec(x_20);
x_22 = l_Lean_Parser_Term_emptyC___elambda__1___closed__8;
x_22 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__6;
x_23 = lean_string_dec_eq(x_21, x_22);
lean_dec(x_21);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_24 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_24 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_24, x_16);
x_26 = l_Lean_Parser_Term_doSeqBracketed___elambda__1___closed__2;
x_27 = l_Lean_Parser_ParserState_mkNode(x_25, x_26, x_10);
@ -2595,7 +2595,7 @@ else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
lean_dec(x_20);
x_30 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_30 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_31 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_30, x_16);
x_32 = l_Lean_Parser_Term_doSeqBracketed___elambda__1___closed__2;
x_33 = l_Lean_Parser_ParserState_mkNode(x_31, x_32, x_10);
@ -2606,7 +2606,7 @@ else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37;
lean_dec(x_18);
x_34 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_34 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_35 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_34, x_16);
x_36 = l_Lean_Parser_Term_doSeqBracketed___elambda__1___closed__2;
x_37 = l_Lean_Parser_ParserState_mkNode(x_35, x_36, x_10);
@ -2715,13 +2715,13 @@ lean_object* x_115; lean_object* x_116; uint8_t x_117;
x_115 = lean_ctor_get(x_114, 1);
lean_inc(x_115);
lean_dec(x_114);
x_116 = l_Lean_Parser_Term_emptyC___elambda__1___closed__7;
x_116 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__5;
x_117 = lean_string_dec_eq(x_115, x_116);
lean_dec(x_115);
if (x_117 == 0)
{
lean_object* x_118; lean_object* x_119;
x_118 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_118 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
x_119 = l_Lean_Parser_ParserState_mkErrorsAt(x_111, x_118, x_110);
x_71 = x_119;
goto block_109;
@ -2737,7 +2737,7 @@ else
{
lean_object* x_120; lean_object* x_121;
lean_dec(x_114);
x_120 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_120 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
x_121 = l_Lean_Parser_ParserState_mkErrorsAt(x_111, x_120, x_110);
x_71 = x_121;
goto block_109;
@ -2747,7 +2747,7 @@ else
{
lean_object* x_122; lean_object* x_123;
lean_dec(x_112);
x_122 = l_Lean_Parser_Term_emptyC___elambda__1___closed__14;
x_122 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__12;
x_123 = l_Lean_Parser_ParserState_mkErrorsAt(x_111, x_122, x_110);
x_71 = x_123;
goto block_109;
@ -2786,13 +2786,13 @@ lean_object* x_81; lean_object* x_82; uint8_t x_83;
x_81 = lean_ctor_get(x_80, 1);
lean_inc(x_81);
lean_dec(x_80);
x_82 = l_Lean_Parser_Term_emptyC___elambda__1___closed__8;
x_82 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__6;
x_83 = lean_string_dec_eq(x_81, x_82);
lean_dec(x_81);
if (x_83 == 0)
{
lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88;
x_84 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_84 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_85 = l_Lean_Parser_ParserState_mkErrorsAt(x_77, x_84, x_76);
x_86 = l_Lean_Parser_Term_doSeqBracketed___elambda__1___closed__2;
x_87 = l_Lean_Parser_ParserState_mkNode(x_85, x_86, x_70);
@ -2815,7 +2815,7 @@ else
{
lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96;
lean_dec(x_80);
x_92 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_92 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_93 = l_Lean_Parser_ParserState_mkErrorsAt(x_77, x_92, x_76);
x_94 = l_Lean_Parser_Term_doSeqBracketed___elambda__1___closed__2;
x_95 = l_Lean_Parser_ParserState_mkNode(x_93, x_94, x_70);
@ -2828,7 +2828,7 @@ else
{
lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101;
lean_dec(x_78);
x_97 = l_Lean_Parser_Term_emptyC___elambda__1___closed__11;
x_97 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___elambda__1___closed__9;
x_98 = l_Lean_Parser_ParserState_mkErrorsAt(x_77, x_97, x_76);
x_99 = l_Lean_Parser_Term_doSeqBracketed___elambda__1___closed__2;
x_100 = l_Lean_Parser_ParserState_mkNode(x_98, x_99, x_70);
@ -2885,7 +2885,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_doSeqIndent___closed__1;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Tactic_indentedNonEmptySeq___closed__2;
x_3 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__2;
x_4 = l_Lean_Parser_sepBy1Info(x_2, x_3);
return x_4;
}
@ -2895,7 +2895,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_doSeqBracketed___closed__1;
x_2 = l_Lean_Parser_Term_emptyC___closed__3;
x_2 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___closed__3;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
@ -2904,7 +2904,7 @@ lean_object* _init_l_Lean_Parser_Term_doSeqBracketed___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_emptyC___closed__2;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Bracketed___closed__1;
x_2 = l_Lean_Parser_Term_doSeqBracketed___closed__2;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
@ -9630,7 +9630,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_doSeqBracketed_formatter___closed__2;
x_2 = l_Lean_Parser_Tactic_indentedNonEmptySeq_formatter___closed__1;
x_2 = l_Lean_Parser_Tactic_tacticSeq1Bracketed_formatter___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_sepBy1_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -9642,7 +9642,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_doSeqBracketed_formatter___closed__3;
x_2 = l_Lean_Parser_Term_emptyC_formatter___closed__4;
x_2 = l_Lean_Parser_Tactic_tacticSeq1Bracketed_formatter___closed__6;
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);
@ -9653,7 +9653,7 @@ lean_object* _init_l_Lean_Parser_Term_doSeqBracketed_formatter___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_emptyC_formatter___closed__3;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Bracketed_formatter___closed__2;
x_2 = l_Lean_Parser_Term_doSeqBracketed_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);
@ -9689,7 +9689,7 @@ lean_object* _init_l_Lean_Parser_Term_doSeqIndent_formatter___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_indentedNonEmptySeq_formatter___closed__1;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Bracketed_formatter___closed__3;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_optional_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -9711,7 +9711,7 @@ lean_object* _init_l_Lean_Parser_Term_doSeqIndent_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_indentedNonEmptySeq_formatter___closed__2;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented_formatter___closed__1;
x_2 = l_Lean_Parser_Term_doSeqIndent_formatter___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -9849,7 +9849,7 @@ lean_object* _init_l_Lean_Parser_Term_doIf_formatter___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_indentedNonEmptySeq_formatter___closed__2;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented_formatter___closed__1;
x_2 = l_Lean_Parser_Term_doIf_formatter___closed__8;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -9883,7 +9883,7 @@ lean_object* _init_l_Lean_Parser_Term_doIf_formatter___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_indentedNonEmptySeq_formatter___closed__2;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented_formatter___closed__1;
x_2 = l_Lean_Parser_Term_doIf_formatter___closed__11;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -10122,7 +10122,7 @@ lean_object* _init_l_Lean_Parser_Term_doSeqIndent_parenthesizer___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_indentedNonEmptySeq_parenthesizer___closed__2;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented_parenthesizer___closed__1;
x_2 = l_Lean_Parser_Term_doSeqIndent_parenthesizer___closed__1;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -10226,7 +10226,7 @@ lean_object* _init_l_Lean_Parser_Term_doIf_parenthesizer___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_indentedNonEmptySeq_parenthesizer___closed__2;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented_parenthesizer___closed__1;
x_2 = l_Lean_Parser_Term_doIf_parenthesizer___closed__5;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -10248,7 +10248,7 @@ lean_object* _init_l_Lean_Parser_Term_doIf_parenthesizer___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_indentedNonEmptySeq_parenthesizer___closed__2;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented_parenthesizer___closed__1;
x_2 = l_Lean_Parser_Term_doIf_parenthesizer___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);

4
stage0/stdlib/Lean/Parser/Syntax.c generated
View file

@ -430,6 +430,7 @@ lean_object* l_Lean_Parser_Syntax_ident___closed__5;
lean_object* l_Lean_Parser_Syntax_sepBy___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_notation___closed__6;
lean_object* l_Lean_Parser_Command_infixl_formatter___closed__2;
extern lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__3;
lean_object* l_Lean_Parser_Command_mixfix___closed__9;
lean_object* l_Lean_Parser_Syntax_try_parenthesizer___closed__4;
lean_object* l_Lean_Parser_maxSymbol_formatter___closed__3;
@ -986,7 +987,6 @@ lean_object* l_Lean_Parser_Command_mixfix___closed__5;
lean_object* l_Lean_Parser_Syntax_cat_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_elab__rules___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_syntaxAbbrev___closed__3;
extern lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__4;
lean_object* l_Lean_Parser_Command_notation_formatter___closed__4;
extern lean_object* l_Lean_Parser_Term_str_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Syntax_notFollowedBy___closed__7;
@ -23476,7 +23476,7 @@ lean_inc(x_23);
if (lean_obj_tag(x_23) == 0)
{
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = l_Lean_Parser_Tactic_seq1Unbox___closed__4;
x_24 = l_Lean_Parser_Tactic_seq1Unbox___closed__3;
lean_inc(x_1);
x_25 = l_Lean_Parser_toggleInsideQuotFn(x_24, x_1, x_22);
x_26 = lean_ctor_get(x_25, 3);

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

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff