diff --git a/stage0/src/Lean/Parser/Tactic.lean b/stage0/src/Lean/Parser/Tactic.lean index fd7ce55693..24c073925f 100644 --- a/stage0/src/Lean/Parser/Tactic.lean +++ b/stage0/src/Lean/Parser/Tactic.lean @@ -26,7 +26,7 @@ def underscoreFn : ParserFn := fun c s => @[combinatorParenthesizer Lean.Parser.Tactic.underscore] def underscore.parenthesizer := PrettyPrinter.Parenthesizer.rawIdent.parenthesizer @[combinatorFormatter Lean.Parser.Tactic.underscore] def underscore.formatter := PrettyPrinter.Formatter.rawIdent.formatter -def ident' : Parser := ident <|> underscore +def ident' : Parser := ident <|> (checkInsideQuot >> Term.hole) <|> (checkOutsideQuot >> underscore) @[builtinTacticParser] def «intro» := parser! nonReservedSymbol "intro " >> notSymbol "|" >> many (checkColGt >> termParser maxPrec) @[builtinTacticParser] def «intros» := parser! nonReservedSymbol "intros " >> many (checkColGt >> ident') diff --git a/stage0/stdlib/Lean/Parser/Tactic.c b/stage0/stdlib/Lean/Parser/Tactic.c index a886c76de0..5cd93c7e52 100644 --- a/stage0/stdlib/Lean/Parser/Tactic.c +++ b/stage0/stdlib/Lean/Parser/Tactic.c @@ -128,6 +128,7 @@ lean_object* l_Lean_Parser_Tactic_altRHS___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_rwRuleSeq___elambda__1___closed__7; lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_locationWildcard_parenthesizer___closed__2; +lean_object* l_Lean_Parser_Tactic_ident_x27_formatter___closed__6; lean_object* l_Lean_Parser_Tactic_traceState_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__5; lean_object* l_Lean_Parser_Tactic_intro___closed__9; @@ -218,6 +219,7 @@ lean_object* l_Lean_Parser_Tactic_location_parenthesizer___closed__7; lean_object* l_Lean_Parser_Tactic_match_formatter___closed__4; lean_object* l_Lean_Parser_Tactic_changeWith___elambda__1___closed__1; lean_object* l___regBuiltin_Lean_Parser_Tactic_have_parenthesizer(lean_object*); +lean_object* l_Lean_PrettyPrinter_Formatter_checkInsideQuot_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Tactic_introMatch(lean_object*); lean_object* l_Lean_Parser_Tactic_clear_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Parser_Tactic_skip_parenthesizer___closed__1; @@ -287,6 +289,7 @@ lean_object* l_Lean_Parser_nonReservedSymbolFn(lean_object*, lean_object*, lean_ lean_object* l_Lean_Parser_Tactic_rewrite___elambda__1___closed__14; lean_object* l_Lean_Parser_Tactic_matchAlts___closed__1; lean_object* l_Lean_Parser_Tactic_paren_parenthesizer___closed__2; +lean_object* l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__3; lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_apply___closed__4; lean_object* l_Lean_Parser_Tactic_orelse_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -372,6 +375,7 @@ extern lean_object* l_Lean_Parser_Term_syntheticHole___closed__7; lean_object* l_Lean_Parser_Tactic_rewrite___elambda__1___closed__15; lean_object* l_Lean_Parser_Tactic_refine_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Parser_Tactic_revert_formatter(lean_object*); +lean_object* l_Lean_Parser_Tactic_ident_x27___closed__5; lean_object* lean_string_append(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_location___elambda__1___closed__7; lean_object* l_Lean_Parser_Tactic_induction_formatter___closed__5; @@ -385,6 +389,7 @@ lean_object* l_Lean_Parser_Tactic_changeWith_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_show___elambda__1___closed__2; lean_object* l_Lean_Parser_Tactic_introMatch_parenthesizer___closed__2; lean_object* l_Lean_Parser_Tactic_rewrite___elambda__1___closed__13; +lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_change___closed__9; lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__14; lean_object* l_Lean_Parser_Tactic_cases_formatter___closed__6; @@ -579,6 +584,7 @@ lean_object* l_Lean_Parser_Tactic_case_parenthesizer___closed__5; extern lean_object* l___regBuiltin_Lean_Parser_Term_hole_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_subst___elambda__1___closed__5; lean_object* l_Lean_Parser_Tactic_induction_parenthesizer___closed__7; +lean_object* l_Lean_Parser_Tactic_ident_x27___closed__4; lean_object* l_Lean_Parser_Tactic_cases___closed__4; extern lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute; lean_object* l___regBuiltin_Lean_Parser_Tactic_case_formatter___closed__1; @@ -598,6 +604,7 @@ extern lean_object* l_Lean_Parser_Term_hole___closed__4; lean_object* l___regBuiltin_Lean_Parser_Tactic_let_formatter___closed__1; lean_object* l___regBuiltinParser_Lean_Parser_Tactic_focus(lean_object*); lean_object* l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_5____closed__1; +extern lean_object* l_Lean_Parser_checkOutsideQuot___closed__1; lean_object* l_Lean_Parser_Tactic_generalizingVars___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_change___closed__2; lean_object* l_Lean_Parser_Tactic_usingRec___elambda__1___closed__4; @@ -653,6 +660,7 @@ lean_object* l_Lean_Parser_Tactic_traceState___closed__1; lean_object* l___regBuiltin_Lean_Parser_Tactic_let_x21_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_match___elambda__1___closed__6; lean_object* l_Lean_Parser_Tactic_inductionAlts_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__5; lean_object* l_Lean_Parser_Tactic_generalize___closed__9; lean_object* l_Lean_Parser_Tactic_case_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_location___closed__2; @@ -741,6 +749,7 @@ extern lean_object* l_Lean_Parser_Term_letDecl; lean_object* l_Lean_Parser_Tactic_locationHyp___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_rwRule_parenthesizer___closed__5; lean_object* l___regBuiltin_Lean_Parser_Tactic_traceState_parenthesizer(lean_object*); +lean_object* l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__3; lean_object* l_Lean_Parser_Tactic_intros_formatter___closed__4; lean_object* l_Lean_Parser_Tactic_usingRec___elambda__1___closed__1; extern lean_object* l_Lean_Parser_Term_matchAlts_formatter___closed__5; @@ -944,6 +953,7 @@ lean_object* l_Lean_Parser_Tactic_rewriteSeq___elambda__1___closed__7; lean_object* l_Lean_Parser_Tactic_location___closed__8; lean_object* l_Lean_Parser_Tactic_exact___closed__3; lean_object* l_Lean_Parser_Tactic_inductionAlts___closed__3; +lean_object* l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__6; lean_object* l_Lean_Parser_Tactic_paren___closed__5; lean_object* l_Lean_Parser_Tactic_location_parenthesizer___closed__2; lean_object* l___regBuiltin_Lean_Parser_Tactic_unknown_formatter___closed__1; @@ -1013,6 +1023,7 @@ lean_object* l_Lean_Parser_Tactic_location_parenthesizer___closed__4; lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__5; lean_object* l_Lean_Parser_Tactic_majorPremise___elambda__1___closed__2; lean_object* l_Lean_Parser_Tactic_suffices___closed__1; +lean_object* l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__4; lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__5; lean_object* l_Lean_Parser_Tactic_inductionAlt_formatter___closed__3; lean_object* l_Lean_Parser_Tactic_case_parenthesizer___closed__2; @@ -1037,6 +1048,7 @@ lean_object* l_Lean_Parser_Tactic_induction_formatter___closed__8; lean_object* l_Lean_Parser_Tactic_refine_x21___elambda__1___closed__5; lean_object* l_Lean_Parser_Tactic_matchAlt___elambda__1___closed__4; lean_object* l_Lean_Parser_Tactic_introMatch___elambda__1___closed__3; +lean_object* l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__2; lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__10; @@ -1096,6 +1108,7 @@ lean_object* l_Lean_Parser_Tactic_paren___closed__1; lean_object* l_Lean_Parser_Tactic_rewrite___elambda__1___closed__4; lean_object* l___regBuiltin_Lean_Parser_Tactic_assumption_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_have___closed__3; +lean_object* l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__2; extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__3; lean_object* l_Lean_Parser_Tactic_done___closed__2; lean_object* l_Lean_Parser_Tactic_change___closed__3; @@ -1182,6 +1195,7 @@ lean_object* l_Lean_Parser_Tactic_injection___elambda__1___closed__4; lean_object* l_Lean_Parser_Tactic_intros___closed__4; lean_object* l_Lean_Parser_Tactic_rewrite_parenthesizer___closed__10; extern lean_object* l___kind_tactic____x40_Init_Tactics___hyg_461____closed__2; +extern lean_object* l_Lean_Parser_checkInsideQuot___closed__1; lean_object* l_Lean_Parser_Tactic_rewrite___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_matchAlt_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_unknown_formatter___closed__4; @@ -1360,6 +1374,7 @@ lean_object* l_Lean_Parser_Tactic_revert___closed__7; lean_object* l___regBuiltinParser_Lean_Parser_Tactic_letrec(lean_object*); lean_object* l_Lean_Parser_Tactic_matchAlt_parenthesizer___closed__3; lean_object* l_Lean_Parser_Tactic_allGoals___closed__5; +lean_object* l_Lean_Parser_Tactic_ident_x27___closed__6; 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; lean_object* l_Lean_Parser_Tactic_generalize_formatter___closed__5; @@ -1485,6 +1500,7 @@ lean_object* l_Lean_Parser_Tactic_rewriteSeq___closed__5; extern lean_object* l_Lean_Parser_Term_matchAlts___closed__2; lean_object* l_Lean_Parser_Tactic_done; lean_object* l_Lean_Parser_Tactic_show_formatter___closed__2; +lean_object* l_Lean_PrettyPrinter_Formatter_checkOutsideQuot_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Parser_Tactic_revert_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_locationWildcard___elambda__1___closed__5; lean_object* l_Lean_Parser_Tactic_withAlts_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1603,6 +1619,7 @@ lean_object* l_Lean_Parser_Tactic_intros_formatter___closed__7; lean_object* l_Lean_Parser_Tactic_let_parenthesizer___closed__2; lean_object* l_Lean_Parser_Tactic_injection; lean_object* l_Lean_Parser_Tactic_induction_formatter___closed__9; +lean_object* l_Lean_Parser_Tactic_ident_x27_formatter___closed__4; lean_object* l_Lean_Parser_Tactic_exact___closed__2; lean_object* l_Lean_Parser_Tactic_suffices___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_rewrite_parenthesizer___closed__7; @@ -1631,6 +1648,7 @@ lean_object* l_Lean_Parser_Tactic_refine_x21___elambda__1___closed__9; lean_object* l_Lean_Parser_Tactic_paren___elambda__1___closed__5; extern lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__6; lean_object* l_Lean_Parser_Tactic_cases___elambda__1(lean_object*, lean_object*); +lean_object* l_Lean_Parser_Tactic_ident_x27_formatter___closed__2; lean_object* l___regBuiltinParser_Lean_Parser_Tactic_rewrite(lean_object*); lean_object* l_Lean_Parser_Tactic_underscoreFn___closed__1; lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__12; @@ -1703,6 +1721,7 @@ 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; lean_object* l_Lean_Parser_Tactic_rwRuleSeq_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Tactic_ident_x27_formatter___closed__5; lean_object* l_Lean_Parser_Tactic_clear_parenthesizer___closed__3; lean_object* l___regBuiltin_Lean_Parser_Tactic_rewrite_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_locationHyp___closed__2; @@ -1758,6 +1777,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Tactic_subst(lean_object*); lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__4; lean_object* l_Lean_Parser_Tactic_refine___elambda__1___closed__1; lean_object* l___regBuiltin_Lean_Parser_Tactic_suffices_parenthesizer___closed__1; +lean_object* l_Lean_Parser_Tactic_ident_x27_formatter___closed__3; lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_let___elambda__1___closed__6; lean_object* l_Lean_Parser_Tactic_locationHyp___closed__1; @@ -1815,6 +1835,7 @@ lean_object* l_Lean_Parser_Tactic_locationHyp_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_matchAlts_formatter___closed__4; lean_object* l_Lean_Parser_Tactic_letrec_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_unknown___elambda__1___lambda__1(lean_object*, lean_object*); +lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Tactic_traceState(lean_object*); lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__8; lean_object* l_Lean_Parser_Tactic_rewriteSeq___closed__1; @@ -1866,6 +1887,7 @@ lean_object* l_Lean_Parser_Tactic_assumption___elambda__1___closed__5; extern lean_object* l_Lean_Parser_Term_letrec_parenthesizer___closed__7; lean_object* l_Lean_Parser_Tactic_let_x21_formatter___closed__2; lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__10; +lean_object* l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__2; lean_object* l_Lean_Parser_Tactic_rwRule___closed__5; lean_object* l___regBuiltin_Lean_Parser_Tactic_generalize_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_underscore_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*); @@ -2157,12 +2179,48 @@ lean_dec(x_1); return x_6; } } +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_checkInsideQuot___closed__1; +x_2 = l_Lean_Parser_Term_hole___closed__4; +x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_checkOutsideQuot___closed__1; +x_2 = l_Lean_Parser_Tactic_underscore___closed__1; +x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__1; +x_2 = l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__2; +x_3 = lean_alloc_closure((void*)(l_Lean_Parser_orelseFn), 4, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} lean_object* l_Lean_Parser_Tactic_ident_x27___elambda__1(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6; x_3 = l_Lean_Parser_ident___closed__2; -x_4 = l_Lean_Parser_Tactic_underscore___closed__1; +x_4 = l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__3; x_5 = 1; x_6 = l_Lean_Parser_orelseFnCore(x_3, x_4, x_5, x_1, x_2); return x_6; @@ -2172,20 +2230,22 @@ static lean_object* _init_l_Lean_Parser_Tactic_ident_x27___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_ident; +x_1 = l_Lean_Parser_Term_hole; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_identNoAntiquot___closed__1; -x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); +x_3 = l_Lean_Parser_epsilonInfo; +x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); return x_4; } } static lean_object* _init_l_Lean_Parser_Tactic_ident_x27___closed__2() { _start: { -lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_ident_x27___elambda__1), 2, 0); -return x_1; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_epsilonInfo; +x_2 = l_Lean_Parser_identNoAntiquot___closed__1; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; } } static lean_object* _init_l_Lean_Parser_Tactic_ident_x27___closed__3() { @@ -2194,6 +2254,36 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Tactic_ident_x27___closed__1; x_2 = l_Lean_Parser_Tactic_ident_x27___closed__2; +x_3 = l_Lean_Parser_orelseInfo(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_ident; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Tactic_ident_x27___closed__3; +x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); +return x_4; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27___closed__5() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_ident_x27___elambda__1), 2, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_ident_x27___closed__4; +x_2 = l_Lean_Parser_Tactic_ident_x27___closed__5; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -2204,7 +2294,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_ident_x27() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Tactic_ident_x27___closed__3; +x_1 = l_Lean_Parser_Tactic_ident_x27___closed__6; return x_1; } } @@ -2824,7 +2914,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1841____closed__23; -x_2 = l_Lean_Parser_Tactic_ident_x27___closed__2; +x_2 = l_Lean_Parser_Tactic_ident_x27___closed__5; x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2); lean_closure_set(x_3, 0, x_1); lean_closure_set(x_3, 1, x_2); @@ -3008,16 +3098,68 @@ static lean_object* _init_l_Lean_Parser_Tactic_ident_x27_formatter___closed__1() _start: { lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkInsideQuot_formatter___boxed), 4, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27_formatter___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_ident_x27_formatter___closed__1; +x_2 = l___regBuiltin_Lean_Parser_Term_hole_formatter___closed__1; +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; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27_formatter___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkOutsideQuot_formatter___boxed), 4, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27_formatter___closed__4() { +_start: +{ +lean_object* x_1; x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_underscore_formatter___boxed), 5, 0); return x_1; } } +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27_formatter___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_ident_x27_formatter___closed__3; +x_2 = l_Lean_Parser_Tactic_ident_x27_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; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27_formatter___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_ident_x27_formatter___closed__2; +x_2 = l_Lean_Parser_Tactic_ident_x27_formatter___closed__5; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_orelse_formatter), 7, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} lean_object* l_Lean_Parser_Tactic_ident_x27_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; x_6 = l_Lean_Parser_Level_ident_formatter___closed__1; -x_7 = l_Lean_Parser_Tactic_ident_x27_formatter___closed__1; +x_7 = l_Lean_Parser_Tactic_ident_x27_formatter___closed__6; 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; } @@ -3136,16 +3278,68 @@ static lean_object* _init_l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed_ _start: { lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___boxed), 4, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__1; +x_2 = l___regBuiltin_Lean_Parser_Term_hole_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); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___boxed), 4, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__4() { +_start: +{ +lean_object* x_1; x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_underscore_parenthesizer___boxed), 1, 0); return x_1; } } +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__3; +x_2 = l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__4; +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; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__2; +x_2 = l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__5; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer), 7, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} lean_object* l_Lean_Parser_Tactic_ident_x27_parenthesizer(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; x_6 = l_Lean_Parser_Level_ident_parenthesizer___closed__1; -x_7 = l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__1; +x_7 = l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__6; 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; } @@ -14021,7 +14215,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__4() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Tactic_ident_x27___closed__2; +x_1 = l_Lean_Parser_Tactic_ident_x27___closed__5; x_2 = lean_alloc_closure((void*)(l_Lean_Parser_manyFn), 3, 1); lean_closure_set(x_2, 0, x_1); return x_2; @@ -14091,7 +14285,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__10() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Tactic_ident_x27___closed__2; +x_1 = l_Lean_Parser_Tactic_ident_x27___closed__5; x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__8; x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2); lean_closure_set(x_3, 0, x_1); @@ -20927,12 +21121,24 @@ l_Lean_Parser_Tactic_underscore___closed__2 = _init_l_Lean_Parser_Tactic_undersc lean_mark_persistent(l_Lean_Parser_Tactic_underscore___closed__2); l_Lean_Parser_Tactic_underscore = _init_l_Lean_Parser_Tactic_underscore(); lean_mark_persistent(l_Lean_Parser_Tactic_underscore); +l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__1(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__1); +l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__2); +l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__3 = _init_l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27___elambda__1___closed__3); l_Lean_Parser_Tactic_ident_x27___closed__1 = _init_l_Lean_Parser_Tactic_ident_x27___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27___closed__1); l_Lean_Parser_Tactic_ident_x27___closed__2 = _init_l_Lean_Parser_Tactic_ident_x27___closed__2(); lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27___closed__2); l_Lean_Parser_Tactic_ident_x27___closed__3 = _init_l_Lean_Parser_Tactic_ident_x27___closed__3(); lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27___closed__3); +l_Lean_Parser_Tactic_ident_x27___closed__4 = _init_l_Lean_Parser_Tactic_ident_x27___closed__4(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27___closed__4); +l_Lean_Parser_Tactic_ident_x27___closed__5 = _init_l_Lean_Parser_Tactic_ident_x27___closed__5(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27___closed__5); +l_Lean_Parser_Tactic_ident_x27___closed__6 = _init_l_Lean_Parser_Tactic_ident_x27___closed__6(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27___closed__6); l_Lean_Parser_Tactic_ident_x27 = _init_l_Lean_Parser_Tactic_ident_x27(); lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27); l_Lean_Parser_Tactic_intro___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_intro___elambda__1___closed__1(); @@ -21081,6 +21287,16 @@ if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l_Lean_Parser_Tactic_ident_x27_formatter___closed__1 = _init_l_Lean_Parser_Tactic_ident_x27_formatter___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27_formatter___closed__1); +l_Lean_Parser_Tactic_ident_x27_formatter___closed__2 = _init_l_Lean_Parser_Tactic_ident_x27_formatter___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27_formatter___closed__2); +l_Lean_Parser_Tactic_ident_x27_formatter___closed__3 = _init_l_Lean_Parser_Tactic_ident_x27_formatter___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27_formatter___closed__3); +l_Lean_Parser_Tactic_ident_x27_formatter___closed__4 = _init_l_Lean_Parser_Tactic_ident_x27_formatter___closed__4(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27_formatter___closed__4); +l_Lean_Parser_Tactic_ident_x27_formatter___closed__5 = _init_l_Lean_Parser_Tactic_ident_x27_formatter___closed__5(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27_formatter___closed__5); +l_Lean_Parser_Tactic_ident_x27_formatter___closed__6 = _init_l_Lean_Parser_Tactic_ident_x27_formatter___closed__6(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27_formatter___closed__6); l_Lean_Parser_Tactic_intros_formatter___closed__1 = _init_l_Lean_Parser_Tactic_intros_formatter___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_intros_formatter___closed__1); l_Lean_Parser_Tactic_intros_formatter___closed__2 = _init_l_Lean_Parser_Tactic_intros_formatter___closed__2(); @@ -21102,6 +21318,16 @@ if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__1); +l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__2); +l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__3 = _init_l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__3); +l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__4 = _init_l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__4(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__4); +l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__5 = _init_l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__5(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__5); +l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__6 = _init_l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__6(); +lean_mark_persistent(l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__6); l_Lean_Parser_Tactic_intros_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_intros_parenthesizer___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_intros_parenthesizer___closed__1); l_Lean_Parser_Tactic_intros_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_intros_parenthesizer___closed__2();