From 489da2720893203bb3ead370a2203cba36aa8189 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Sep 2020 16:49:07 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Lean/Parser/Tactic.lean | 1 + stage0/stdlib/Lean/Delaborator.c | 32 +- stage0/stdlib/Lean/Elab/Binders.c | 3 +- stage0/stdlib/Lean/Elab/BuiltinNotation.c | 1259 +++++++++++++-------- stage0/stdlib/Lean/Elab/Do.c | 9 +- stage0/stdlib/Lean/Elab/Match.c | 6 +- stage0/stdlib/Lean/Elab/Quotation.c | 90 +- stage0/stdlib/Lean/Elab/StructInst.c | 10 +- stage0/stdlib/Lean/Parser/Tactic.c | 559 +++++++++ 9 files changed, 1429 insertions(+), 540 deletions(-) diff --git a/stage0/src/Lean/Parser/Tactic.lean b/stage0/src/Lean/Parser/Tactic.lean index 74943c9fa1..bcd972bb70 100644 --- a/stage0/src/Lean/Parser/Tactic.lean +++ b/stage0/src/Lean/Parser/Tactic.lean @@ -37,6 +37,7 @@ def ident' : Parser := ident <|> underscore @[builtinTacticParser] def «refine!» := parser! nonReservedSymbol "refine! " >> termParser @[builtinTacticParser] def «case» := parser! nonReservedSymbol "case " >> ident >> darrow >> tacticSeq @[builtinTacticParser] def «allGoals» := parser! nonReservedSymbol "allGoals " >> tacticSeq +@[builtinTacticParser] def «focus» := parser! nonReservedSymbol "focus " >> tacticSeq @[builtinTacticParser] def «skip» := parser! nonReservedSymbol "skip" @[builtinTacticParser] def «done» := parser! nonReservedSymbol "done" @[builtinTacticParser] def «admit» := parser! nonReservedSymbol "admit" diff --git a/stage0/stdlib/Lean/Delaborator.c b/stage0/stdlib/Lean/Delaborator.c index 2bd37b6fe6..276957a6df 100644 --- a/stage0/stdlib/Lean/Delaborator.c +++ b/stage0/stdlib/Lean/Delaborator.c @@ -385,6 +385,7 @@ lean_object* l_Lean_Delaborator_delabDiv___lambda__1___boxed(lean_object*, lean_ lean_object* l_Lean_Delaborator_delabOrM___lambda__1___closed__1; lean_object* l___regBuiltin_Lean_Delaborator_delabBAnd___closed__1; lean_object* l___regBuiltin_Lean_Delaborator_delabOr___closed__2; +lean_object* l_Lean_Delaborator_delabLetE___closed__16; lean_object* l_Lean_Delaborator_delabStructureInstance___lambda__1___closed__3; lean_object* l_Lean_Delaborator_delabInfixOp___lambda__2___closed__1; lean_object* l___regBuiltin_Lean_Delaborator_delabCoe___closed__2; @@ -621,6 +622,7 @@ lean_object* l_Array_umapMAux___main___at_Lean_Delaborator_delabConst___spec__1( lean_object* l_Lean_mkSepArray(lean_object*, lean_object*); lean_object* l_Lean_Delaborator_delabProjectionApp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_redLength___main___rarg(lean_object*); +lean_object* l_Lean_Delaborator_delabLetE___closed__15; lean_object* l___private_Lean_Delaborator_2__unresolveUsingNamespace___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Delaborator_mkDelabAttribute___closed__4; lean_object* l___regBuiltin_Lean_Delaborator_delabGE___closed__1; @@ -16563,6 +16565,28 @@ lean_ctor_set(x_3, 1, x_2); return x_3; } } +lean_object* _init_l_Lean_Delaborator_delabLetE___closed__15() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Array_empty___closed__1; +x_2 = l_Lean_Delaborator_delabLetE___closed__14; +x_3 = lean_array_push(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Delaborator_delabLetE___closed__16() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_nullKind___closed__2; +x_2 = l_Lean_Delaborator_delabLetE___closed__15; +x_3 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} lean_object* l_Lean_Delaborator_delabLetE(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { _start: { @@ -16664,7 +16688,7 @@ lean_ctor_set(x_49, 0, x_48); lean_ctor_set(x_49, 1, x_47); x_50 = l_Lean_Delaborator_delabLetE___closed__4; x_51 = lean_array_push(x_50, x_49); -x_52 = l_Lean_Delaborator_delabLetE___closed__14; +x_52 = l_Lean_Delaborator_delabLetE___closed__16; x_53 = lean_array_push(x_51, x_52); x_54 = lean_array_push(x_53, x_28); x_55 = l_Lean_Delaborator_delabLetE___closed__2; @@ -16713,7 +16737,7 @@ lean_ctor_set(x_79, 0, x_78); lean_ctor_set(x_79, 1, x_77); x_80 = l_Lean_Delaborator_delabLetE___closed__4; x_81 = lean_array_push(x_80, x_79); -x_82 = l_Lean_Delaborator_delabLetE___closed__14; +x_82 = l_Lean_Delaborator_delabLetE___closed__16; x_83 = lean_array_push(x_81, x_82); x_84 = lean_array_push(x_83, x_57); x_85 = l_Lean_Delaborator_delabLetE___closed__2; @@ -25479,6 +25503,10 @@ l_Lean_Delaborator_delabLetE___closed__13 = _init_l_Lean_Delaborator_delabLetE__ lean_mark_persistent(l_Lean_Delaborator_delabLetE___closed__13); l_Lean_Delaborator_delabLetE___closed__14 = _init_l_Lean_Delaborator_delabLetE___closed__14(); lean_mark_persistent(l_Lean_Delaborator_delabLetE___closed__14); +l_Lean_Delaborator_delabLetE___closed__15 = _init_l_Lean_Delaborator_delabLetE___closed__15(); +lean_mark_persistent(l_Lean_Delaborator_delabLetE___closed__15); +l_Lean_Delaborator_delabLetE___closed__16 = _init_l_Lean_Delaborator_delabLetE___closed__16(); +lean_mark_persistent(l_Lean_Delaborator_delabLetE___closed__16); l___regBuiltin_Lean_Delaborator_delabLetE___closed__1 = _init_l___regBuiltin_Lean_Delaborator_delabLetE___closed__1(); lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLetE___closed__1); res = l___regBuiltin_Lean_Delaborator_delabLetE(lean_io_mk_world()); diff --git a/stage0/stdlib/Lean/Elab/Binders.c b/stage0/stdlib/Lean/Elab/Binders.c index 2e51a27e9e..61ca1d762b 100644 --- a/stage0/stdlib/Lean/Elab/Binders.c +++ b/stage0/stdlib/Lean/Elab/Binders.c @@ -18,6 +18,7 @@ lean_object* l___private_Lean_Elab_Binders_16__expandMatchAltsIntoMatchAux___mai lean_object* l_Lean_Syntax_updateKind(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabBinder___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabBinders(lean_object*); +extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; lean_object* l___private_Lean_Elab_Binders_16__expandMatchAltsIntoMatchAux(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_quoteAutoTactic___main___closed__12; lean_object* l___private_Lean_Elab_Binders_2__expandBinderIdent(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -16908,7 +16909,7 @@ lean_ctor_set(x_121, 0, x_120); lean_ctor_set(x_121, 1, x_119); x_122 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_123 = lean_array_push(x_122, x_121); -x_124 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_124 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_125 = lean_array_push(x_123, x_124); x_126 = l___private_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__7; x_127 = lean_array_push(x_126, x_102); diff --git a/stage0/stdlib/Lean/Elab/BuiltinNotation.c b/stage0/stdlib/Lean/Elab/BuiltinNotation.c index 703624459c..0f78f968cc 100644 --- a/stage0/stdlib/Lean/Elab/BuiltinNotation.c +++ b/stage0/stdlib/Lean/Elab/BuiltinNotation.c @@ -24,6 +24,7 @@ lean_object* l_Lean_mkCIdentFrom(lean_object*, lean_object*); lean_object* l___private_Lean_Elab_BuiltinNotation_1__elabParserMacroAux___closed__25; lean_object* l_Lean_Elab_Term_expandNot___closed__1; lean_object* l_Lean_Elab_Term_expandUnreachable___rarg___closed__6; +extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; lean_object* l___regBuiltin_Lean_Elab_Term_elabParserMacro(lean_object*); lean_object* l___private_Lean_Elab_BuiltinNotation_1__elabParserMacroAux___closed__22; lean_object* l_Lean_mkAppStx(lean_object*, lean_object*); @@ -3037,7 +3038,7 @@ lean_ctor_set(x_63, 0, x_62); lean_ctor_set(x_63, 1, x_61); x_64 = l_Lean_Elab_Term_expandShow___closed__16; x_65 = lean_array_push(x_64, x_63); -x_66 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_66 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_67 = lean_array_push(x_65, x_66); x_68 = lean_array_push(x_67, x_43); x_69 = l_Lean_Elab_Term_elabLetDeclCore___closed__8; @@ -3153,30 +3154,30 @@ return x_3; lean_object* l_Lean_Elab_Term_expandHave(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { -uint8_t x_4; lean_object* x_271; uint8_t x_272; -x_271 = l_Lean_Elab_Term_expandHave___closed__2; +uint8_t x_4; lean_object* x_340; uint8_t x_341; +x_340 = l_Lean_Elab_Term_expandHave___closed__2; lean_inc(x_1); -x_272 = l_Lean_Syntax_isOfKind(x_1, x_271); -if (x_272 == 0) +x_341 = l_Lean_Syntax_isOfKind(x_1, x_340); +if (x_341 == 0) { -uint8_t x_273; -x_273 = 0; -x_4 = x_273; -goto block_270; +uint8_t x_342; +x_342 = 0; +x_4 = x_342; +goto block_339; } else { -lean_object* x_274; lean_object* x_275; lean_object* x_276; uint8_t x_277; -x_274 = l_Lean_Syntax_getArgs(x_1); -x_275 = lean_array_get_size(x_274); -lean_dec(x_274); -x_276 = lean_unsigned_to_nat(6u); -x_277 = lean_nat_dec_eq(x_275, x_276); -lean_dec(x_275); -x_4 = x_277; -goto block_270; +lean_object* x_343; lean_object* x_344; lean_object* x_345; uint8_t x_346; +x_343 = l_Lean_Syntax_getArgs(x_1); +x_344 = lean_array_get_size(x_343); +lean_dec(x_343); +x_345 = lean_unsigned_to_nat(6u); +x_346 = lean_nat_dec_eq(x_344, x_345); +lean_dec(x_344); +x_4 = x_346; +goto block_339; } -block_270: +block_339: { if (x_4 == 0) { @@ -3190,32 +3191,32 @@ return x_6; } else { -lean_object* x_7; lean_object* x_8; uint8_t x_9; lean_object* x_138; uint8_t x_139; uint8_t x_140; +lean_object* x_7; lean_object* x_8; uint8_t x_9; lean_object* x_174; uint8_t x_175; uint8_t x_176; x_7 = lean_unsigned_to_nat(1u); x_8 = l_Lean_Syntax_getArg(x_1, x_7); -x_138 = l_Lean_nullKind___closed__2; +x_174 = l_Lean_nullKind___closed__2; lean_inc(x_8); -x_139 = l_Lean_Syntax_isOfKind(x_8, x_138); -if (x_139 == 0) +x_175 = l_Lean_Syntax_isOfKind(x_8, x_174); +if (x_175 == 0) { -uint8_t x_265; -x_265 = 0; -x_140 = x_265; -goto block_264; +uint8_t x_334; +x_334 = 0; +x_176 = x_334; +goto block_333; } else { -lean_object* x_266; lean_object* x_267; lean_object* x_268; uint8_t x_269; -x_266 = l_Lean_Syntax_getArgs(x_8); -x_267 = lean_array_get_size(x_266); -lean_dec(x_266); -x_268 = lean_unsigned_to_nat(0u); -x_269 = lean_nat_dec_eq(x_267, x_268); -lean_dec(x_267); -x_140 = x_269; -goto block_264; +lean_object* x_335; lean_object* x_336; lean_object* x_337; uint8_t x_338; +x_335 = l_Lean_Syntax_getArgs(x_8); +x_336 = lean_array_get_size(x_335); +lean_dec(x_335); +x_337 = lean_unsigned_to_nat(0u); +x_338 = lean_nat_dec_eq(x_336, x_337); +lean_dec(x_336); +x_176 = x_338; +goto block_333; } -block_137: +block_173: { if (x_9 == 0) { @@ -3230,7 +3231,7 @@ return x_11; } else { -lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; uint8_t x_53; lean_object* x_131; uint8_t x_132; +lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; uint8_t x_65; lean_object* x_167; uint8_t x_168; x_12 = lean_unsigned_to_nat(0u); x_13 = l_Lean_Syntax_getArg(x_8, x_12); lean_dec(x_8); @@ -3238,28 +3239,28 @@ x_14 = lean_unsigned_to_nat(2u); x_15 = l_Lean_Syntax_getArg(x_1, x_14); x_16 = lean_unsigned_to_nat(3u); x_17 = l_Lean_Syntax_getArg(x_1, x_16); -x_131 = l_Lean_Elab_Term_expandShow___closed__4; +x_167 = l_Lean_Elab_Term_expandShow___closed__4; lean_inc(x_17); -x_132 = l_Lean_Syntax_isOfKind(x_17, x_131); -if (x_132 == 0) +x_168 = l_Lean_Syntax_isOfKind(x_17, x_167); +if (x_168 == 0) { -uint8_t x_133; -x_133 = 0; -x_53 = x_133; -goto block_130; +uint8_t x_169; +x_169 = 0; +x_65 = x_169; +goto block_166; } else { -lean_object* x_134; lean_object* x_135; uint8_t x_136; -x_134 = l_Lean_Syntax_getArgs(x_17); -x_135 = lean_array_get_size(x_134); -lean_dec(x_134); -x_136 = lean_nat_dec_eq(x_135, x_14); -lean_dec(x_135); -x_53 = x_136; -goto block_130; +lean_object* x_170; lean_object* x_171; uint8_t x_172; +x_170 = l_Lean_Syntax_getArgs(x_17); +x_171 = lean_array_get_size(x_170); +lean_dec(x_170); +x_172 = lean_nat_dec_eq(x_171, x_14); +lean_dec(x_171); +x_65 = x_172; +goto block_166; } -block_52: +block_64: { if (x_18 == 0) { @@ -3276,505 +3277,769 @@ return x_20; } else { -lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; +lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24; lean_object* x_58; uint8_t x_59; x_21 = l_Lean_Syntax_getArg(x_17, x_7); lean_dec(x_17); -x_22 = lean_unsigned_to_nat(5u); +x_22 = lean_unsigned_to_nat(4u); x_23 = l_Lean_Syntax_getArg(x_1, x_22); -lean_dec(x_1); -x_24 = l_Array_empty___closed__1; -x_25 = lean_array_push(x_24, x_13); -x_26 = l___private_Lean_Elab_Quotation_8__letBindRhss___main___closed__13; -x_27 = lean_array_push(x_25, x_26); -x_28 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__26; -x_29 = lean_array_push(x_28, x_15); -x_30 = l_Lean_Elab_Term_elabLetDeclCore___closed__6; -x_31 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_31, 0, x_30); -lean_ctor_set(x_31, 1, x_29); -x_32 = lean_array_push(x_24, x_31); -x_33 = l_Lean_nullKind___closed__2; -x_34 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_34, 0, x_33); -lean_ctor_set(x_34, 1, x_32); -x_35 = lean_array_push(x_27, x_34); -x_36 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__10; -x_37 = lean_array_push(x_35, x_36); -x_38 = lean_array_push(x_37, x_21); -x_39 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__8; -x_40 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_40, 0, x_39); -lean_ctor_set(x_40, 1, x_38); -x_41 = lean_array_push(x_24, x_40); -x_42 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__6; -x_43 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_43, 0, x_42); -lean_ctor_set(x_43, 1, x_41); -x_44 = l_Lean_Elab_Term_expandShow___closed__16; -x_45 = lean_array_push(x_44, x_43); -x_46 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; -x_47 = lean_array_push(x_45, x_46); -x_48 = lean_array_push(x_47, x_23); -x_49 = l_Lean_Elab_Term_elabLetDeclCore___closed__8; -x_50 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_50, 0, x_49); -lean_ctor_set(x_50, 1, x_48); -x_51 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_51, 0, x_50); -lean_ctor_set(x_51, 1, x_3); -return x_51; -} -} -block_130: +x_58 = l_Lean_nullKind___closed__2; +lean_inc(x_23); +x_59 = l_Lean_Syntax_isOfKind(x_23, x_58); +if (x_59 == 0) { -if (x_53 == 0) -{ -uint8_t x_54; lean_object* x_93; uint8_t x_94; -x_93 = l___regBuiltin_Lean_Elab_Term_elabByTactic___closed__2; -lean_inc(x_17); -x_94 = l_Lean_Syntax_isOfKind(x_17, x_93); -if (x_94 == 0) -{ -uint8_t x_95; -x_95 = 0; -x_54 = x_95; -goto block_92; -} -else -{ -lean_object* x_96; lean_object* x_97; uint8_t x_98; -x_96 = l_Lean_Syntax_getArgs(x_17); -x_97 = lean_array_get_size(x_96); -lean_dec(x_96); -x_98 = lean_nat_dec_eq(x_97, x_14); -lean_dec(x_97); -x_54 = x_98; -goto block_92; -} -block_92: -{ -if (x_54 == 0) -{ -lean_object* x_55; uint8_t x_56; -x_55 = l_Lean_Elab_Term_expandHave___closed__4; -lean_inc(x_17); -x_56 = l_Lean_Syntax_isOfKind(x_17, x_55); -if (x_56 == 0) -{ -uint8_t x_57; -x_57 = 0; -x_18 = x_57; -goto block_52; -} -else -{ -lean_object* x_58; lean_object* x_59; uint8_t x_60; -x_58 = l_Lean_Syntax_getArgs(x_17); -x_59 = lean_array_get_size(x_58); -lean_dec(x_58); -x_60 = lean_nat_dec_eq(x_59, x_14); -lean_dec(x_59); -x_18 = x_60; -goto block_52; -} +uint8_t x_60; +lean_dec(x_23); +x_60 = 0; +x_24 = x_60; +goto block_57; } else { lean_object* x_61; lean_object* x_62; uint8_t x_63; -x_61 = l_Lean_Syntax_getArg(x_17, x_7); -lean_dec(x_17); -x_62 = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__2; -lean_inc(x_61); -x_63 = l_Lean_Syntax_isOfKind(x_61, x_62); -if (x_63 == 0) -{ -lean_object* x_64; lean_object* x_65; +x_61 = l_Lean_Syntax_getArgs(x_23); +lean_dec(x_23); +x_62 = lean_array_get_size(x_61); lean_dec(x_61); +x_63 = lean_nat_dec_eq(x_62, x_7); +lean_dec(x_62); +x_24 = x_63; +goto block_57; +} +block_57: +{ +if (x_24 == 0) +{ +lean_object* x_25; lean_object* x_26; +lean_dec(x_21); lean_dec(x_15); lean_dec(x_13); lean_dec(x_1); -x_64 = lean_box(1); -x_65 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_65, 0, x_64); -lean_ctor_set(x_65, 1, x_3); -return x_65; +x_25 = lean_box(1); +x_26 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_26, 0, x_25); +lean_ctor_set(x_26, 1, x_3); +return x_26; } else { -lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; -x_66 = lean_unsigned_to_nat(5u); -x_67 = l_Lean_Syntax_getArg(x_1, x_66); +lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; +x_27 = lean_unsigned_to_nat(5u); +x_28 = l_Lean_Syntax_getArg(x_1, x_27); lean_dec(x_1); -x_68 = l_Array_empty___closed__1; -x_69 = lean_array_push(x_68, x_13); -x_70 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__25; -x_71 = lean_array_push(x_69, x_70); -x_72 = l_Lean_nullKind___closed__2; -x_73 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_73, 0, x_72); -lean_ctor_set(x_73, 1, x_71); -x_74 = l_Lean_Elab_Term_expandHave___closed__6; -x_75 = lean_array_push(x_74, x_73); -x_76 = lean_array_push(x_75, x_15); -x_77 = l_Lean_Elab_Term_expandShow___closed__12; -x_78 = lean_array_push(x_77, x_61); -x_79 = l___regBuiltin_Lean_Elab_Term_elabByTactic___closed__2; -x_80 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_80, 0, x_79); -lean_ctor_set(x_80, 1, x_78); -x_81 = l_Lean_Elab_Term_expandShow___closed__9; -x_82 = lean_array_push(x_81, x_80); -x_83 = l_Lean_Elab_Term_expandShow___closed__4; -x_84 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_84, 0, x_83); -lean_ctor_set(x_84, 1, x_82); -x_85 = lean_array_push(x_76, x_84); -x_86 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; -x_87 = lean_array_push(x_85, x_86); -x_88 = lean_array_push(x_87, x_67); -x_89 = l_Lean_Elab_Term_expandHave___closed__2; +x_29 = l_Array_empty___closed__1; +x_30 = lean_array_push(x_29, x_13); +x_31 = l___private_Lean_Elab_Quotation_8__letBindRhss___main___closed__13; +x_32 = lean_array_push(x_30, x_31); +x_33 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__26; +x_34 = lean_array_push(x_33, x_15); +x_35 = l_Lean_Elab_Term_elabLetDeclCore___closed__6; +x_36 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_36, 0, x_35); +lean_ctor_set(x_36, 1, x_34); +x_37 = lean_array_push(x_29, x_36); +x_38 = l_Lean_nullKind___closed__2; +x_39 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_39, 0, x_38); +lean_ctor_set(x_39, 1, x_37); +x_40 = lean_array_push(x_32, x_39); +x_41 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__10; +x_42 = lean_array_push(x_40, x_41); +x_43 = lean_array_push(x_42, x_21); +x_44 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__8; +x_45 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_45, 0, x_44); +lean_ctor_set(x_45, 1, x_43); +x_46 = lean_array_push(x_29, x_45); +x_47 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__6; +x_48 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_48, 0, x_47); +lean_ctor_set(x_48, 1, x_46); +x_49 = l_Lean_Elab_Term_expandShow___closed__16; +x_50 = lean_array_push(x_49, x_48); +x_51 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; +x_52 = lean_array_push(x_50, x_51); +x_53 = lean_array_push(x_52, x_28); +x_54 = l_Lean_Elab_Term_elabLetDeclCore___closed__8; +x_55 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_55, 0, x_54); +lean_ctor_set(x_55, 1, x_53); +x_56 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_56, 0, x_55); +lean_ctor_set(x_56, 1, x_3); +return x_56; +} +} +} +} +block_166: +{ +if (x_65 == 0) +{ +uint8_t x_66; lean_object* x_117; uint8_t x_118; +x_117 = l___regBuiltin_Lean_Elab_Term_elabByTactic___closed__2; +lean_inc(x_17); +x_118 = l_Lean_Syntax_isOfKind(x_17, x_117); +if (x_118 == 0) +{ +uint8_t x_119; +x_119 = 0; +x_66 = x_119; +goto block_116; +} +else +{ +lean_object* x_120; lean_object* x_121; uint8_t x_122; +x_120 = l_Lean_Syntax_getArgs(x_17); +x_121 = lean_array_get_size(x_120); +lean_dec(x_120); +x_122 = lean_nat_dec_eq(x_121, x_14); +lean_dec(x_121); +x_66 = x_122; +goto block_116; +} +block_116: +{ +if (x_66 == 0) +{ +lean_object* x_67; uint8_t x_68; +x_67 = l_Lean_Elab_Term_expandHave___closed__4; +lean_inc(x_17); +x_68 = l_Lean_Syntax_isOfKind(x_17, x_67); +if (x_68 == 0) +{ +uint8_t x_69; +x_69 = 0; +x_18 = x_69; +goto block_64; +} +else +{ +lean_object* x_70; lean_object* x_71; uint8_t x_72; +x_70 = l_Lean_Syntax_getArgs(x_17); +x_71 = lean_array_get_size(x_70); +lean_dec(x_70); +x_72 = lean_nat_dec_eq(x_71, x_14); +lean_dec(x_71); +x_18 = x_72; +goto block_64; +} +} +else +{ +lean_object* x_73; lean_object* x_74; uint8_t x_75; +x_73 = l_Lean_Syntax_getArg(x_17, x_7); +lean_dec(x_17); +x_74 = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__2; +lean_inc(x_73); +x_75 = l_Lean_Syntax_isOfKind(x_73, x_74); +if (x_75 == 0) +{ +lean_object* x_76; lean_object* x_77; +lean_dec(x_73); +lean_dec(x_15); +lean_dec(x_13); +lean_dec(x_1); +x_76 = lean_box(1); +x_77 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_77, 0, x_76); +lean_ctor_set(x_77, 1, x_3); +return x_77; +} +else +{ +lean_object* x_78; lean_object* x_79; uint8_t x_80; lean_object* x_110; uint8_t x_111; +x_78 = lean_unsigned_to_nat(4u); +x_79 = l_Lean_Syntax_getArg(x_1, x_78); +x_110 = l_Lean_nullKind___closed__2; +lean_inc(x_79); +x_111 = l_Lean_Syntax_isOfKind(x_79, x_110); +if (x_111 == 0) +{ +uint8_t x_112; +lean_dec(x_79); +x_112 = 0; +x_80 = x_112; +goto block_109; +} +else +{ +lean_object* x_113; lean_object* x_114; uint8_t x_115; +x_113 = l_Lean_Syntax_getArgs(x_79); +lean_dec(x_79); +x_114 = lean_array_get_size(x_113); +lean_dec(x_113); +x_115 = lean_nat_dec_eq(x_114, x_7); +lean_dec(x_114); +x_80 = x_115; +goto block_109; +} +block_109: +{ +if (x_80 == 0) +{ +lean_object* x_81; lean_object* x_82; +lean_dec(x_73); +lean_dec(x_15); +lean_dec(x_13); +lean_dec(x_1); +x_81 = lean_box(1); +x_82 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_82, 0, x_81); +lean_ctor_set(x_82, 1, x_3); +return x_82; +} +else +{ +lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; +x_83 = lean_unsigned_to_nat(5u); +x_84 = l_Lean_Syntax_getArg(x_1, x_83); +lean_dec(x_1); +x_85 = l_Array_empty___closed__1; +x_86 = lean_array_push(x_85, x_13); +x_87 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__25; +x_88 = lean_array_push(x_86, x_87); +x_89 = l_Lean_nullKind___closed__2; x_90 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_90, 0, x_89); lean_ctor_set(x_90, 1, x_88); -x_91 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_91, 0, x_90); -lean_ctor_set(x_91, 1, x_3); -return x_91; +x_91 = l_Lean_Elab_Term_expandHave___closed__6; +x_92 = lean_array_push(x_91, x_90); +x_93 = lean_array_push(x_92, x_15); +x_94 = l_Lean_Elab_Term_expandShow___closed__12; +x_95 = lean_array_push(x_94, x_73); +x_96 = l___regBuiltin_Lean_Elab_Term_elabByTactic___closed__2; +x_97 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_97, 0, x_96); +lean_ctor_set(x_97, 1, x_95); +x_98 = l_Lean_Elab_Term_expandShow___closed__9; +x_99 = lean_array_push(x_98, x_97); +x_100 = l_Lean_Elab_Term_expandShow___closed__4; +x_101 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_101, 0, x_100); +lean_ctor_set(x_101, 1, x_99); +x_102 = lean_array_push(x_93, x_101); +x_103 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; +x_104 = lean_array_push(x_102, x_103); +x_105 = lean_array_push(x_104, x_84); +x_106 = l_Lean_Elab_Term_expandHave___closed__2; +x_107 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_107, 0, x_106); +lean_ctor_set(x_107, 1, x_105); +x_108 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_108, 0, x_107); +lean_ctor_set(x_108, 1, x_3); +return x_108; +} +} } } } } else { -lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; -x_99 = l_Lean_Syntax_getArg(x_17, x_7); +lean_object* x_123; lean_object* x_124; lean_object* x_125; uint8_t x_126; lean_object* x_160; uint8_t x_161; +x_123 = l_Lean_Syntax_getArg(x_17, x_7); lean_dec(x_17); -x_100 = lean_unsigned_to_nat(5u); -x_101 = l_Lean_Syntax_getArg(x_1, x_100); +x_124 = lean_unsigned_to_nat(4u); +x_125 = l_Lean_Syntax_getArg(x_1, x_124); +x_160 = l_Lean_nullKind___closed__2; +lean_inc(x_125); +x_161 = l_Lean_Syntax_isOfKind(x_125, x_160); +if (x_161 == 0) +{ +uint8_t x_162; +lean_dec(x_125); +x_162 = 0; +x_126 = x_162; +goto block_159; +} +else +{ +lean_object* x_163; lean_object* x_164; uint8_t x_165; +x_163 = l_Lean_Syntax_getArgs(x_125); +lean_dec(x_125); +x_164 = lean_array_get_size(x_163); +lean_dec(x_163); +x_165 = lean_nat_dec_eq(x_164, x_7); +lean_dec(x_164); +x_126 = x_165; +goto block_159; +} +block_159: +{ +if (x_126 == 0) +{ +lean_object* x_127; lean_object* x_128; +lean_dec(x_123); +lean_dec(x_15); +lean_dec(x_13); lean_dec(x_1); -x_102 = l_Array_empty___closed__1; -x_103 = lean_array_push(x_102, x_13); -x_104 = l___private_Lean_Elab_Quotation_8__letBindRhss___main___closed__13; -x_105 = lean_array_push(x_103, x_104); -x_106 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__26; -x_107 = lean_array_push(x_106, x_15); -x_108 = l_Lean_Elab_Term_elabLetDeclCore___closed__6; -x_109 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_109, 0, x_108); -lean_ctor_set(x_109, 1, x_107); -x_110 = lean_array_push(x_102, x_109); -x_111 = l_Lean_nullKind___closed__2; -x_112 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_112, 0, x_111); -lean_ctor_set(x_112, 1, x_110); -x_113 = lean_array_push(x_105, x_112); -x_114 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__10; -x_115 = lean_array_push(x_113, x_114); -x_116 = lean_array_push(x_115, x_99); -x_117 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__8; -x_118 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_118, 0, x_117); -lean_ctor_set(x_118, 1, x_116); -x_119 = lean_array_push(x_102, x_118); -x_120 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__6; -x_121 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_121, 0, x_120); -lean_ctor_set(x_121, 1, x_119); -x_122 = l_Lean_Elab_Term_expandShow___closed__16; -x_123 = lean_array_push(x_122, x_121); -x_124 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; -x_125 = lean_array_push(x_123, x_124); -x_126 = lean_array_push(x_125, x_101); -x_127 = l_Lean_Elab_Term_elabLetDeclCore___closed__8; +x_127 = lean_box(1); x_128 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_128, 0, x_127); -lean_ctor_set(x_128, 1, x_126); -x_129 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_129, 0, x_128); -lean_ctor_set(x_129, 1, x_3); -return x_129; -} -} -} -} -block_264: -{ -if (x_140 == 0) -{ -if (x_139 == 0) -{ -uint8_t x_141; -x_141 = 0; -x_9 = x_141; -goto block_137; +lean_ctor_set(x_128, 1, x_3); +return x_128; } else { -lean_object* x_142; lean_object* x_143; lean_object* x_144; uint8_t x_145; -x_142 = l_Lean_Syntax_getArgs(x_8); -x_143 = lean_array_get_size(x_142); -lean_dec(x_142); -x_144 = lean_unsigned_to_nat(2u); -x_145 = lean_nat_dec_eq(x_143, x_144); -lean_dec(x_143); -x_9 = x_145; -goto block_137; +lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; +x_129 = lean_unsigned_to_nat(5u); +x_130 = l_Lean_Syntax_getArg(x_1, x_129); +lean_dec(x_1); +x_131 = l_Array_empty___closed__1; +x_132 = lean_array_push(x_131, x_13); +x_133 = l___private_Lean_Elab_Quotation_8__letBindRhss___main___closed__13; +x_134 = lean_array_push(x_132, x_133); +x_135 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__26; +x_136 = lean_array_push(x_135, x_15); +x_137 = l_Lean_Elab_Term_elabLetDeclCore___closed__6; +x_138 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_138, 0, x_137); +lean_ctor_set(x_138, 1, x_136); +x_139 = lean_array_push(x_131, x_138); +x_140 = l_Lean_nullKind___closed__2; +x_141 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_141, 0, x_140); +lean_ctor_set(x_141, 1, x_139); +x_142 = lean_array_push(x_134, x_141); +x_143 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__10; +x_144 = lean_array_push(x_142, x_143); +x_145 = lean_array_push(x_144, x_123); +x_146 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__8; +x_147 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_147, 0, x_146); +lean_ctor_set(x_147, 1, x_145); +x_148 = lean_array_push(x_131, x_147); +x_149 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__6; +x_150 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_150, 0, x_149); +lean_ctor_set(x_150, 1, x_148); +x_151 = l_Lean_Elab_Term_expandShow___closed__16; +x_152 = lean_array_push(x_151, x_150); +x_153 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; +x_154 = lean_array_push(x_152, x_153); +x_155 = lean_array_push(x_154, x_130); +x_156 = l_Lean_Elab_Term_elabLetDeclCore___closed__8; +x_157 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_157, 0, x_156); +lean_ctor_set(x_157, 1, x_155); +x_158 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_158, 0, x_157); +lean_ctor_set(x_158, 1, x_3); +return x_158; +} +} +} +} +} +} +block_333: +{ +if (x_176 == 0) +{ +if (x_175 == 0) +{ +uint8_t x_177; +x_177 = 0; +x_9 = x_177; +goto block_173; +} +else +{ +lean_object* x_178; lean_object* x_179; lean_object* x_180; uint8_t x_181; +x_178 = l_Lean_Syntax_getArgs(x_8); +x_179 = lean_array_get_size(x_178); +lean_dec(x_178); +x_180 = lean_unsigned_to_nat(2u); +x_181 = lean_nat_dec_eq(x_179, x_180); +lean_dec(x_179); +x_9 = x_181; +goto block_173; } } else { -lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; uint8_t x_150; uint8_t x_186; lean_object* x_258; uint8_t x_259; +lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; uint8_t x_186; uint8_t x_233; lean_object* x_327; uint8_t x_328; lean_dec(x_8); -x_146 = lean_unsigned_to_nat(2u); -x_147 = l_Lean_Syntax_getArg(x_1, x_146); -x_148 = lean_unsigned_to_nat(3u); -x_149 = l_Lean_Syntax_getArg(x_1, x_148); -x_258 = l_Lean_Elab_Term_expandShow___closed__4; -lean_inc(x_149); -x_259 = l_Lean_Syntax_isOfKind(x_149, x_258); -if (x_259 == 0) +x_182 = lean_unsigned_to_nat(2u); +x_183 = l_Lean_Syntax_getArg(x_1, x_182); +x_184 = lean_unsigned_to_nat(3u); +x_185 = l_Lean_Syntax_getArg(x_1, x_184); +x_327 = l_Lean_Elab_Term_expandShow___closed__4; +lean_inc(x_185); +x_328 = l_Lean_Syntax_isOfKind(x_185, x_327); +if (x_328 == 0) { -uint8_t x_260; -x_260 = 0; -x_186 = x_260; -goto block_257; +uint8_t x_329; +x_329 = 0; +x_233 = x_329; +goto block_326; } else { -lean_object* x_261; lean_object* x_262; uint8_t x_263; -x_261 = l_Lean_Syntax_getArgs(x_149); -x_262 = lean_array_get_size(x_261); -lean_dec(x_261); -x_263 = lean_nat_dec_eq(x_262, x_146); -lean_dec(x_262); -x_186 = x_263; -goto block_257; +lean_object* x_330; lean_object* x_331; uint8_t x_332; +x_330 = l_Lean_Syntax_getArgs(x_185); +x_331 = lean_array_get_size(x_330); +lean_dec(x_330); +x_332 = lean_nat_dec_eq(x_331, x_182); +lean_dec(x_331); +x_233 = x_332; +goto block_326; } -block_185: -{ -if (x_150 == 0) -{ -lean_object* x_151; lean_object* x_152; -lean_dec(x_149); -lean_dec(x_147); -lean_dec(x_1); -x_151 = lean_box(1); -x_152 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_152, 0, x_151); -lean_ctor_set(x_152, 1, x_3); -return x_152; -} -else -{ -lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172; lean_object* x_173; lean_object* x_174; lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; -x_153 = l_Lean_Syntax_getArg(x_149, x_7); -lean_dec(x_149); -x_154 = lean_unsigned_to_nat(5u); -x_155 = l_Lean_Syntax_getArg(x_1, x_154); -x_156 = l_Lean_Elab_Term_expandShow___closed__14; -x_157 = l_Lean_mkIdentFrom(x_1, x_156); -lean_dec(x_1); -x_158 = l_Array_empty___closed__1; -x_159 = lean_array_push(x_158, x_157); -x_160 = l___private_Lean_Elab_Quotation_8__letBindRhss___main___closed__13; -x_161 = lean_array_push(x_159, x_160); -x_162 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__26; -x_163 = lean_array_push(x_162, x_147); -x_164 = l_Lean_Elab_Term_elabLetDeclCore___closed__6; -x_165 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_165, 0, x_164); -lean_ctor_set(x_165, 1, x_163); -x_166 = lean_array_push(x_158, x_165); -x_167 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_167, 0, x_138); -lean_ctor_set(x_167, 1, x_166); -x_168 = lean_array_push(x_161, x_167); -x_169 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__10; -x_170 = lean_array_push(x_168, x_169); -x_171 = lean_array_push(x_170, x_153); -x_172 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__8; -x_173 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_173, 0, x_172); -lean_ctor_set(x_173, 1, x_171); -x_174 = lean_array_push(x_158, x_173); -x_175 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__6; -x_176 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_176, 0, x_175); -lean_ctor_set(x_176, 1, x_174); -x_177 = l_Lean_Elab_Term_expandShow___closed__16; -x_178 = lean_array_push(x_177, x_176); -x_179 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; -x_180 = lean_array_push(x_178, x_179); -x_181 = lean_array_push(x_180, x_155); -x_182 = l_Lean_Elab_Term_elabLetDeclCore___closed__8; -x_183 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_183, 0, x_182); -lean_ctor_set(x_183, 1, x_181); -x_184 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_184, 0, x_183); -lean_ctor_set(x_184, 1, x_3); -return x_184; -} -} -block_257: +block_232: { if (x_186 == 0) { -uint8_t x_187; lean_object* x_219; uint8_t x_220; -x_219 = l___regBuiltin_Lean_Elab_Term_elabByTactic___closed__2; -lean_inc(x_149); -x_220 = l_Lean_Syntax_isOfKind(x_149, x_219); -if (x_220 == 0) -{ -uint8_t x_221; -x_221 = 0; -x_187 = x_221; -goto block_218; +lean_object* x_187; lean_object* x_188; +lean_dec(x_185); +lean_dec(x_183); +lean_dec(x_1); +x_187 = lean_box(1); +x_188 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_188, 0, x_187); +lean_ctor_set(x_188, 1, x_3); +return x_188; } else { -lean_object* x_222; lean_object* x_223; uint8_t x_224; -x_222 = l_Lean_Syntax_getArgs(x_149); -x_223 = lean_array_get_size(x_222); -lean_dec(x_222); -x_224 = lean_nat_dec_eq(x_223, x_146); -lean_dec(x_223); -x_187 = x_224; -goto block_218; -} -block_218: +lean_object* x_189; lean_object* x_190; lean_object* x_191; uint8_t x_192; uint8_t x_227; +x_189 = l_Lean_Syntax_getArg(x_185, x_7); +lean_dec(x_185); +x_190 = lean_unsigned_to_nat(4u); +x_191 = l_Lean_Syntax_getArg(x_1, x_190); +lean_inc(x_191); +x_227 = l_Lean_Syntax_isOfKind(x_191, x_174); +if (x_227 == 0) { -if (x_187 == 0) -{ -lean_object* x_188; uint8_t x_189; -x_188 = l_Lean_Elab_Term_expandHave___closed__4; -lean_inc(x_149); -x_189 = l_Lean_Syntax_isOfKind(x_149, x_188); -if (x_189 == 0) -{ -uint8_t x_190; -x_190 = 0; -x_150 = x_190; -goto block_185; -} -else -{ -lean_object* x_191; lean_object* x_192; uint8_t x_193; -x_191 = l_Lean_Syntax_getArgs(x_149); -x_192 = lean_array_get_size(x_191); +uint8_t x_228; lean_dec(x_191); -x_193 = lean_nat_dec_eq(x_192, x_146); -lean_dec(x_192); -x_150 = x_193; -goto block_185; -} +x_228 = 0; +x_192 = x_228; +goto block_226; } else { -lean_object* x_194; lean_object* x_195; uint8_t x_196; -x_194 = l_Lean_Syntax_getArg(x_149, x_7); -lean_dec(x_149); -x_195 = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__2; -lean_inc(x_194); -x_196 = l_Lean_Syntax_isOfKind(x_194, x_195); -if (x_196 == 0) +lean_object* x_229; lean_object* x_230; uint8_t x_231; +x_229 = l_Lean_Syntax_getArgs(x_191); +lean_dec(x_191); +x_230 = lean_array_get_size(x_229); +lean_dec(x_229); +x_231 = lean_nat_dec_eq(x_230, x_7); +lean_dec(x_230); +x_192 = x_231; +goto block_226; +} +block_226: { -lean_object* x_197; lean_object* x_198; -lean_dec(x_194); -lean_dec(x_147); +if (x_192 == 0) +{ +lean_object* x_193; lean_object* x_194; +lean_dec(x_189); +lean_dec(x_183); lean_dec(x_1); -x_197 = lean_box(1); -x_198 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_198, 0, x_197); -lean_ctor_set(x_198, 1, x_3); -return x_198; +x_193 = lean_box(1); +x_194 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_194, 0, x_193); +lean_ctor_set(x_194, 1, x_3); +return x_194; } else { -lean_object* x_199; lean_object* x_200; lean_object* x_201; lean_object* x_202; lean_object* x_203; lean_object* x_204; lean_object* x_205; lean_object* x_206; lean_object* x_207; lean_object* x_208; lean_object* x_209; lean_object* x_210; lean_object* x_211; lean_object* x_212; lean_object* x_213; lean_object* x_214; lean_object* x_215; lean_object* x_216; lean_object* x_217; -x_199 = lean_unsigned_to_nat(5u); -x_200 = l_Lean_Syntax_getArg(x_1, x_199); +lean_object* x_195; lean_object* x_196; lean_object* x_197; lean_object* x_198; lean_object* x_199; lean_object* x_200; lean_object* x_201; lean_object* x_202; lean_object* x_203; lean_object* x_204; lean_object* x_205; lean_object* x_206; lean_object* x_207; lean_object* x_208; lean_object* x_209; lean_object* x_210; lean_object* x_211; lean_object* x_212; lean_object* x_213; lean_object* x_214; lean_object* x_215; lean_object* x_216; lean_object* x_217; lean_object* x_218; lean_object* x_219; lean_object* x_220; lean_object* x_221; lean_object* x_222; lean_object* x_223; lean_object* x_224; lean_object* x_225; +x_195 = lean_unsigned_to_nat(5u); +x_196 = l_Lean_Syntax_getArg(x_1, x_195); +x_197 = l_Lean_Elab_Term_expandShow___closed__14; +x_198 = l_Lean_mkIdentFrom(x_1, x_197); lean_dec(x_1); -x_201 = l_Lean_Elab_Term_expandHave___closed__7; -x_202 = lean_array_push(x_201, x_147); -x_203 = l_Lean_Elab_Term_expandShow___closed__12; -x_204 = lean_array_push(x_203, x_194); -x_205 = l___regBuiltin_Lean_Elab_Term_elabByTactic___closed__2; +x_199 = l_Array_empty___closed__1; +x_200 = lean_array_push(x_199, x_198); +x_201 = l___private_Lean_Elab_Quotation_8__letBindRhss___main___closed__13; +x_202 = lean_array_push(x_200, x_201); +x_203 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__26; +x_204 = lean_array_push(x_203, x_183); +x_205 = l_Lean_Elab_Term_elabLetDeclCore___closed__6; x_206 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_206, 0, x_205); lean_ctor_set(x_206, 1, x_204); -x_207 = l_Lean_Elab_Term_expandShow___closed__9; -x_208 = lean_array_push(x_207, x_206); -x_209 = l_Lean_Elab_Term_expandShow___closed__4; -x_210 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_210, 0, x_209); -lean_ctor_set(x_210, 1, x_208); -x_211 = lean_array_push(x_202, x_210); -x_212 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; -x_213 = lean_array_push(x_211, x_212); -x_214 = lean_array_push(x_213, x_200); -x_215 = l_Lean_Elab_Term_expandHave___closed__2; -x_216 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_216, 0, x_215); -lean_ctor_set(x_216, 1, x_214); -x_217 = lean_alloc_ctor(0, 2, 0); +x_207 = lean_array_push(x_199, x_206); +x_208 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_208, 0, x_174); +lean_ctor_set(x_208, 1, x_207); +x_209 = lean_array_push(x_202, x_208); +x_210 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__10; +x_211 = lean_array_push(x_209, x_210); +x_212 = lean_array_push(x_211, x_189); +x_213 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__8; +x_214 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_214, 0, x_213); +lean_ctor_set(x_214, 1, x_212); +x_215 = lean_array_push(x_199, x_214); +x_216 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__6; +x_217 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_217, 0, x_216); -lean_ctor_set(x_217, 1, x_3); -return x_217; +lean_ctor_set(x_217, 1, x_215); +x_218 = l_Lean_Elab_Term_expandShow___closed__16; +x_219 = lean_array_push(x_218, x_217); +x_220 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; +x_221 = lean_array_push(x_219, x_220); +x_222 = lean_array_push(x_221, x_196); +x_223 = l_Lean_Elab_Term_elabLetDeclCore___closed__8; +x_224 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_224, 0, x_223); +lean_ctor_set(x_224, 1, x_222); +x_225 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_225, 0, x_224); +lean_ctor_set(x_225, 1, x_3); +return x_225; +} +} +} +} +block_326: +{ +if (x_233 == 0) +{ +uint8_t x_234; lean_object* x_277; uint8_t x_278; +x_277 = l___regBuiltin_Lean_Elab_Term_elabByTactic___closed__2; +lean_inc(x_185); +x_278 = l_Lean_Syntax_isOfKind(x_185, x_277); +if (x_278 == 0) +{ +uint8_t x_279; +x_279 = 0; +x_234 = x_279; +goto block_276; +} +else +{ +lean_object* x_280; lean_object* x_281; uint8_t x_282; +x_280 = l_Lean_Syntax_getArgs(x_185); +x_281 = lean_array_get_size(x_280); +lean_dec(x_280); +x_282 = lean_nat_dec_eq(x_281, x_182); +lean_dec(x_281); +x_234 = x_282; +goto block_276; +} +block_276: +{ +if (x_234 == 0) +{ +lean_object* x_235; uint8_t x_236; +x_235 = l_Lean_Elab_Term_expandHave___closed__4; +lean_inc(x_185); +x_236 = l_Lean_Syntax_isOfKind(x_185, x_235); +if (x_236 == 0) +{ +uint8_t x_237; +x_237 = 0; +x_186 = x_237; +goto block_232; +} +else +{ +lean_object* x_238; lean_object* x_239; uint8_t x_240; +x_238 = l_Lean_Syntax_getArgs(x_185); +x_239 = lean_array_get_size(x_238); +lean_dec(x_238); +x_240 = lean_nat_dec_eq(x_239, x_182); +lean_dec(x_239); +x_186 = x_240; +goto block_232; +} +} +else +{ +lean_object* x_241; lean_object* x_242; uint8_t x_243; +x_241 = l_Lean_Syntax_getArg(x_185, x_7); +lean_dec(x_185); +x_242 = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__2; +lean_inc(x_241); +x_243 = l_Lean_Syntax_isOfKind(x_241, x_242); +if (x_243 == 0) +{ +lean_object* x_244; lean_object* x_245; +lean_dec(x_241); +lean_dec(x_183); +lean_dec(x_1); +x_244 = lean_box(1); +x_245 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_245, 0, x_244); +lean_ctor_set(x_245, 1, x_3); +return x_245; +} +else +{ +lean_object* x_246; lean_object* x_247; uint8_t x_248; uint8_t x_271; +x_246 = lean_unsigned_to_nat(4u); +x_247 = l_Lean_Syntax_getArg(x_1, x_246); +lean_inc(x_247); +x_271 = l_Lean_Syntax_isOfKind(x_247, x_174); +if (x_271 == 0) +{ +uint8_t x_272; +lean_dec(x_247); +x_272 = 0; +x_248 = x_272; +goto block_270; +} +else +{ +lean_object* x_273; lean_object* x_274; uint8_t x_275; +x_273 = l_Lean_Syntax_getArgs(x_247); +lean_dec(x_247); +x_274 = lean_array_get_size(x_273); +lean_dec(x_273); +x_275 = lean_nat_dec_eq(x_274, x_7); +lean_dec(x_274); +x_248 = x_275; +goto block_270; +} +block_270: +{ +if (x_248 == 0) +{ +lean_object* x_249; lean_object* x_250; +lean_dec(x_241); +lean_dec(x_183); +lean_dec(x_1); +x_249 = lean_box(1); +x_250 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_250, 0, x_249); +lean_ctor_set(x_250, 1, x_3); +return x_250; +} +else +{ +lean_object* x_251; lean_object* x_252; lean_object* x_253; lean_object* x_254; lean_object* x_255; lean_object* x_256; lean_object* x_257; lean_object* x_258; lean_object* x_259; lean_object* x_260; lean_object* x_261; lean_object* x_262; lean_object* x_263; lean_object* x_264; lean_object* x_265; lean_object* x_266; lean_object* x_267; lean_object* x_268; lean_object* x_269; +x_251 = lean_unsigned_to_nat(5u); +x_252 = l_Lean_Syntax_getArg(x_1, x_251); +lean_dec(x_1); +x_253 = l_Lean_Elab_Term_expandHave___closed__7; +x_254 = lean_array_push(x_253, x_183); +x_255 = l_Lean_Elab_Term_expandShow___closed__12; +x_256 = lean_array_push(x_255, x_241); +x_257 = l___regBuiltin_Lean_Elab_Term_elabByTactic___closed__2; +x_258 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_258, 0, x_257); +lean_ctor_set(x_258, 1, x_256); +x_259 = l_Lean_Elab_Term_expandShow___closed__9; +x_260 = lean_array_push(x_259, x_258); +x_261 = l_Lean_Elab_Term_expandShow___closed__4; +x_262 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_262, 0, x_261); +lean_ctor_set(x_262, 1, x_260); +x_263 = lean_array_push(x_254, x_262); +x_264 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; +x_265 = lean_array_push(x_263, x_264); +x_266 = lean_array_push(x_265, x_252); +x_267 = l_Lean_Elab_Term_expandHave___closed__2; +x_268 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_268, 0, x_267); +lean_ctor_set(x_268, 1, x_266); +x_269 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_269, 0, x_268); +lean_ctor_set(x_269, 1, x_3); +return x_269; +} +} } } } } else { -lean_object* x_225; lean_object* x_226; lean_object* x_227; lean_object* x_228; lean_object* x_229; lean_object* x_230; lean_object* x_231; lean_object* x_232; lean_object* x_233; lean_object* x_234; lean_object* x_235; lean_object* x_236; lean_object* x_237; lean_object* x_238; lean_object* x_239; lean_object* x_240; lean_object* x_241; lean_object* x_242; lean_object* x_243; lean_object* x_244; lean_object* x_245; lean_object* x_246; lean_object* x_247; lean_object* x_248; lean_object* x_249; lean_object* x_250; lean_object* x_251; lean_object* x_252; lean_object* x_253; lean_object* x_254; lean_object* x_255; lean_object* x_256; -x_225 = l_Lean_Syntax_getArg(x_149, x_7); -lean_dec(x_149); -x_226 = lean_unsigned_to_nat(5u); -x_227 = l_Lean_Syntax_getArg(x_1, x_226); -x_228 = l_Lean_Elab_Term_expandShow___closed__14; -x_229 = l_Lean_mkIdentFrom(x_1, x_228); +lean_object* x_283; lean_object* x_284; lean_object* x_285; uint8_t x_286; uint8_t x_321; +x_283 = l_Lean_Syntax_getArg(x_185, x_7); +lean_dec(x_185); +x_284 = lean_unsigned_to_nat(4u); +x_285 = l_Lean_Syntax_getArg(x_1, x_284); +lean_inc(x_285); +x_321 = l_Lean_Syntax_isOfKind(x_285, x_174); +if (x_321 == 0) +{ +uint8_t x_322; +lean_dec(x_285); +x_322 = 0; +x_286 = x_322; +goto block_320; +} +else +{ +lean_object* x_323; lean_object* x_324; uint8_t x_325; +x_323 = l_Lean_Syntax_getArgs(x_285); +lean_dec(x_285); +x_324 = lean_array_get_size(x_323); +lean_dec(x_323); +x_325 = lean_nat_dec_eq(x_324, x_7); +lean_dec(x_324); +x_286 = x_325; +goto block_320; +} +block_320: +{ +if (x_286 == 0) +{ +lean_object* x_287; lean_object* x_288; +lean_dec(x_283); +lean_dec(x_183); lean_dec(x_1); -x_230 = l_Array_empty___closed__1; -x_231 = lean_array_push(x_230, x_229); -x_232 = l___private_Lean_Elab_Quotation_8__letBindRhss___main___closed__13; -x_233 = lean_array_push(x_231, x_232); -x_234 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__26; -x_235 = lean_array_push(x_234, x_147); -x_236 = l_Lean_Elab_Term_elabLetDeclCore___closed__6; -x_237 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_237, 0, x_236); -lean_ctor_set(x_237, 1, x_235); -x_238 = lean_array_push(x_230, x_237); -x_239 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_239, 0, x_138); -lean_ctor_set(x_239, 1, x_238); -x_240 = lean_array_push(x_233, x_239); -x_241 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__10; -x_242 = lean_array_push(x_240, x_241); -x_243 = lean_array_push(x_242, x_225); -x_244 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__8; -x_245 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_245, 0, x_244); -lean_ctor_set(x_245, 1, x_243); -x_246 = lean_array_push(x_230, x_245); -x_247 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__6; -x_248 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_248, 0, x_247); -lean_ctor_set(x_248, 1, x_246); -x_249 = l_Lean_Elab_Term_expandShow___closed__16; -x_250 = lean_array_push(x_249, x_248); -x_251 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; -x_252 = lean_array_push(x_250, x_251); -x_253 = lean_array_push(x_252, x_227); -x_254 = l_Lean_Elab_Term_elabLetDeclCore___closed__8; -x_255 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_255, 0, x_254); -lean_ctor_set(x_255, 1, x_253); -x_256 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_256, 0, x_255); -lean_ctor_set(x_256, 1, x_3); -return x_256; +x_287 = lean_box(1); +x_288 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_288, 0, x_287); +lean_ctor_set(x_288, 1, x_3); +return x_288; +} +else +{ +lean_object* x_289; lean_object* x_290; lean_object* x_291; lean_object* x_292; lean_object* x_293; lean_object* x_294; lean_object* x_295; lean_object* x_296; lean_object* x_297; lean_object* x_298; lean_object* x_299; lean_object* x_300; lean_object* x_301; lean_object* x_302; lean_object* x_303; lean_object* x_304; lean_object* x_305; lean_object* x_306; lean_object* x_307; lean_object* x_308; lean_object* x_309; lean_object* x_310; lean_object* x_311; lean_object* x_312; lean_object* x_313; lean_object* x_314; lean_object* x_315; lean_object* x_316; lean_object* x_317; lean_object* x_318; lean_object* x_319; +x_289 = lean_unsigned_to_nat(5u); +x_290 = l_Lean_Syntax_getArg(x_1, x_289); +x_291 = l_Lean_Elab_Term_expandShow___closed__14; +x_292 = l_Lean_mkIdentFrom(x_1, x_291); +lean_dec(x_1); +x_293 = l_Array_empty___closed__1; +x_294 = lean_array_push(x_293, x_292); +x_295 = l___private_Lean_Elab_Quotation_8__letBindRhss___main___closed__13; +x_296 = lean_array_push(x_294, x_295); +x_297 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__26; +x_298 = lean_array_push(x_297, x_183); +x_299 = l_Lean_Elab_Term_elabLetDeclCore___closed__6; +x_300 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_300, 0, x_299); +lean_ctor_set(x_300, 1, x_298); +x_301 = lean_array_push(x_293, x_300); +x_302 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_302, 0, x_174); +lean_ctor_set(x_302, 1, x_301); +x_303 = lean_array_push(x_296, x_302); +x_304 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__10; +x_305 = lean_array_push(x_303, x_304); +x_306 = lean_array_push(x_305, x_283); +x_307 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__8; +x_308 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_308, 0, x_307); +lean_ctor_set(x_308, 1, x_306); +x_309 = lean_array_push(x_293, x_308); +x_310 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__6; +x_311 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_311, 0, x_310); +lean_ctor_set(x_311, 1, x_309); +x_312 = l_Lean_Elab_Term_expandShow___closed__16; +x_313 = lean_array_push(x_312, x_311); +x_314 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; +x_315 = lean_array_push(x_313, x_314); +x_316 = lean_array_push(x_315, x_290); +x_317 = l_Lean_Elab_Term_elabLetDeclCore___closed__8; +x_318 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_318, 0, x_317); +lean_ctor_set(x_318, 1, x_316); +x_319 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_319, 0, x_318); +lean_ctor_set(x_319, 1, x_3); +return x_319; +} +} } } } @@ -3819,7 +4084,7 @@ x_10 = lean_unsigned_to_nat(0u); x_11 = lean_nat_dec_eq(x_5, x_10); if (x_11 == 0) { -lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; +lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; x_12 = lean_unsigned_to_nat(1u); x_13 = lean_nat_sub(x_5, x_12); lean_dec(x_5); @@ -3832,26 +4097,32 @@ lean_inc(x_3); x_18 = lean_array_push(x_3, x_17); x_19 = lean_array_push(x_18, x_14); x_20 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; -x_21 = lean_array_push(x_19, x_20); -x_22 = lean_array_push(x_21, x_7); +lean_inc(x_3); +x_21 = lean_array_push(x_3, x_20); +x_22 = l_Lean_nullKind___closed__2; x_23 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_23, 0, x_16); -lean_ctor_set(x_23, 1, x_22); +lean_ctor_set(x_23, 0, x_22); +lean_ctor_set(x_23, 1, x_21); +x_24 = lean_array_push(x_19, x_23); +x_25 = lean_array_push(x_24, x_7); +x_26 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_26, 0, x_16); +lean_ctor_set(x_26, 1, x_25); x_5 = x_13; x_6 = lean_box(0); -x_7 = x_23; +x_7 = x_26; goto _start; } else { -lean_object* x_25; +lean_object* x_28; lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); -x_25 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_25, 0, x_7); -lean_ctor_set(x_25, 1, x_9); -return x_25; +x_28 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_28, 0, x_7); +lean_ctor_set(x_28, 1, x_9); +return x_28; } } } diff --git a/stage0/stdlib/Lean/Elab/Do.c b/stage0/stdlib/Lean/Elab/Do.c index becc5ee929..83eb45a74b 100644 --- a/stage0/stdlib/Lean/Elab/Do.c +++ b/stage0/stdlib/Lean/Elab/Do.c @@ -14,6 +14,7 @@ extern "C" { #endif extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__15; +extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; lean_object* l___private_Lean_Elab_Do_6__expandLiftMethodAux___main___closed__4; lean_object* lean_array_set(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Do_11__processDoElemsAux___main___closed__4; @@ -3478,7 +3479,7 @@ lean_ctor_set(x_492, 0, x_491); lean_ctor_set(x_492, 1, x_490); x_493 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_494 = lean_array_push(x_493, x_472); -x_495 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_495 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_496 = lean_array_push(x_494, x_495); x_497 = lean_array_push(x_496, x_492); x_498 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -3535,7 +3536,7 @@ x_517 = l_Lean_Syntax_getArg(x_516, x_515); lean_dec(x_516); x_518 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_519 = lean_array_push(x_518, x_472); -x_520 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_520 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_521 = lean_array_push(x_519, x_520); x_522 = lean_array_push(x_521, x_517); x_523 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -4363,7 +4364,7 @@ lean_ctor_set(x_980, 0, x_979); lean_ctor_set(x_980, 1, x_978); x_981 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_982 = lean_array_push(x_981, x_960); -x_983 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_983 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_984 = lean_array_push(x_982, x_983); x_985 = lean_array_push(x_984, x_980); x_986 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -4425,7 +4426,7 @@ x_1007 = l_Lean_Syntax_getArg(x_1006, x_1005); lean_dec(x_1006); x_1008 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_1009 = lean_array_push(x_1008, x_960); -x_1010 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_1010 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_1011 = lean_array_push(x_1009, x_1010); x_1012 = lean_array_push(x_1011, x_1007); x_1013 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; diff --git a/stage0/stdlib/Lean/Elab/Match.c b/stage0/stdlib/Lean/Elab/Match.c index bd59e4d842..8d8263353a 100644 --- a/stage0/stdlib/Lean/Elab/Match.c +++ b/stage0/stdlib/Lean/Elab/Match.c @@ -19,6 +19,7 @@ lean_object* l_List_reverse___rarg(lean_object*); lean_object* l___private_Lean_Elab_Match_9__getMatchAlts(lean_object*); lean_object* l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2; lean_object* l___private_Lean_Elab_Match_27__nameToPattern___main___closed__3; +extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; lean_object* lean_array_set(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabNoMatch___closed__1; lean_object* l_Lean_mkAppStx(lean_object*, lean_object*); @@ -427,7 +428,6 @@ extern lean_object* l___private_Lean_Elab_App_22__elabAppFn___main___closed__5; uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_elabMatch___spec__10(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Match_3__elabDiscrsWitMatchTypeAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Syntax_inhabited; -extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; lean_object* l_Lean_Elab_Term_elabMVarWithIdKind___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Match_6__elabMatchTypeAndDiscrsAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -741,7 +741,7 @@ lean_ctor_set(x_29, 0, x_28); lean_ctor_set(x_29, 1, x_27); x_30 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_31 = lean_array_push(x_30, x_29); -x_32 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_32 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_33 = lean_array_push(x_31, x_32); x_34 = lean_array_push(x_33, x_4); x_35 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -853,7 +853,7 @@ lean_ctor_set(x_37, 0, x_36); lean_ctor_set(x_37, 1, x_35); x_38 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_39 = lean_array_push(x_38, x_37); -x_40 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_40 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_41 = lean_array_push(x_39, x_40); x_42 = lean_array_push(x_41, x_5); x_43 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; diff --git a/stage0/stdlib/Lean/Elab/Quotation.c b/stage0/stdlib/Lean/Elab/Quotation.c index 6982f19a47..1805b0d122 100644 --- a/stage0/stdlib/Lean/Elab/Quotation.c +++ b/stage0/stdlib/Lean/Elab/Quotation.c @@ -18,6 +18,7 @@ uint8_t l_Lean_Syntax_isQuot(lean_object*); extern lean_object* l_Lean_Expr_eq_x3f___closed__1; lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__15; lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__56; +lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; lean_object* l_List_foldl___main___at___private_Lean_Elab_Quotation_10__toPreterm___main___spec__3(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Quotation_9__exprPlaceholder___closed__1; lean_object* l___private_Lean_Elab_Quotation_8__letBindRhss___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -133,6 +134,7 @@ lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__1; lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSyntax___closed__1; lean_object* l_Lean_Elab_Term_Quotation_antiquotKind_x3f___closed__1; lean_object* l_List_head_x21___at___private_Lean_Elab_Quotation_6__compileStxMatch___main___spec__2___closed__3; +lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__17; lean_object* lean_string_utf8_byte_size(lean_object*); lean_object* l_Lean_Elab_Term_Quotation_elabStxQuot(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_mkAppStx___closed__4; @@ -4670,6 +4672,28 @@ lean_ctor_set(x_3, 1, x_2); return x_3; } } +lean_object* _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__17() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Array_empty___closed__1; +x_2 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_3 = lean_array_push(x_1, x_2); +return x_3; +} +} +lean_object* _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_nullKind___closed__2; +x_2 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__17; +x_3 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) { _start: { @@ -4715,7 +4739,7 @@ lean_ctor_set(x_34, 0, x_33); lean_ctor_set(x_34, 1, x_32); x_35 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_36 = lean_array_push(x_35, x_34); -x_37 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_37 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_38 = lean_array_push(x_36, x_37); x_39 = lean_array_push(x_38, x_2); x_40 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -4762,7 +4786,7 @@ lean_ctor_set(x_62, 0, x_61); lean_ctor_set(x_62, 1, x_60); x_63 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_64 = lean_array_push(x_63, x_62); -x_65 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_65 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_66 = lean_array_push(x_64, x_65); x_67 = lean_array_push(x_66, x_2); x_68 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -5051,7 +5075,7 @@ lean_ctor_set(x_58, 0, x_21); lean_ctor_set(x_58, 1, x_57); x_59 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_60 = lean_array_push(x_59, x_58); -x_61 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_61 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_62 = lean_array_push(x_60, x_61); x_63 = lean_array_push(x_62, x_4); x_64 = lean_alloc_ctor(1, 2, 0); @@ -5136,7 +5160,7 @@ lean_ctor_set(x_107, 0, x_70); lean_ctor_set(x_107, 1, x_106); x_108 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_109 = lean_array_push(x_108, x_107); -x_110 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_110 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_111 = lean_array_push(x_109, x_110); x_112 = lean_array_push(x_111, x_4); x_113 = lean_alloc_ctor(1, 2, 0); @@ -5255,7 +5279,7 @@ lean_ctor_set(x_34, 0, x_33); lean_ctor_set(x_34, 1, x_32); x_35 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_36 = lean_array_push(x_35, x_34); -x_37 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_37 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_38 = lean_array_push(x_36, x_37); x_39 = lean_array_push(x_38, x_2); x_40 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -5302,7 +5326,7 @@ lean_ctor_set(x_62, 0, x_61); lean_ctor_set(x_62, 1, x_60); x_63 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_64 = lean_array_push(x_63, x_62); -x_65 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_65 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_66 = lean_array_push(x_64, x_65); x_67 = lean_array_push(x_66, x_2); x_68 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -8068,7 +8092,7 @@ lean_ctor_set(x_83, 0, x_82); lean_ctor_set(x_83, 1, x_81); x_84 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_85 = lean_array_push(x_84, x_83); -x_86 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_86 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_87 = lean_array_push(x_85, x_86); x_88 = lean_array_push(x_87, x_58); x_89 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -8114,7 +8138,7 @@ lean_ctor_set(x_110, 0, x_109); lean_ctor_set(x_110, 1, x_108); x_111 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_112 = lean_array_push(x_111, x_110); -x_113 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_113 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_114 = lean_array_push(x_112, x_113); x_115 = lean_array_push(x_114, x_58); x_116 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -8273,7 +8297,7 @@ lean_ctor_set(x_181, 0, x_180); lean_ctor_set(x_181, 1, x_179); x_182 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_183 = lean_array_push(x_182, x_181); -x_184 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_184 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_185 = lean_array_push(x_183, x_184); x_186 = lean_array_push(x_148, x_161); x_187 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19; @@ -8346,7 +8370,7 @@ lean_ctor_set(x_225, 0, x_224); lean_ctor_set(x_225, 1, x_223); x_226 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_227 = lean_array_push(x_226, x_225); -x_228 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_228 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_229 = lean_array_push(x_227, x_228); x_230 = lean_array_push(x_148, x_161); x_231 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19; @@ -8564,7 +8588,7 @@ lean_ctor_set(x_317, 0, x_316); lean_ctor_set(x_317, 1, x_315); x_318 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_319 = lean_array_push(x_318, x_317); -x_320 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_320 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_321 = lean_array_push(x_319, x_320); x_322 = lean_array_push(x_283, x_296); x_323 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19; @@ -8824,7 +8848,7 @@ lean_ctor_set(x_402, 0, x_401); lean_ctor_set(x_402, 1, x_400); x_403 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_404 = lean_array_push(x_403, x_402); -x_405 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_405 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_406 = lean_array_push(x_404, x_405); x_407 = lean_array_push(x_406, x_376); x_408 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -9014,7 +9038,7 @@ lean_ctor_set(x_478, 0, x_477); lean_ctor_set(x_478, 1, x_476); x_479 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_480 = lean_array_push(x_479, x_478); -x_481 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_481 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_482 = lean_array_push(x_480, x_481); x_483 = lean_array_push(x_444, x_457); x_484 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19; @@ -9334,7 +9358,7 @@ lean_ctor_set(x_578, 0, x_577); lean_ctor_set(x_578, 1, x_576); x_579 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_580 = lean_array_push(x_579, x_578); -x_581 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_581 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_582 = lean_array_push(x_580, x_581); x_583 = lean_array_push(x_582, x_553); x_584 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -9380,7 +9404,7 @@ lean_ctor_set(x_605, 0, x_604); lean_ctor_set(x_605, 1, x_603); x_606 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_607 = lean_array_push(x_606, x_605); -x_608 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_608 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_609 = lean_array_push(x_607, x_608); x_610 = lean_array_push(x_609, x_553); x_611 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -9611,7 +9635,7 @@ lean_ctor_set(x_719, 0, x_718); lean_ctor_set(x_719, 1, x_717); x_720 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_721 = lean_array_push(x_720, x_719); -x_722 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_722 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_723 = lean_array_push(x_721, x_722); x_724 = lean_array_push(x_643, x_700); x_725 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19; @@ -9683,7 +9707,7 @@ lean_ctor_set(x_762, 0, x_761); lean_ctor_set(x_762, 1, x_760); x_763 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_764 = lean_array_push(x_763, x_762); -x_765 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_765 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_766 = lean_array_push(x_764, x_765); x_767 = lean_array_push(x_643, x_700); x_768 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19; @@ -9974,7 +9998,7 @@ lean_ctor_set(x_897, 0, x_896); lean_ctor_set(x_897, 1, x_895); x_898 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_899 = lean_array_push(x_898, x_897); -x_900 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_900 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_901 = lean_array_push(x_899, x_900); x_902 = lean_array_push(x_820, x_877); x_903 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19; @@ -10237,7 +10261,7 @@ lean_ctor_set(x_982, 0, x_981); lean_ctor_set(x_982, 1, x_980); x_983 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_984 = lean_array_push(x_983, x_982); -x_985 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_985 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_986 = lean_array_push(x_984, x_985); x_987 = lean_array_push(x_986, x_956); x_988 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -10499,7 +10523,7 @@ lean_ctor_set(x_1101, 0, x_1100); lean_ctor_set(x_1101, 1, x_1099); x_1102 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_1103 = lean_array_push(x_1102, x_1101); -x_1104 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_1104 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_1105 = lean_array_push(x_1103, x_1104); x_1106 = lean_array_push(x_1024, x_1081); x_1107 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19; @@ -11262,7 +11286,7 @@ lean_ctor_set(x_84, 0, x_83); lean_ctor_set(x_84, 1, x_82); x_85 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_86 = lean_array_push(x_85, x_84); -x_87 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_87 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_88 = lean_array_push(x_86, x_87); x_89 = lean_array_push(x_88, x_59); x_90 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -11310,7 +11334,7 @@ lean_ctor_set(x_111, 0, x_110); lean_ctor_set(x_111, 1, x_109); x_112 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_113 = lean_array_push(x_112, x_111); -x_114 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_114 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_115 = lean_array_push(x_113, x_114); x_116 = lean_array_push(x_115, x_59); x_117 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -11472,7 +11496,7 @@ lean_ctor_set(x_170, 0, x_169); lean_ctor_set(x_170, 1, x_168); x_171 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_172 = lean_array_push(x_171, x_170); -x_173 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_173 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_174 = lean_array_push(x_172, x_173); x_175 = lean_array_push(x_174, x_144); x_176 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -11678,7 +11702,7 @@ lean_ctor_set(x_252, 0, x_251); lean_ctor_set(x_252, 1, x_250); x_253 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_254 = lean_array_push(x_253, x_252); -x_255 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_255 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_256 = lean_array_push(x_254, x_255); x_257 = lean_array_push(x_256, x_230); x_258 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -11721,7 +11745,7 @@ lean_ctor_set(x_276, 0, x_275); lean_ctor_set(x_276, 1, x_274); x_277 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_278 = lean_array_push(x_277, x_276); -x_279 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_279 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_280 = lean_array_push(x_278, x_279); x_281 = lean_array_push(x_280, x_230); x_282 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -11878,7 +11902,7 @@ lean_ctor_set(x_332, 0, x_331); lean_ctor_set(x_332, 1, x_330); x_333 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_334 = lean_array_push(x_333, x_332); -x_335 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_335 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_336 = lean_array_push(x_334, x_335); x_337 = lean_array_push(x_336, x_309); x_338 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -12100,7 +12124,7 @@ lean_ctor_set(x_414, 0, x_413); lean_ctor_set(x_414, 1, x_412); x_415 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_416 = lean_array_push(x_415, x_414); -x_417 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_417 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_418 = lean_array_push(x_416, x_417); x_419 = lean_array_push(x_418, x_391); x_420 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -12335,7 +12359,7 @@ lean_ctor_set(x_501, 0, x_500); lean_ctor_set(x_501, 1, x_499); x_502 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_503 = lean_array_push(x_502, x_501); -x_504 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_504 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_505 = lean_array_push(x_503, x_504); x_506 = lean_array_push(x_505, x_475); x_507 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -12575,7 +12599,7 @@ lean_ctor_set(x_588, 0, x_587); lean_ctor_set(x_588, 1, x_586); x_589 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_590 = lean_array_push(x_589, x_588); -x_591 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_591 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_592 = lean_array_push(x_590, x_591); x_593 = lean_array_push(x_592, x_565); x_594 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -12826,7 +12850,7 @@ lean_ctor_set(x_678, 0, x_677); lean_ctor_set(x_678, 1, x_676); x_679 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_680 = lean_array_push(x_679, x_678); -x_681 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_681 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_682 = lean_array_push(x_680, x_681); x_683 = lean_array_push(x_682, x_652); x_684 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -13069,7 +13093,7 @@ lean_ctor_set(x_765, 0, x_764); lean_ctor_set(x_765, 1, x_763); x_766 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_767 = lean_array_push(x_766, x_765); -x_768 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_768 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_769 = lean_array_push(x_767, x_768); x_770 = lean_array_push(x_769, x_742); x_771 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -23860,6 +23884,10 @@ l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__15 = _init lean_mark_persistent(l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__15); l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16 = _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16(); lean_mark_persistent(l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16); +l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__17 = _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__17(); +lean_mark_persistent(l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__17); +l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18 = _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18(); +lean_mark_persistent(l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18); l___private_Lean_Elab_Quotation_4__getHeadInfo___lambda__1___closed__1 = _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___lambda__1___closed__1(); lean_mark_persistent(l___private_Lean_Elab_Quotation_4__getHeadInfo___lambda__1___closed__1); l___private_Lean_Elab_Quotation_4__getHeadInfo___lambda__1___closed__2 = _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___lambda__1___closed__2(); diff --git a/stage0/stdlib/Lean/Elab/StructInst.c b/stage0/stdlib/Lean/Elab/StructInst.c index c7f1ec8862..1a1d552e00 100644 --- a/stage0/stdlib/Lean/Elab/StructInst.c +++ b/stage0/stdlib/Lean/Elab/StructInst.c @@ -19,6 +19,7 @@ lean_object* l_Lean_Elab_Term_StructInst_formatStruct___main(lean_object*); lean_object* l___private_Lean_Elab_StructInst_1__expandNonAtomicExplicitSource___closed__3; lean_object* l_Lean_Elab_Term_StructInst_Struct_modifyFields(lean_object*, lean_object*); lean_object* l_Lean_fmt___at_Lean_Position_Lean_HasFormat___spec__1(lean_object*); +extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; lean_object* l_List_forM___main___at_Lean_Elab_Term_StructInst_DefaultFields_step___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_StructInst_17__groupFields___lambda__2___boxed(lean_object*, lean_object*); lean_object* l___private_Lean_Elab_StructInst_12__mkFieldMap(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -372,7 +373,6 @@ extern lean_object* l_Lean_Syntax_inhabited; size_t lean_ptr_addr(lean_object*); lean_object* l_Array_foldlStepMAux___main___at___private_Lean_Elab_StructInst_3__isModifyOp_x3f___spec__1___closed__3; lean_object* l_Lean_throwError___at_Lean_Elab_Term_StructInst_DefaultFields_propagateLoop___main___spec__2(lean_object*); -extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_propagateLoop___main___closed__3; lean_object* lean_instantiate_value_lparams(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_StructInst_throwFailedToElabField___rarg___closed__2; @@ -849,7 +849,7 @@ lean_ctor_set(x_61, 0, x_60); lean_ctor_set(x_61, 1, x_59); x_62 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_63 = lean_array_push(x_62, x_61); -x_64 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_64 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_65 = lean_array_push(x_63, x_64); x_66 = lean_array_push(x_65, x_40); x_67 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -894,7 +894,7 @@ lean_ctor_set(x_86, 0, x_85); lean_ctor_set(x_86, 1, x_84); x_87 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_88 = lean_array_push(x_87, x_86); -x_89 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_89 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_90 = lean_array_push(x_88, x_89); x_91 = lean_array_push(x_90, x_40); x_92 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -1056,7 +1056,7 @@ lean_ctor_set(x_152, 0, x_151); lean_ctor_set(x_152, 1, x_150); x_153 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_154 = lean_array_push(x_153, x_152); -x_155 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_155 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_156 = lean_array_push(x_154, x_155); x_157 = lean_array_push(x_156, x_130); x_158 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; @@ -1290,7 +1290,7 @@ lean_ctor_set(x_231, 0, x_230); lean_ctor_set(x_231, 1, x_229); x_232 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4; x_233 = lean_array_push(x_232, x_231); -x_234 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16; +x_234 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18; x_235 = lean_array_push(x_233, x_234); x_236 = lean_array_push(x_235, x_209); x_237 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2; diff --git a/stage0/stdlib/Lean/Parser/Tactic.c b/stage0/stdlib/Lean/Parser/Tactic.c index 4305bf4aef..10c7c24a47 100644 --- a/stage0/stdlib/Lean/Parser/Tactic.c +++ b/stage0/stdlib/Lean/Parser/Tactic.c @@ -125,6 +125,7 @@ extern lean_object* l_Lean_mkThunk___closed__1; lean_object* l_Lean_Parser_Tactic_admit___closed__5; lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_matchAlts_parenthesizer___closed__2; +lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__7; lean_object* l_Lean_Parser_Tactic_orelse___closed__1; lean_object* l_Lean_Parser_Tactic_failIfSuccess___closed__6; lean_object* l___regBuiltin_Lean_Parser_Tactic_orelse_parenthesizer___closed__1; @@ -265,6 +266,7 @@ lean_object* l_Lean_Parser_Tactic_paren_parenthesizer___closed__2; 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*); +lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__6; lean_object* l_Lean_Parser_Tactic_done_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__6; @@ -332,6 +334,7 @@ lean_object* lean_array_get_size(lean_object*); lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_location___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_let___elambda__1___closed__1; +lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__5; extern lean_object* l_Lean_Parser_Tactic_seq1; extern lean_object* l_Lean_Parser_Term_subtype_formatter___closed__6; lean_object* l_Lean_Parser_Tactic_refine_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -342,6 +345,7 @@ lean_object* l_Lean_Parser_Tactic_induction_formatter___closed__5; extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2; lean_object* l_Lean_Parser_Tactic_matchAlts_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__5; +lean_object* l_Lean_Parser_Tactic_focus_parenthesizer___closed__1; extern lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__18; lean_object* l_Lean_Parser_Tactic_withIds___closed__2; lean_object* l_Lean_Parser_tokenFn(lean_object*, lean_object*); @@ -439,6 +443,7 @@ lean_object* l_Lean_Parser_Tactic_case_formatter___closed__6; lean_object* l_Lean_Parser_Tactic_apply___closed__5; lean_object* l_Lean_Parser_Tactic_done_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__3; +lean_object* l_Lean_Parser_Tactic_focus___closed__2; lean_object* l_Lean_Parser_Tactic_changeWith_formatter___closed__3; lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__2; lean_object* l_Lean_Parser_Tactic_assumption___closed__4; @@ -529,7 +534,9 @@ lean_object* l_Lean_Parser_Tactic_subst___closed__2; lean_object* l_Lean_Parser_Tactic_rewrite; lean_object* l___regBuiltin_Lean_Parser_Tactic_injection_parenthesizer(lean_object*); lean_object* l_Lean_Parser_Tactic_refine_x21_formatter___closed__2; +lean_object* l_Lean_Parser_Tactic_focus___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_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; @@ -537,6 +544,7 @@ lean_object* l_Lean_Parser_Tactic_failIfSuccess___closed__7; lean_object* l_Lean_Parser_Tactic_withIds_formatter___closed__2; lean_object* l_Lean_Parser_Tactic_inductionAlts___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_failIfSuccess_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__6; lean_object* l_Lean_Parser_Tactic_traceState___closed__5; lean_object* l___regBuiltin_Lean_Parser_Tactic_injection_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_changeWith_formatter___closed__5; @@ -672,6 +680,7 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_failIfSuccess_formatter___closed_ lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Tactic_locationHyp___elambda__1___spec__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__9; lean_object* l_Lean_Parser_Tactic_changeWith___closed__8; +lean_object* l_Lean_Parser_Tactic_focus___closed__1; lean_object* l_Lean_Parser_Tactic_change___closed__8; lean_object* l___regBuiltinParser_Lean_Parser_Tactic_intros(lean_object*); lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__6; @@ -690,6 +699,7 @@ lean_object* l_Lean_Parser_Tactic_generalizingVars_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_rewrite___closed__9; lean_object* l_Lean_Parser_Tactic_admit___closed__4; lean_object* l_Lean_Parser_Tactic_matchAlts_parenthesizer___closed__4; +lean_object* l_Lean_Parser_Tactic_focus; lean_object* l_Lean_Parser_Tactic_rewrite_formatter___closed__7; lean_object* l_Lean_Parser_Tactic_intro_parenthesizer___closed__6; lean_object* l___regBuiltin_Lean_Parser_Tactic_clear_formatter___closed__1; @@ -705,6 +715,7 @@ lean_object* l_Lean_Parser_Tactic_let_x21___closed__2; lean_object* l_Lean_Parser_Tactic_changeWith_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_matchAlt___closed__1; lean_object* l_Lean_Parser_Tactic_majorPremise_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Tactic_focus___closed__6; lean_object* l_Lean_Parser_Tactic_generalize_formatter___closed__10; lean_object* l_Lean_Parser_Tactic_changeWith___closed__1; lean_object* l_Lean_Parser_Tactic_apply_formatter___closed__4; @@ -790,6 +801,7 @@ lean_object* l_Lean_Parser_Tactic_let_formatter(lean_object*, lean_object*, lean lean_object* l_Lean_Parser_Tactic_ident_x27_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_generalize___closed__11; lean_object* l_Lean_Parser_Tactic_injection___elambda__1___closed__3; +lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__2; lean_object* l___regBuiltin_Lean_Parser_Tactic_match_formatter___closed__1; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_tupleTail___elambda__1___spec__1(uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_rewrite___elambda__1___closed__3; @@ -819,6 +831,7 @@ extern lean_object* l___regBuiltin_Lean_Parser_Term_syntheticHole_parenthesizer_ lean_object* l_Lean_Parser_Tactic_admit___closed__2; lean_object* lean_name_mk_string(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_orelse_parenthesizer___closed__1; +lean_object* l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_rwRuleSeq; lean_object* l_Lean_Parser_Tactic_rewrite___closed__1; extern lean_object* l_Lean_Parser_Term_match___closed__2; @@ -857,6 +870,7 @@ lean_object* l_Lean_Parser_Tactic_locationWildcard___elambda__1___closed__2; lean_object* l_Lean_Parser_Tactic_refine_formatter___closed__3; lean_object* l_Lean_Parser_Tactic_traceState___closed__6; lean_object* l___regBuiltin_Lean_Parser_Tactic_skip_parenthesizer(lean_object*); +lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_let___closed__4; lean_object* l_Lean_Parser_Tactic_let_formatter___closed__1; lean_object* l___regBuiltin_Lean_Parser_Tactic_clear_parenthesizer___closed__1; @@ -898,6 +912,7 @@ lean_object* l_Lean_Parser_Tactic_induction_parenthesizer___closed__3; lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_let_x21___elambda__1___closed__2; lean_object* l_Lean_Parser_Tactic_paren___closed__3; +lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__8; lean_object* l_Lean_Parser_Tactic_inductionAlts_parenthesizer___closed__2; lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__3; lean_object* l_Lean_Parser_Tactic_majorPremise___closed__2; @@ -937,6 +952,7 @@ lean_object* l_Lean_Parser_Tactic_introMatch___elambda__1___closed__3; 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_paren_formatter___closed__3; +lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__4; lean_object* l___regBuiltin_Lean_Parser_Tactic_admit_parenthesizer(lean_object*); lean_object* l_Lean_Parser_Tactic_refine___elambda__1___closed__7; lean_object* l___regBuiltin_Lean_Parser_Tactic_failIfSuccess_parenthesizer___closed__1; @@ -997,6 +1013,7 @@ lean_object* l_Lean_Parser_Tactic_rewriteSeq_parenthesizer___closed__3; lean_object* l_Lean_Parser_Tactic_subst___closed__3; lean_object* l_Lean_Parser_ParserState_popSyntax(lean_object*); lean_object* l_Lean_Parser_Tactic_usingRec_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Tactic_focus_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_paren_parenthesizer___closed__4; lean_object* l_Lean_Parser_Tactic_subst_formatter___closed__2; lean_object* l_Lean_Parser_Tactic_paren___elambda__1___closed__2; @@ -1082,6 +1099,7 @@ lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__6; lean_object* l___regBuiltin_Lean_Parser_Tactic_refine_parenthesizer(lean_object*); lean_object* l___regBuiltin_Lean_Parser_Tactic_induction_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_location_parenthesizer___closed__1; +lean_object* l_Lean_Parser_Tactic_focus_formatter___closed__2; lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__6; lean_object* l___regBuiltin_Lean_Parser_Tactic_refine_formatter(lean_object*); lean_object* l_Lean_Parser_Tactic_intros___closed__9; @@ -1131,6 +1149,7 @@ lean_object* l_Lean_Parser_Tactic_refine___closed__2; lean_object* l_Lean_Parser_Tactic_orelse_formatter___closed__1; lean_object* l___regBuiltinParser_Lean_Parser_Tactic_exact(lean_object*); lean_object* l_Lean_Parser_Tactic_assumption___elambda__1___closed__1; +lean_object* l_Lean_Parser_Tactic_focus_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_show___closed__3; lean_object* l_Lean_Parser_Tactic_location_formatter___closed__2; lean_object* l_Lean_Parser_Tactic_majorPremise___closed__6; @@ -1150,6 +1169,7 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_let_x21_formatter(lean_object*); lean_object* l_Lean_Parser_Tactic_locationTarget_parenthesizer___closed__2; lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_matchAlt_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Tactic_focus___closed__5; lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__2; lean_object* l___regBuiltin_Lean_Parser_Tactic_nestedTactic_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__8; @@ -1190,6 +1210,7 @@ lean_object* l_Lean_Parser_Tactic_cases___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__12; lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__4; lean_object* l_Lean_Parser_Tactic_have___elambda__1(lean_object*, lean_object*); +lean_object* l_Lean_Parser_Tactic_focus_formatter___closed__3; extern lean_object* l_Lean_Parser_Term_let___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_revert___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_suffices; @@ -1263,6 +1284,7 @@ lean_object* l_Lean_Parser_Tactic_rwRule_parenthesizer___closed__4; extern lean_object* l_Lean_Parser_epsilonInfo; lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_change___elambda__1___closed__3; +lean_object* l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer(lean_object*); lean_object* l_Lean_Parser_Tactic_assumption___closed__3; lean_object* l_Lean_Parser_Tactic_done___closed__1; lean_object* l_Lean_Parser_Tactic_locationWildcard___elambda__1(lean_object*, lean_object*); @@ -1275,6 +1297,7 @@ extern lean_object* l_Lean_Parser_Term_typeAscription___closed__1; lean_object* l___regBuiltin_Lean_Parser_Tactic_changeWith_formatter(lean_object*); lean_object* l_Lean_Parser_Tactic_case_formatter___closed__5; lean_object* l_Lean_Parser_Tactic_majorPremise___elambda__1___closed__4; +lean_object* l___regBuiltin_Lean_Parser_Tactic_focus_formatter(lean_object*); lean_object* l_Lean_Parser_Tactic_locationTarget___closed__5; lean_object* l_Lean_Parser_categoryParser___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Parser_Tactic_show_formatter___closed__1; @@ -1301,6 +1324,7 @@ lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__6; lean_object* l_Lean_Parser_Tactic_suffices_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_traceState___elambda__1___closed__6; lean_object* l_Lean_Parser_Tactic_rwRule___closed__1; +lean_object* l_Lean_Parser_Tactic_focus_formatter___closed__4; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__1(uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_change___elambda__1(lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_match_parenthesizer___closed__3; @@ -1355,6 +1379,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Tactic_paren(lean_object*); lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__2; lean_object* l_Lean_Parser_Tactic_matchAlt; lean_object* l_Lean_Parser_Tactic_done___closed__4; +lean_object* l_Lean_Parser_Tactic_focus___closed__7; lean_object* l_Lean_Parser_Tactic_locationHyp___elambda__1___closed__4; lean_object* l_String_trim(lean_object*); lean_object* l_Lean_Parser_Tactic_allGoals_formatter___closed__2; @@ -1373,6 +1398,7 @@ lean_object* l_Lean_Parser_Tactic_matchAlt_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_locationWildcard_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_change_parenthesizer___closed__4; lean_object* l_Lean_Parser_Tactic_revert_parenthesizer___closed__3; +lean_object* l___regBuiltin_Lean_Parser_Tactic_focus_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_rewrite_formatter___closed__2; lean_object* l_Lean_Parser_Tactic_locationTarget; lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__5; @@ -1428,6 +1454,7 @@ lean_object* l_Lean_Parser_Tactic_suffices___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_rewrite_parenthesizer___closed__7; lean_object* l_Lean_Parser_Tactic_intro___closed__2; lean_object* l_Lean_Parser_Tactic_exact_formatter___closed__2; +lean_object* l_Lean_Parser_Tactic_focus___closed__3; lean_object* l_Lean_Parser_Tactic_generalize_formatter___closed__8; lean_object* l_Lean_Parser_Tactic_change___elambda__1___closed__8; lean_object* l_Lean_Parser_Term_syntheticHole___elambda__1(lean_object*, lean_object*); @@ -1568,6 +1595,7 @@ lean_object* l_Lean_Parser_Tactic_assumption___elambda__1(lean_object*, lean_obj lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__5; lean_object* l_Lean_Parser_Tactic_matchAlts; lean_object* l___regBuiltin_Lean_Parser_Tactic_refine_x21_formatter(lean_object*); +lean_object* l_Lean_Parser_Tactic_focus_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_locationTarget___elambda__1___closed__9; lean_object* l_Lean_Parser_Tactic_admit_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_refine_x21_formatter___closed__3; @@ -1597,6 +1625,7 @@ lean_object* l_Lean_Parser_Tactic_subst___elambda__1___closed__4; lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__10; lean_object* l_Lean_Parser_Tactic_show_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_let_x21___closed__3; +lean_object* l_Lean_Parser_Tactic_focus_parenthesizer___closed__2; lean_object* l_Lean_Parser_Tactic_locationHyp_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_matchAlts_formatter___closed__4; lean_object* l_Lean_PrettyPrinter_Formatter_notFollowedBy_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1652,6 +1681,7 @@ 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*); lean_object* l_Lean_Parser_Tactic_skip___closed__4; +lean_object* l_Lean_Parser_Tactic_focus___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_rwRule___closed__7; lean_object* l_Lean_Parser_Tactic_rwRule_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Parser_Tactic_allGoals_formatter___closed__1; @@ -9190,6 +9220,478 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } +lean_object* _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("focus"); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2; +x_2 = l_Lean_Parser_Tactic_focus___elambda__1___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2; +x_2 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__1; +x_2 = l_Lean_Parser_Tactic_focus___elambda__1___closed__3; +x_3 = 1; +x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__5() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("focus "); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__5; +x_2 = l_String_trim(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Char_HasRepr___closed__1; +x_2 = l_Lean_Parser_Tactic_focus___elambda__1___closed__6; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__8() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__7; +x_2 = l_Char_HasRepr___closed__1; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* l_Lean_Parser_Tactic_focus___elambda__1(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7; +x_3 = l_Lean_Parser_Tactic_tacticSeq; +x_4 = lean_ctor_get(x_3, 1); +lean_inc(x_4); +x_5 = l_Lean_Parser_Tactic_focus___elambda__1___closed__4; +x_6 = lean_ctor_get(x_5, 1); +lean_inc(x_6); +lean_inc(x_2); +lean_inc(x_1); +x_7 = l_Lean_Parser_tryAnti(x_1, x_2); +if (x_7 == 0) +{ +lean_object* x_8; lean_object* x_9; lean_object* x_10; +lean_dec(x_6); +x_8 = lean_unsigned_to_nat(1024u); +x_9 = l_Lean_Parser_checkPrecFn(x_8, x_1, x_2); +x_10 = lean_ctor_get(x_9, 3); +lean_inc(x_10); +if (lean_obj_tag(x_10) == 0) +{ +lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; +x_11 = lean_ctor_get(x_9, 0); +lean_inc(x_11); +x_12 = lean_array_get_size(x_11); +lean_dec(x_11); +x_13 = l_Lean_Parser_Tactic_focus___elambda__1___closed__6; +x_14 = l_Lean_Parser_Tactic_focus___elambda__1___closed__8; +lean_inc(x_1); +x_15 = l_Lean_Parser_nonReservedSymbolFnAux(x_13, x_14, x_1, x_9); +x_16 = lean_ctor_get(x_15, 3); +lean_inc(x_16); +if (lean_obj_tag(x_16) == 0) +{ +lean_object* x_17; lean_object* x_18; lean_object* x_19; +x_17 = lean_apply_2(x_4, x_1, x_15); +x_18 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2; +x_19 = l_Lean_Parser_ParserState_mkNode(x_17, x_18, x_12); +return x_19; +} +else +{ +lean_object* x_20; lean_object* x_21; +lean_dec(x_16); +lean_dec(x_4); +lean_dec(x_1); +x_20 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2; +x_21 = l_Lean_Parser_ParserState_mkNode(x_15, x_20, x_12); +return x_21; +} +} +else +{ +lean_dec(x_10); +lean_dec(x_4); +lean_dec(x_1); +return x_9; +} +} +else +{ +lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; +x_22 = lean_ctor_get(x_2, 0); +lean_inc(x_22); +x_23 = lean_array_get_size(x_22); +lean_dec(x_22); +x_24 = lean_ctor_get(x_2, 1); +lean_inc(x_24); +lean_inc(x_1); +x_25 = lean_apply_2(x_6, x_1, x_2); +x_26 = lean_ctor_get(x_25, 3); +lean_inc(x_26); +if (lean_obj_tag(x_26) == 0) +{ +lean_dec(x_24); +lean_dec(x_23); +lean_dec(x_4); +lean_dec(x_1); +return x_25; +} +else +{ +lean_object* x_27; lean_object* x_28; uint8_t x_29; +x_27 = lean_ctor_get(x_26, 0); +lean_inc(x_27); +lean_dec(x_26); +x_28 = lean_ctor_get(x_25, 1); +lean_inc(x_28); +x_29 = lean_nat_dec_eq(x_28, x_24); +lean_dec(x_28); +if (x_29 == 0) +{ +lean_dec(x_27); +lean_dec(x_24); +lean_dec(x_23); +lean_dec(x_4); +lean_dec(x_1); +return x_25; +} +else +{ +lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; +lean_inc(x_24); +x_30 = l_Lean_Parser_ParserState_restore(x_25, x_23, x_24); +lean_dec(x_23); +x_31 = lean_unsigned_to_nat(1024u); +x_32 = l_Lean_Parser_checkPrecFn(x_31, x_1, x_30); +x_33 = lean_ctor_get(x_32, 3); +lean_inc(x_33); +if (lean_obj_tag(x_33) == 0) +{ +lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; +x_34 = lean_ctor_get(x_32, 0); +lean_inc(x_34); +x_35 = lean_array_get_size(x_34); +lean_dec(x_34); +x_36 = l_Lean_Parser_Tactic_focus___elambda__1___closed__6; +x_37 = l_Lean_Parser_Tactic_focus___elambda__1___closed__8; +lean_inc(x_1); +x_38 = l_Lean_Parser_nonReservedSymbolFnAux(x_36, x_37, x_1, x_32); +x_39 = lean_ctor_get(x_38, 3); +lean_inc(x_39); +if (lean_obj_tag(x_39) == 0) +{ +lean_object* x_40; lean_object* x_41; lean_object* x_42; uint8_t x_43; lean_object* x_44; +x_40 = lean_apply_2(x_4, x_1, x_38); +x_41 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2; +x_42 = l_Lean_Parser_ParserState_mkNode(x_40, x_41, x_35); +x_43 = 1; +x_44 = l_Lean_Parser_mergeOrElseErrors(x_42, x_27, x_24, x_43); +lean_dec(x_24); +return x_44; +} +else +{ +lean_object* x_45; lean_object* x_46; uint8_t x_47; lean_object* x_48; +lean_dec(x_39); +lean_dec(x_4); +lean_dec(x_1); +x_45 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2; +x_46 = l_Lean_Parser_ParserState_mkNode(x_38, x_45, x_35); +x_47 = 1; +x_48 = l_Lean_Parser_mergeOrElseErrors(x_46, x_27, x_24, x_47); +lean_dec(x_24); +return x_48; +} +} +else +{ +uint8_t x_49; lean_object* x_50; +lean_dec(x_33); +lean_dec(x_4); +lean_dec(x_1); +x_49 = 1; +x_50 = l_Lean_Parser_mergeOrElseErrors(x_32, x_27, x_24, x_49); +lean_dec(x_24); +return x_50; +} +} +} +} +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___closed__1() { +_start: +{ +lean_object* x_1; uint8_t x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__6; +x_2 = 0; +x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_tacticSeq; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Tactic_focus___closed__1; +x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2; +x_2 = l_Lean_Parser_Tactic_focus___closed__2; +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_epsilonInfo; +x_2 = l_Lean_Parser_Tactic_focus___closed__3; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__4; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Tactic_focus___closed__4; +x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___closed__6() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_focus___elambda__1), 2, 0); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_focus___closed__5; +x_2 = l_Lean_Parser_Tactic_focus___closed__6; +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Parser_Tactic_focus___closed__7; +return x_1; +} +} +lean_object* l___regBuiltinParser_Lean_Parser_Tactic_focus(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2; +x_3 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2; +x_4 = 1; +x_5 = l_Lean_Parser_Tactic_focus; +x_6 = lean_unsigned_to_nat(0u); +x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1); +return x_7; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus_formatter___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; +x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__1; +x_2 = l_Lean_Parser_Tactic_focus___elambda__1___closed__3; +x_3 = 1; +x_4 = lean_box(x_3); +x_5 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot_formatter___boxed), 8, 3); +lean_closure_set(x_5, 0, x_1); +lean_closure_set(x_5, 1, x_2); +lean_closure_set(x_5, 2, x_4); +return x_5; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus_formatter___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__5; +x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_nonReservedSymbol_formatter___boxed), 6, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus_formatter___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_focus_formatter___closed__2; +x_2 = l_Lean_Parser_Term_byTactic_formatter___closed__3; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus_formatter___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2; +x_2 = lean_unsigned_to_nat(1024u); +x_3 = l_Lean_Parser_Tactic_focus_formatter___closed__3; +x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3); +lean_closure_set(x_4, 0, x_1); +lean_closure_set(x_4, 1, x_2); +lean_closure_set(x_4, 2, x_3); +return x_4; +} +} +lean_object* l_Lean_Parser_Tactic_focus_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_Tactic_focus_formatter___closed__1; +x_7 = l_Lean_Parser_Tactic_focus_formatter___closed__4; +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; +} +} +lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_focus_formatter___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_focus_formatter), 5, 0); +return x_1; +} +} +lean_object* l___regBuiltin_Lean_Parser_Tactic_focus_formatter(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_2 = l_Lean_PrettyPrinter_formatterAttribute; +x_3 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2; +x_4 = l___regBuiltin_Lean_Parser_Tactic_focus_formatter___closed__1; +x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); +return x_5; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus_parenthesizer___closed__1() { +_start: +{ +lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__3; +x_2 = 1; +x_3 = lean_box(x_2); +x_4 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot_parenthesizer___rarg___boxed), 7, 2); +lean_closure_set(x_4, 0, x_1); +lean_closure_set(x_4, 1, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Tactic_focus_parenthesizer___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2; +x_2 = lean_unsigned_to_nat(1024u); +x_3 = l_Lean_Parser_Tactic_allGoals_parenthesizer___closed__2; +x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3); +lean_closure_set(x_4, 0, x_1); +lean_closure_set(x_4, 1, x_2); +lean_closure_set(x_4, 2, x_3); +return x_4; +} +} +lean_object* l_Lean_Parser_Tactic_focus_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_Tactic_focus_parenthesizer___closed__1; +x_7 = l_Lean_Parser_Tactic_focus_parenthesizer___closed__2; +x_8 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5); +return x_8; +} +} +lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_focus_parenthesizer), 5, 0); +return x_1; +} +} +lean_object* l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_2 = l_Lean_PrettyPrinter_parenthesizerAttribute; +x_3 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2; +x_4 = l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer___closed__1; +x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); +return x_5; +} +} lean_object* _init_l_Lean_Parser_Tactic_skip___elambda__1___closed__1() { _start: { @@ -31402,6 +31904,63 @@ lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_allGoals_parenthesizer___ res = l___regBuiltin_Lean_Parser_Tactic_allGoals_parenthesizer(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l_Lean_Parser_Tactic_focus___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__1(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__1); +l_Lean_Parser_Tactic_focus___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__2); +l_Lean_Parser_Tactic_focus___elambda__1___closed__3 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__3); +l_Lean_Parser_Tactic_focus___elambda__1___closed__4 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__4(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__4); +l_Lean_Parser_Tactic_focus___elambda__1___closed__5 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__5(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__5); +l_Lean_Parser_Tactic_focus___elambda__1___closed__6 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__6(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__6); +l_Lean_Parser_Tactic_focus___elambda__1___closed__7 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__7(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__7); +l_Lean_Parser_Tactic_focus___elambda__1___closed__8 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__8(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__8); +l_Lean_Parser_Tactic_focus___closed__1 = _init_l_Lean_Parser_Tactic_focus___closed__1(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__1); +l_Lean_Parser_Tactic_focus___closed__2 = _init_l_Lean_Parser_Tactic_focus___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__2); +l_Lean_Parser_Tactic_focus___closed__3 = _init_l_Lean_Parser_Tactic_focus___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__3); +l_Lean_Parser_Tactic_focus___closed__4 = _init_l_Lean_Parser_Tactic_focus___closed__4(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__4); +l_Lean_Parser_Tactic_focus___closed__5 = _init_l_Lean_Parser_Tactic_focus___closed__5(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__5); +l_Lean_Parser_Tactic_focus___closed__6 = _init_l_Lean_Parser_Tactic_focus___closed__6(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__6); +l_Lean_Parser_Tactic_focus___closed__7 = _init_l_Lean_Parser_Tactic_focus___closed__7(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__7); +l_Lean_Parser_Tactic_focus = _init_l_Lean_Parser_Tactic_focus(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus); +res = l___regBuiltinParser_Lean_Parser_Tactic_focus(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +l_Lean_Parser_Tactic_focus_formatter___closed__1 = _init_l_Lean_Parser_Tactic_focus_formatter___closed__1(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus_formatter___closed__1); +l_Lean_Parser_Tactic_focus_formatter___closed__2 = _init_l_Lean_Parser_Tactic_focus_formatter___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus_formatter___closed__2); +l_Lean_Parser_Tactic_focus_formatter___closed__3 = _init_l_Lean_Parser_Tactic_focus_formatter___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus_formatter___closed__3); +l_Lean_Parser_Tactic_focus_formatter___closed__4 = _init_l_Lean_Parser_Tactic_focus_formatter___closed__4(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus_formatter___closed__4); +l___regBuiltin_Lean_Parser_Tactic_focus_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_focus_formatter___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_focus_formatter___closed__1); +res = l___regBuiltin_Lean_Parser_Tactic_focus_formatter(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +l_Lean_Parser_Tactic_focus_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_focus_parenthesizer___closed__1(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus_parenthesizer___closed__1); +l_Lean_Parser_Tactic_focus_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_focus_parenthesizer___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_focus_parenthesizer___closed__2); +l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer___closed__1); +res = l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l_Lean_Parser_Tactic_skip___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_skip___elambda__1___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_skip___elambda__1___closed__1); l_Lean_Parser_Tactic_skip___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_skip___elambda__1___closed__2();