From 524eca4d7ffefb3dbe92f844ccbc23b351172bcf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 26 Aug 2020 09:39:01 -0700 Subject: [PATCH] chore: udpate stage0 --- stage0/src/Lean/Parser/Term.lean | 1 + stage0/stdlib/Lean/Parser/Command.c | 139 +-- stage0/stdlib/Lean/Parser/Term.c | 1663 ++++++++++++++++++++++++++- 3 files changed, 1674 insertions(+), 129 deletions(-) diff --git a/stage0/src/Lean/Parser/Term.lean b/stage0/src/Lean/Parser/Term.lean index 5ca92dff68..912146d736 100644 --- a/stage0/src/Lean/Parser/Term.lean +++ b/stage0/src/Lean/Parser/Term.lean @@ -125,6 +125,7 @@ def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts fa def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (letIdDecl <|> letPatDecl <|> letEqnsDecl) @[builtinTermParser] def «let» := parser!:leadPrec "let " >> letDecl >> "; " >> termParser @[builtinTermParser] def «let!» := parser!:leadPrec "let! " >> letDecl >> "; " >> termParser +@[builtinTermParser] def «letrec» := parser!:leadPrec "letrec " >> optional ("partial ") >> letDecl >> many (", " >> letDecl) >> "; " >> termParser def leftArrow : Parser := unicodeSymbol " ← " " <- " def doLet := parser! "let ">> letDecl diff --git a/stage0/stdlib/Lean/Parser/Command.c b/stage0/stdlib/Lean/Parser/Command.c index 87d99d09e4..624bbeb780 100644 --- a/stage0/stdlib/Lean/Parser/Command.c +++ b/stage0/stdlib/Lean/Parser/Command.c @@ -205,7 +205,6 @@ lean_object* l_Lean_Parser_Command_declaration_formatter___closed__7; lean_object* l_Lean_Parser_Command_mutualElement_formatter___closed__1; lean_object* l_Lean_Parser_Command_mutual___closed__8; lean_object* l_Lean_Parser_Command_visibility_formatter___closed__2; -lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__7; lean_object* l_Lean_Parser_Command_export___closed__8; lean_object* l_Lean_Parser_Command_variables_formatter___closed__3; lean_object* l_Lean_Parser_Command_mutualElement___closed__5; @@ -260,6 +259,7 @@ lean_object* l_Lean_Parser_Command_ctor_parenthesizer___closed__5; lean_object* l_Lean_Parser_Command_declaration_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_extends___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_end_formatter___closed__3; +extern lean_object* l_Lean_Parser_Term_letrec_formatter___closed__3; lean_object* l_Lean_Parser_Command_ctor___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_open_formatter___closed__9; lean_object* l___regBuiltin_Lean_Parser_Command_universe_parenthesizer(lean_object*); @@ -583,7 +583,6 @@ lean_object* l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__1 lean_object* l_Lean_Parser_Command_openHiding_parenthesizer___closed__5; lean_object* l_Lean_Parser_Command_openHiding___closed__5; lean_object* l_Lean_Parser_Command_protected___elambda__1___closed__7; -lean_object* l_Lean_Parser_Command_partial_formatter___closed__3; lean_object* l___regBuiltin_Lean_Parser_Command_end_parenthesizer___closed__1; lean_object* l___regBuiltin_Lean_Parser_Command_variables_parenthesizer___closed__1; lean_object* l_Lean_Parser_Command_ctor_parenthesizer___closed__4; @@ -752,6 +751,7 @@ lean_object* l_Lean_Parser_Command_openSimple___closed__1; lean_object* l_Lean_Parser_Command_declaration___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_structInstBinder; lean_object* l_Lean_Parser_Command_attribute_parenthesizer___closed__3; +extern lean_object* l_Lean_Parser_Term_letrec___closed__2; lean_object* l_Lean_Parser_Command_structure_parenthesizer___closed__3; lean_object* l_Lean_Parser_manyAux___main(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_export_parenthesizer___closed__1; @@ -769,7 +769,6 @@ lean_object* l_Lean_Parser_Command_structure___closed__10; lean_object* l_Lean_Parser_Command_attrArg_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_attribute_formatter___closed__8; lean_object* l_Lean_Parser_nonReservedSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__6; lean_object* l_Lean_Parser_Command_declaration_parenthesizer___closed__4; lean_object* l_Lean_Parser_Command_structure_formatter___closed__1; lean_object* l_Lean_Parser_Command_declaration_formatter___closed__6; @@ -865,6 +864,7 @@ lean_object* l_Lean_Parser_Command_openHiding___elambda__1(lean_object*, lean_ob lean_object* l_Lean_Parser_Command_docComment___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_universe___elambda__1___closed__5; lean_object* l_Lean_Parser_Command_mutual_formatter___closed__5; +extern lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__11; lean_object* l_Lean_Parser_Command_openRenamingItem___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_def___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_example___closed__7; @@ -1210,7 +1210,6 @@ lean_object* l_Lean_Parser_Command_attributes___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_eval___closed__3; lean_object* l_Lean_Parser_Command_attributes_parenthesizer___closed__6; lean_object* l___regBuiltin_Lean_Parser_Command_variable_parenthesizer(lean_object*); -lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__8; lean_object* l___regBuiltin_Lean_Parser_Command_namespace_parenthesizer___closed__1; lean_object* l_Lean_Parser_Command_structure_parenthesizer___closed__12; lean_object* l_Lean_Parser_Command_noncomputable___elambda__1___closed__7; @@ -1495,7 +1494,6 @@ lean_object* l_Lean_Parser_Command_declModifiers_parenthesizer___closed__11; lean_object* l_Lean_Parser_Command_structImplicitBinder; lean_object* l_Lean_Parser_Command_openRenaming_formatter___closed__5; extern lean_object* l_Lean_Parser_Term_doPat_formatter___closed__4; -lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__5; lean_object* l_Lean_Parser_Command_set__option___closed__8; lean_object* l_Lean_Parser_Term_quot_parenthesizer___closed__5; lean_object* l_Lean_Parser_Command_export_parenthesizer___closed__5; @@ -1544,6 +1542,7 @@ lean_object* l_Lean_Parser_Command_structCtor___closed__5; lean_object* l_Lean_Parser_Command_docComment___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_open_formatter___closed__1; lean_object* l_Lean_Parser_Command_private___closed__4; +extern lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__8; lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_structure_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__5; @@ -1946,7 +1945,6 @@ lean_object* l_Lean_Parser_Command_structFields_parenthesizer(lean_object*, lean lean_object* l_Lean_Parser_Command_exit; lean_object* l_Lean_Parser_Command_namespace___closed__1; lean_object* l_Lean_Parser_Command_structFields_formatter___closed__4; -lean_object* l_Lean_Parser_Command_partial___closed__6; lean_object* l_Lean_Parser_Command_declaration_parenthesizer___closed__7; lean_object* l_Lean_Parser_Command_synth_parenthesizer___closed__2; lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__1; @@ -2199,7 +2197,6 @@ lean_object* l_Lean_Parser_Command_declModifiers_parenthesizer___closed__5; lean_object* l_Lean_Parser_Command_set__option___closed__6; lean_object* l_Lean_Parser_Command_variables_formatter___closed__1; lean_object* l_Lean_PrettyPrinter_Formatter_andthen_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__9; lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_structCtor___elambda__1___closed__6; extern lean_object* l_Lean_Parser_Term_optType_formatter___closed__1; @@ -6865,55 +6862,6 @@ x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_Command_partial___elambda__1___closed__5() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string("partial "); -return x_1; -} -} -lean_object* _init_l_Lean_Parser_Command_partial___elambda__1___closed__6() { -_start: -{ -lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__5; -x_2 = l_String_trim(x_1); -return x_2; -} -} -lean_object* _init_l_Lean_Parser_Command_partial___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_Command_partial___elambda__1___closed__6; -x_3 = lean_string_append(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Command_partial___elambda__1___closed__8() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_partial___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* _init_l_Lean_Parser_Command_partial___elambda__1___closed__9() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_partial___elambda__1___closed__8; -x_3 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_3, 0, x_2); -lean_ctor_set(x_3, 1, x_1); -return x_3; -} -} lean_object* l_Lean_Parser_Command_partial___elambda__1(lean_object* x_1, lean_object* x_2) { _start: { @@ -6957,13 +6905,13 @@ lean_object* x_16; lean_object* x_17; uint8_t x_18; x_16 = lean_ctor_get(x_15, 1); lean_inc(x_16); lean_dec(x_15); -x_17 = l_Lean_Parser_Command_partial___elambda__1___closed__6; +x_17 = l_Lean_Parser_Term_letrec___elambda__1___closed__8; x_18 = lean_string_dec_eq(x_16, x_17); lean_dec(x_16); if (x_18 == 0) { lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; -x_19 = l_Lean_Parser_Command_partial___elambda__1___closed__9; +x_19 = l_Lean_Parser_Term_letrec___elambda__1___closed__11; x_20 = l_Lean_Parser_ParserState_mkErrorsAt(x_12, x_19, x_11); x_21 = l_Lean_Parser_Command_partial___elambda__1___closed__2; x_22 = l_Lean_Parser_ParserState_mkNode(x_20, x_21, x_10); @@ -6982,7 +6930,7 @@ else { lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_dec(x_15); -x_25 = l_Lean_Parser_Command_partial___elambda__1___closed__9; +x_25 = l_Lean_Parser_Term_letrec___elambda__1___closed__11; x_26 = l_Lean_Parser_ParserState_mkErrorsAt(x_12, x_25, x_11); x_27 = l_Lean_Parser_Command_partial___elambda__1___closed__2; x_28 = l_Lean_Parser_ParserState_mkNode(x_26, x_27, x_10); @@ -6993,7 +6941,7 @@ else { lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_dec(x_13); -x_29 = l_Lean_Parser_Command_partial___elambda__1___closed__9; +x_29 = l_Lean_Parser_Term_letrec___elambda__1___closed__11; x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_12, x_29, x_11); x_31 = l_Lean_Parser_Command_partial___elambda__1___closed__2; x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_10); @@ -7080,13 +7028,13 @@ lean_object* x_52; lean_object* x_53; uint8_t x_54; x_52 = lean_ctor_get(x_51, 1); lean_inc(x_52); lean_dec(x_51); -x_53 = l_Lean_Parser_Command_partial___elambda__1___closed__6; +x_53 = l_Lean_Parser_Term_letrec___elambda__1___closed__8; x_54 = lean_string_dec_eq(x_52, x_53); lean_dec(x_52); if (x_54 == 0) { lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; -x_55 = l_Lean_Parser_Command_partial___elambda__1___closed__9; +x_55 = l_Lean_Parser_Term_letrec___elambda__1___closed__11; x_56 = l_Lean_Parser_ParserState_mkErrorsAt(x_48, x_55, x_47); x_57 = l_Lean_Parser_Command_partial___elambda__1___closed__2; x_58 = l_Lean_Parser_ParserState_mkNode(x_56, x_57, x_46); @@ -7109,7 +7057,7 @@ else { lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_dec(x_51); -x_63 = l_Lean_Parser_Command_partial___elambda__1___closed__9; +x_63 = l_Lean_Parser_Term_letrec___elambda__1___closed__11; x_64 = l_Lean_Parser_ParserState_mkErrorsAt(x_48, x_63, x_47); x_65 = l_Lean_Parser_Command_partial___elambda__1___closed__2; x_66 = l_Lean_Parser_ParserState_mkNode(x_64, x_65, x_46); @@ -7122,7 +7070,7 @@ else { lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_dec(x_49); -x_68 = l_Lean_Parser_Command_partial___elambda__1___closed__9; +x_68 = l_Lean_Parser_Term_letrec___elambda__1___closed__11; x_69 = l_Lean_Parser_ParserState_mkErrorsAt(x_48, x_68, x_47); x_70 = l_Lean_Parser_Command_partial___elambda__1___closed__2; x_71 = l_Lean_Parser_ParserState_mkNode(x_69, x_70, x_46); @@ -7148,45 +7096,36 @@ return x_73; lean_object* _init_l_Lean_Parser_Command_partial___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__6; -x_2 = l_Lean_Parser_symbolInfo(x_1); -return x_2; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__2; +x_2 = l_Lean_Parser_Term_letrec___closed__2; +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +return x_3; } } lean_object* _init_l_Lean_Parser_Command_partial___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__2; +x_1 = l_Lean_Parser_epsilonInfo; x_2 = l_Lean_Parser_Command_partial___closed__1; -x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } } lean_object* _init_l_Lean_Parser_Command_partial___closed__3() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_epsilonInfo; -x_2 = l_Lean_Parser_Command_partial___closed__2; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Command_partial___closed__4() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__4; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Command_partial___closed__3; +x_3 = l_Lean_Parser_Command_partial___closed__2; x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_Command_partial___closed__5() { +lean_object* _init_l_Lean_Parser_Command_partial___closed__4() { _start: { lean_object* x_1; @@ -7194,12 +7133,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_partial___elambda__1), 2, return x_1; } } -lean_object* _init_l_Lean_Parser_Command_partial___closed__6() { +lean_object* _init_l_Lean_Parser_Command_partial___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_partial___closed__4; -x_2 = l_Lean_Parser_Command_partial___closed__5; +x_1 = l_Lean_Parser_Command_partial___closed__3; +x_2 = l_Lean_Parser_Command_partial___closed__4; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -7210,7 +7149,7 @@ lean_object* _init_l_Lean_Parser_Command_partial() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Command_partial___closed__6; +x_1 = l_Lean_Parser_Command_partial___closed__5; return x_1; } } @@ -25826,20 +25765,10 @@ return x_5; lean_object* _init_l_Lean_Parser_Command_partial_formatter___closed__2() { _start: { -lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__5; -x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_symbol_formatter___boxed), 6, 1); -lean_closure_set(x_2, 0, x_1); -return x_2; -} -} -lean_object* _init_l_Lean_Parser_Command_partial_formatter___closed__3() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__2; x_2 = lean_unsigned_to_nat(1024u); -x_3 = l_Lean_Parser_Command_partial_formatter___closed__2; +x_3 = l_Lean_Parser_Term_letrec_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); @@ -25852,7 +25781,7 @@ _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; x_6 = l_Lean_Parser_Command_partial_formatter___closed__1; -x_7 = l_Lean_Parser_Command_partial_formatter___closed__3; +x_7 = l_Lean_Parser_Command_partial_formatter___closed__2; x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5); return x_8; } @@ -50610,16 +50539,6 @@ l_Lean_Parser_Command_partial___elambda__1___closed__3 = _init_l_Lean_Parser_Com lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__3); l_Lean_Parser_Command_partial___elambda__1___closed__4 = _init_l_Lean_Parser_Command_partial___elambda__1___closed__4(); lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__4); -l_Lean_Parser_Command_partial___elambda__1___closed__5 = _init_l_Lean_Parser_Command_partial___elambda__1___closed__5(); -lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__5); -l_Lean_Parser_Command_partial___elambda__1___closed__6 = _init_l_Lean_Parser_Command_partial___elambda__1___closed__6(); -lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__6); -l_Lean_Parser_Command_partial___elambda__1___closed__7 = _init_l_Lean_Parser_Command_partial___elambda__1___closed__7(); -lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__7); -l_Lean_Parser_Command_partial___elambda__1___closed__8 = _init_l_Lean_Parser_Command_partial___elambda__1___closed__8(); -lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__8); -l_Lean_Parser_Command_partial___elambda__1___closed__9 = _init_l_Lean_Parser_Command_partial___elambda__1___closed__9(); -lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__9); l_Lean_Parser_Command_partial___closed__1 = _init_l_Lean_Parser_Command_partial___closed__1(); lean_mark_persistent(l_Lean_Parser_Command_partial___closed__1); l_Lean_Parser_Command_partial___closed__2 = _init_l_Lean_Parser_Command_partial___closed__2(); @@ -50630,8 +50549,6 @@ l_Lean_Parser_Command_partial___closed__4 = _init_l_Lean_Parser_Command_partial_ lean_mark_persistent(l_Lean_Parser_Command_partial___closed__4); l_Lean_Parser_Command_partial___closed__5 = _init_l_Lean_Parser_Command_partial___closed__5(); lean_mark_persistent(l_Lean_Parser_Command_partial___closed__5); -l_Lean_Parser_Command_partial___closed__6 = _init_l_Lean_Parser_Command_partial___closed__6(); -lean_mark_persistent(l_Lean_Parser_Command_partial___closed__6); l_Lean_Parser_Command_partial = _init_l_Lean_Parser_Command_partial(); lean_mark_persistent(l_Lean_Parser_Command_partial); l_Lean_Parser_Command_declModifiers___elambda__1___closed__1 = _init_l_Lean_Parser_Command_declModifiers___elambda__1___closed__1(); @@ -51577,8 +51494,6 @@ l_Lean_Parser_Command_partial_formatter___closed__1 = _init_l_Lean_Parser_Comman lean_mark_persistent(l_Lean_Parser_Command_partial_formatter___closed__1); l_Lean_Parser_Command_partial_formatter___closed__2 = _init_l_Lean_Parser_Command_partial_formatter___closed__2(); lean_mark_persistent(l_Lean_Parser_Command_partial_formatter___closed__2); -l_Lean_Parser_Command_partial_formatter___closed__3 = _init_l_Lean_Parser_Command_partial_formatter___closed__3(); -lean_mark_persistent(l_Lean_Parser_Command_partial_formatter___closed__3); l_Lean_Parser_Command_declModifiers_formatter___closed__1 = _init_l_Lean_Parser_Command_declModifiers_formatter___closed__1(); lean_mark_persistent(l_Lean_Parser_Command_declModifiers_formatter___closed__1); l_Lean_Parser_Command_declModifiers_formatter___closed__2 = _init_l_Lean_Parser_Command_declModifiers_formatter___closed__2(); diff --git a/stage0/stdlib/Lean/Parser/Term.c b/stage0/stdlib/Lean/Parser/Term.c index 42db6a9a49..b024086682 100644 --- a/stage0/stdlib/Lean/Parser/Term.c +++ b/stage0/stdlib/Lean/Parser/Term.c @@ -45,6 +45,7 @@ lean_object* l_Lean_Parser_Level_quot___closed__3; lean_object* l_Lean_Parser_Term_uminus_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_not; lean_object* l_Lean_Parser_Term_where_formatter___closed__5; +lean_object* l_Lean_Parser_Term_letrec_formatter___closed__4; extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_term_parenthesizer___lambda__1___closed__2; lean_object* l_Lean_Parser_Term_paren_formatter___closed__5; lean_object* l_Lean_Parser_Term_letIdDecl; @@ -64,6 +65,7 @@ lean_object* l_Lean_Parser_Term_explicitUniv_parenthesizer___closed__2; lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_doPat_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Parser_Term_map_parenthesizer___closed__1; +lean_object* l_Lean_Parser_Term_letrec_parenthesizer___closed__2; lean_object* l___regBuiltinParser_Lean_Parser_Term_iff(lean_object*); lean_object* l_Lean_Parser_Term_matchAlts_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_matchDiscr___closed__4; @@ -100,6 +102,7 @@ lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__10; lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__9; lean_object* l_Lean_Parser_Term_or___closed__1; lean_object* l_Lean_Parser_Term_proj_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_letrec_formatter___closed__9; lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_listLit___elambda__1___spec__1(uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___closed__2; lean_object* l___regBuiltin_Lean_Parser_Term_or_formatter___closed__1; @@ -162,6 +165,7 @@ lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___closed__6; lean_object* l_Lean_Parser_Term_emptyC_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_band_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_regBuiltinTacticParserAttr___closed__1; +lean_object* l_Lean_Parser_Term_letrec_formatter___closed__7; lean_object* l_Lean_Parser_Term_borrowed___closed__4; lean_object* l_Lean_Parser_Term_explicitBinder_parenthesizer___closed__4; lean_object* l_Lean_Parser_Term_matchDiscr___closed__2; @@ -242,11 +246,13 @@ lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___closed__6; lean_object* l_Lean_Parser_Term_match__syntax_parenthesizer___closed__2; lean_object* l_Lean_Parser_Term_append_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_infixR_parenthesizer(lean_object*); +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__13; lean_object* l_Lean_Parser_Term_namedHole_formatter___closed__2; lean_object* l___regBuiltin_Lean_Parser_Term_where_formatter(lean_object*); lean_object* l_Lean_Parser_Term_inaccessible___closed__1; lean_object* l_Lean_Parser_Term_bindOp_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_matchAlts_formatter___lambda__1___closed__6; +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__6; lean_object* l_Lean_Parser_Term_parser_x21_formatter___closed__4; lean_object* l_Lean_Parser_Term_not___closed__6; lean_object* l_Lean_Parser_Term_funBinder_quot_formatter___closed__3; @@ -435,6 +441,7 @@ lean_object* l_Lean_Parser_Term_seqLeft___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_le_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Tactic_seq___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Tactic_seq___elambda__1___spec__1(uint8_t, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__2; lean_object* l___regBuiltin_Lean_Parser_Term_append_parenthesizer___closed__1; lean_object* l___regBuiltin_Lean_Parser_Term_explicit_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_hole___elambda__1(lean_object*, lean_object*); @@ -454,6 +461,7 @@ lean_object* l_Lean_Parser_Term_nativeRefl___closed__4; lean_object* l_Lean_Parser_Term_match___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_mul_formatter___closed__1; lean_object* l_Lean_Parser_Term_arrayRef_parenthesizer___closed__1; +lean_object* l_Lean_Parser_Term_letrec_formatter___closed__3; lean_object* l_Lean_Parser_Term_subst_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_type___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_doElem_parenthesizer___closed__3; @@ -461,6 +469,7 @@ lean_object* l_Lean_Parser_Term_letPatDecl___closed__2; lean_object* l_Lean_Parser_Term_where___elambda__1___closed__2; lean_object* l___regBuiltin_Lean_Parser_Term_subst_formatter(lean_object*); lean_object* l_Lean_Parser_Term_letPatDecl; +lean_object* l_Lean_Parser_Term_letrec_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_not_formatter___closed__3; lean_object* l_Lean_Parser_Term_listLit_formatter___closed__6; lean_object* l_Lean_Parser_Term_bnot___closed__2; @@ -493,6 +502,7 @@ lean_object* l_Lean_Parser_Term_fromTerm_parenthesizer___closed__2; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_match___elambda__1___closed__8; lean_object* l_Lean_Parser_Term_prod_formatter___closed__1; +lean_object* l_Lean_Parser_Term_letrec___closed__7; lean_object* l_Lean_Parser_Term_forall_formatter___closed__5; lean_object* l_Lean_Parser_Term_suffices_formatter___closed__7; lean_object* l_Lean_Parser_Term_binderTactic___closed__7; @@ -575,6 +585,7 @@ lean_object* l_Lean_Parser_Term_simpleBinder_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_bracketedBinder_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Level_quot_formatter___closed__2; lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__8; +lean_object* l_Lean_Parser_Term_letrec_formatter___closed__5; lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_beq___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_type_formatter___closed__6; @@ -692,12 +703,14 @@ lean_object* l_Lean_Parser_strLit_formatter___closed__1; lean_object* l_Lean_Parser_Term_let_formatter___closed__2; lean_object* l_Lean_Parser_Term_suffices_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__5; +lean_object* l___regBuiltinParser_Lean_Parser_Term_letrec(lean_object*); lean_object* l_Lean_Parser_Term_decide; lean_object* l___regBuiltin_Lean_Parser_Term_subst_formatter___closed__1; lean_object* l___regBuiltin_Lean_Parser_Term_nomatch_parenthesizer(lean_object*); lean_object* l_Lean_Parser_Term_listLit___closed__2; lean_object* l_Lean_Parser_Term_band___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_ParserState_mkTrailingNode(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letrec___elambda__1___spec__1(lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Parser_Term_gt_formatter___closed__1; lean_object* l_Lean_Parser_Term_seqRight___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_eq_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -985,6 +998,7 @@ lean_object* l_Lean_Parser_Term_anonymousCtor___closed__2; lean_object* l___regBuiltin_Lean_Parser_Term_app_formatter(lean_object*); lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_sort___elambda__1___closed__6; +lean_object* l_Lean_Parser_Term_letrec___closed__11; lean_object* l_Lean_Parser_Term_funBinder_quot___elambda__1___closed__10; lean_object* l_Lean_PrettyPrinter_Parenthesizer_unicodeSymbol_parenthesizer___boxed(lean_object*); lean_object* l_Lean_Parser_Term_match_parenthesizer___closed__9; @@ -1041,6 +1055,7 @@ lean_object* l_Lean_Parser_Term_bracketedDoSeq___closed__3; lean_object* l___regBuiltin_Lean_Parser_Term_sorry_formatter___closed__1; lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__14; lean_object* l_Lean_Parser_Term_doPat___closed__6; +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__9; lean_object* l_Lean_Parser_Term_match_parenthesizer___closed__4; lean_object* l_Lean_Parser_Term_borrowed_parenthesizer___closed__2; lean_object* l_Lean_Parser_Term_sorry___closed__4; @@ -1126,6 +1141,7 @@ lean_object* l_Lean_PrettyPrinter_Formatter_trailingNode_formatter(lean_object*, lean_object* l_Lean_Parser_Term_orM_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_listLit___closed__6; lean_object* l_Lean_Parser_Term_tparser_x21_parenthesizer___closed__1; +lean_object* l_Lean_Parser_Term_letrec_formatter___closed__6; lean_object* l_Lean_Parser_Term_doElem_parenthesizer___closed__2; lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_paren___closed__1; @@ -1145,6 +1161,7 @@ lean_object* l_Lean_Parser_Term_seqRight___closed__1; lean_object* l___regBuiltin_Lean_Parser_Term_seqLeft_formatter___closed__1; lean_object* l_Lean_Parser_Term_doElem___closed__3; lean_object* l_Lean_Parser_Term_if___closed__3; +lean_object* l_Lean_Parser_Term_letrec_parenthesizer___closed__5; lean_object* l_Lean_Parser_Term_matchAlts___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_byTactic___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__15; @@ -1261,6 +1278,7 @@ lean_object* l_Lean_Parser_Term_arrow___closed__4; lean_object* l_Lean_Parser_Term_arrayRef_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_have_parenthesizer___closed__8; lean_object* l_Lean_Parser_Term_namedArgument_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_letrec___closed__2; lean_object* l_Lean_Parser_Term_letIdLhs___closed__5; lean_object* l_Lean_Parser_Term_byTactic___elambda__1___closed__8; lean_object* l_Lean_Parser_Level_quot___elambda__1___closed__2; @@ -1321,6 +1339,7 @@ lean_object* l_Lean_Parser_Term_tupleTail___closed__1; lean_object* l_Lean_Parser_Term_not___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_le___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_not_formatter___closed__2; +lean_object* l___regBuiltin_Lean_Parser_Term_letrec_formatter(lean_object*); lean_object* l___regBuiltin_Lean_Parser_Term_tacticBlock_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_seq___closed__5; lean_object* l___regBuiltin_Lean_Parser_Term_suffices_parenthesizer(lean_object*); @@ -1347,6 +1366,7 @@ lean_object* l_Lean_Parser_Term_proj___closed__4; lean_object* l_Lean_Parser_Term_nativeRefl___closed__2; lean_object* l_Lean_Parser_Term_pow___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_char___closed__1; +lean_object* l_Lean_Parser_Term_letrec___closed__12; lean_object* l_Lean_Parser_Term_fun; lean_object* l_Lean_Parser_Term_byTactic___elambda__1___closed__4; lean_object* l_Lean_Parser_nodeInfo(lean_object*, lean_object*); @@ -1366,6 +1386,7 @@ lean_object* l_Lean_Parser_Term_subst_formatter___closed__2; lean_object* l_Lean_Parser_Tactic_seq___closed__3; lean_object* l_Lean_Parser_Term_let___closed__4; lean_object* l_Lean_Parser_strLit_parenthesizer___closed__1; +lean_object* l_Lean_Parser_Term_letrec_parenthesizer___closed__8; lean_object* l_Lean_Parser_Term_explicitBinder_formatter(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_bracketedBinder_parenthesizer___closed__1; lean_object* l_Lean_Parser_darrow_parenthesizer(lean_object*); @@ -1429,6 +1450,7 @@ lean_object* l_Lean_Parser_Term_where_parenthesizer(lean_object*, lean_object*, lean_object* l_Lean_Parser_Term_type_formatter___closed__4; lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__6; lean_object* l_Lean_Parser_Term_match_formatter___closed__9; +lean_object* l_Lean_Parser_Term_letrec_parenthesizer___closed__3; lean_object* l_Lean_Parser_Term_haveAssign_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_sorry___elambda__1___closed__8; lean_object* l___regBuiltin_Lean_Parser_Term_modN_parenthesizer(lean_object*); @@ -1485,6 +1507,7 @@ lean_object* l_Lean_Parser_Term_bracketedDoSeq___closed__4; lean_object* l_Lean_Parser_nodeWithAntiquot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Parser_Term_nomatch_parenthesizer___closed__1; +lean_object* l_Lean_Parser_Term_letrec___closed__8; lean_object* l_Lean_Parser_Tactic_quot_formatter___closed__5; lean_object* l_Lean_Parser_Term_binderIdent___closed__3; lean_object* l_Lean_Parser_Term_forall_formatter___closed__10; @@ -1513,9 +1536,11 @@ lean_object* l_Lean_Parser_Term_sorry___closed__3; lean_object* l_Lean_Parser_Term_instBinder___elambda__1___closed__2; lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_app___elambda__1___spec__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_explicitUniv_formatter___closed__6; +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__11; lean_object* l_Lean_Parser_Term_dollar_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_ge___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_structInstField___closed__2; +lean_object* l_Lean_Parser_Term_letrec_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_have; lean_object* l_Lean_Parser_Term_letIdLhs___closed__3; lean_object* l_Lean_Parser_Term_doPat___closed__11; @@ -1534,6 +1559,7 @@ lean_object* l_Lean_Parser_Term_anonymousCtor_formatter___closed__1; lean_object* l_Lean_Parser_Term_show___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_structInst_parenthesizer___closed__9; lean_object* l_Lean_Parser_Term_type___closed__7; +lean_object* l_Lean_Parser_Term_letrec_formatter___closed__10; lean_object* l_Lean_Parser_Term_arrayRef; lean_object* l_Lean_Parser_Term_cdot; lean_object* l___regBuiltin_Lean_Parser_Term_band_formatter___closed__1; @@ -1573,6 +1599,7 @@ lean_object* l_Lean_Parser_Term_structInst_formatter___closed__13; lean_object* l_Lean_Parser_Term_doLet___closed__3; lean_object* l_Lean_Parser_Term_seq___elambda__1___closed__2; lean_object* l___regBuiltin_Lean_Parser_Term_let_x21_parenthesizer___closed__1; +lean_object* l_Lean_Parser_Term_letrec___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_bnot___closed__5; lean_object* l_Lean_Parser_Term_structInstField___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_paren___closed__4; @@ -1675,7 +1702,6 @@ lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__3; lean_object* l_Lean_Parser_Term_emptyC___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_infixR_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_orelse___closed__1; -lean_object* l_Lean_Parser_Term_doLet_parenthesizer___closed__3; lean_object* l_Lean_Parser_Term_fun_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_type_parenthesizer___closed__6; lean_object* l_Lean_Parser_Term_structInstField_formatter___closed__2; @@ -1815,6 +1841,7 @@ lean_object* l_Lean_Parser_Term_structInstField_parenthesizer___closed__3; lean_object* l_Lean_Parser_Term_doElem___closed__1; lean_object* l_Lean_Parser_Term_let_x21___closed__7; lean_object* l___regBuiltin_Lean_Parser_Term_ne_parenthesizer___closed__1; +lean_object* l___regBuiltin_Lean_Parser_Term_letrec_parenthesizer(lean_object*); lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__13; lean_object* l_Lean_Parser_Term_structInst_parenthesizer___closed__11; lean_object* l_Lean_Parser_Term_ne___closed__1; @@ -1971,6 +1998,7 @@ lean_object* l_Lean_Parser_Term_proj___closed__3; lean_object* l___regBuiltin_Lean_Parser_Term_nativeDecide_formatter(lean_object*); lean_object* l_Lean_Parser_Term_uminus; lean_object* l_Lean_Parser_Term_funBinder_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_letrec_parenthesizer___closed__4; lean_object* l_Lean_Parser_Term_bracketedDoSeq_parenthesizer___closed__4; lean_object* l_Lean_Parser_Term_namedArgument; lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___closed__8; @@ -2083,6 +2111,7 @@ lean_object* l_Lean_Parser_Term_nomatch_formatter___closed__2; lean_object* l_Lean_Parser_Term_optExprPrecedence___closed__3; lean_object* l_Lean_Parser_Term_listLit_formatter___closed__3; lean_object* l_Lean_Parser_Term_proj___closed__2; +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__12; lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_iff___closed__4; lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*); @@ -2099,6 +2128,7 @@ lean_object* l_Lean_Parser_Term_dollar_formatter___closed__3; lean_object* l_Lean_Parser_Term_doElem_parenthesizer___closed__4; lean_object* l_Lean_Parser_Term_structInstField_formatter___closed__4; lean_object* l_Lean_Parser_Term_mod___closed__4; +lean_object* l___regBuiltin_Lean_Parser_Term_letrec_formatter___closed__1; lean_object* l_Lean_Parser_Term_arrow___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_explicit_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_explicit___closed__7; @@ -2136,6 +2166,7 @@ lean_object* l_Lean_Parser_Term_proj_parenthesizer___closed__3; lean_object* l_Lean_Parser_Term_subtype_parenthesizer___closed__4; lean_object* l_Lean_Parser_Term_tacticBlock___closed__2; lean_object* l_Lean_Parser_Term_bor___elambda__1___closed__1; +lean_object* l_Lean_Parser_Term_letrec___closed__1; lean_object* l_Lean_Parser_Term_letEqnsDecl___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_listLit___closed__7; lean_object* l_Lean_Parser_Term_listLit_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -2334,6 +2365,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_beq(lean_object*); lean_object* l_Lean_Parser_Term_borrowed_parenthesizer___closed__4; lean_object* l_Lean_Parser_Term_tparser_x21___closed__5; lean_object* l_Lean_Parser_Term_binderTactic___closed__4; +lean_object* l_Lean_Parser_Term_letrec___closed__4; lean_object* l_Lean_Parser_Term_structInstArrayRef_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_prop___closed__5; lean_object* l_Lean_Parser_Term_dollarProj___closed__5; @@ -2366,6 +2398,7 @@ lean_object* l_Lean_Parser_Term_letIdLhs___closed__2; lean_object* l_Lean_Parser_Term_doPat___closed__1; lean_object* l_Lean_Parser_Term_show___closed__3; lean_object* l_Lean_Parser_Term_le___elambda__1___closed__1; +lean_object* l_Lean_Parser_Term_letrec___closed__9; lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__10; lean_object* l_Lean_Parser_Term_cons___closed__1; extern lean_object* l_Lean_Parser_antiquotNestedExpr_formatter___closed__2; @@ -2386,6 +2419,7 @@ lean_object* l_Lean_Parser_Term_tupleTail_formatter___closed__5; lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__10; lean_object* l_Lean_Parser_Term_have_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__10; lean_object* l_Lean_Parser_Term_cdot_parenthesizer___closed__2; lean_object* l_Lean_Parser_Term_funBinder_quot_formatter___closed__1; lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -2567,6 +2601,8 @@ lean_object* l_Lean_Parser_Term_bindOp; lean_object* l_Lean_Parser_Term_doPat___closed__10; lean_object* l_Lean_Parser_Term_simpleBinder; lean_object* l_Lean_Parser_Term_bor___elambda__1___closed__3; +lean_object* l_Lean_Parser_Term_letrec___closed__3; +lean_object* l_Lean_Parser_Term_letrec_formatter___closed__11; lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__8(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_tparser_x21_parenthesizer___closed__2; lean_object* l_Lean_Parser_Term_band_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -2710,6 +2746,7 @@ lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser uint8_t lean_nat_dec_le(lean_object*, lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Term_subst(lean_object*); lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_match___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__8; lean_object* l_Lean_Parser_Term_anonymousCtor___closed__7; lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__6; lean_object* l_Lean_Parser_Term_andthen___closed__2; @@ -2730,6 +2767,7 @@ lean_object* l_Lean_Parser_Term_forall___closed__2; lean_object* l___regBuiltin_Lean_Parser_Term_dollar_formatter(lean_object*); lean_object* l_Lean_Parser_Term_inaccessible_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_doPat_formatter___closed__7; +lean_object* l_Lean_Parser_Term_letrec_parenthesizer___closed__6; lean_object* l_Lean_Parser_Term_do_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_num; lean_object* l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__2; @@ -2840,6 +2878,7 @@ lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__13; lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__6; lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_match___elambda__1___spec__2(uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Term_uminus(lean_object*); +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__1; lean_object* l___regBuiltin_Lean_Parser_Term_hole_parenthesizer(lean_object*); lean_object* l_Lean_Parser_Term_instBinder___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_funBinder_parenthesizer___closed__2; @@ -2858,6 +2897,7 @@ lean_object* l_Lean_Parser_Term_tparser_x21___closed__7; lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_sub___closed__3; lean_object* l_Lean_Parser_Term_typeSpec___closed__3; +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_iff___closed__1; lean_object* l_Lean_Parser_Term_orelse___closed__3; lean_object* l_Lean_Parser_Term_fun___closed__3; @@ -2927,6 +2967,7 @@ lean_object* l_Lean_Parser_Term_if___elambda__1___closed__8; lean_object* l_Lean_Parser_Term_forall_formatter___closed__3; lean_object* l_Lean_Parser_Term_letEqnsDecl___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_structInst_formatter___closed__5; +lean_object* l_Lean_Parser_Term_letrec___closed__5; lean_object* l_Lean_Parser_Term_instBinder_formatter___closed__2; lean_object* l_Lean_Parser_Term_let_formatter___closed__3; lean_object* l_Lean_Parser_Term_match_parenthesizer___closed__7; @@ -2957,6 +2998,7 @@ lean_object* l_Lean_Parser_Term_match___closed__8; lean_object* l_Lean_Parser_Term_mul___closed__3; lean_object* l___regBuiltinParser_Lean_Parser_Term_cons(lean_object*); lean_object* l_Lean_Parser_Term_forall___closed__8; +lean_object* l_Lean_Parser_Term_letrec___closed__14; lean_object* l_Lean_Parser_Term_fromTerm___closed__6; lean_object* l___regBuiltinParser_Lean_Parser_Term_namedHole(lean_object*); lean_object* l_Lean_Parser_Term_char_parenthesizer___closed__1; @@ -3032,6 +3074,7 @@ lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_if___closed__6; lean_object* l_Lean_Parser_Term_andM_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_namedHole_formatter___closed__3; +lean_object* l_Lean_Parser_Term_letrec___closed__13; lean_object* l_Lean_Parser_Term_implicitBinder_formatter___closed__2; lean_object* l_Lean_Parser_nameLit_formatter___closed__1; lean_object* l_Lean_Parser_Term_letIdDecl___closed__2; @@ -3117,6 +3160,7 @@ lean_object* l_Lean_Parser_Term_match__syntax_formatter___closed__5; lean_object* l_Lean_Parser_Term_if___closed__4; lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___closed__7; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_matchAlts___elambda__1___spec__17___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__3; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_matchAlts___elambda__1___spec__17(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_where_formatter___closed__3; @@ -3213,6 +3257,7 @@ lean_object* l_Lean_Parser_Term_nativeDecide_formatter___closed__3; lean_object* l_Lean_Parser_Term_bindOp_formatter___closed__1; lean_object* l_Lean_Parser_Term_structInst___closed__7; lean_object* l_Lean_Parser_Term_if_parenthesizer___closed__1; +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_structInst_formatter___closed__16; lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___closed__6; lean_object* l_Lean_Parser_Term_tacticBlock_formatter___closed__7; @@ -3435,6 +3480,7 @@ lean_object* l_Lean_Parser_Term_depArrow___elambda__1(lean_object*, lean_object* lean_object* l_Lean_Parser_Term_gt___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_doLet_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_typeSpec___elambda__1___closed__2; +lean_object* l_Lean_Parser_Term_letrec___closed__6; lean_object* l_Lean_Parser_Term_liftMethod; lean_object* l_Lean_PrettyPrinter_Formatter_symbol_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_explicitBinder_parenthesizer___closed__8; @@ -3492,6 +3538,7 @@ lean_object* l___regBuiltin_Lean_Parser_Term_fun_formatter___closed__1; lean_object* l_Lean_Parser_Term_if___elambda__1___closed__12; lean_object* l_Lean_Parser_Term_matchAlts___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_show_formatter___closed__2; +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__14; lean_object* l_Lean_Parser_Term_subst___closed__7; extern lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__1; lean_object* l_Lean_Parser_Term_haveAssign_formatter___closed__3; @@ -3519,6 +3566,7 @@ lean_object* l_Lean_Parser_Term_app___closed__2; lean_object* l_Lean_Parser_Term_namedArgument_parenthesizer___closed__5; lean_object* l___regBuiltin_Lean_Parser_Term_heq_formatter(lean_object*); lean_object* l_Lean_Parser_Term_explicit___closed__5; +lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_matchDiscr_parenthesizer___closed__6; lean_object* l_Lean_Parser_Term_do___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_have___closed__12; @@ -3673,6 +3721,7 @@ lean_object* l_Lean_Parser_Term_modN___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__9; lean_object* l_Lean_Parser_Term_subtype_formatter___closed__7; lean_object* l___regBuiltinParser_Lean_Parser_Term_or(lean_object*); +lean_object* l_Lean_Parser_Term_letrec_formatter___closed__2; lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_subst___elambda__1___spec__2___closed__4; lean_object* l_Lean_Parser_Term_iff___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_tacticBlock_formatter___closed__5; @@ -3704,6 +3753,7 @@ lean_object* l_Lean_Parser_Term_letDecl___closed__3; lean_object* l_Lean_Parser_Term_namedHole___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_subtype___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_tacticBlock___closed__5; +lean_object* l_Lean_Parser_Term_letrec_formatter___closed__1; lean_object* l_Lean_Parser_Term_if___closed__7; lean_object* l_Lean_Parser_Term_match___closed__10; lean_object* l_Lean_Parser_Term_match__syntax_formatter___closed__1; @@ -3776,6 +3826,7 @@ lean_object* l_Lean_Parser_Term_unicodeInfixR___elambda__1(lean_object*, lean_ob lean_object* l_Lean_Parser_Term_matchAlts_formatter___lambda__1___closed__1; lean_object* l_Lean_Parser_Term_funBinder_quot___elambda__1___closed__9; lean_object* l_Lean_Parser_Term_str_formatter___closed__1; +lean_object* l___regBuiltin_Lean_Parser_Term_letrec_parenthesizer___closed__1; lean_object* l___regBuiltin_Lean_Parser_Term_add_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_binderDefault___closed__5; @@ -3796,10 +3847,12 @@ lean_object* l___regBuiltin_Lean_Parser_Term_num_formatter(lean_object*); lean_object* l_Lean_Parser_Term_bnot_parenthesizer___closed__2; lean_object* l_Lean_Parser_Term_seq___closed__4; lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__12(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_letrec_parenthesizer___closed__7; lean_object* l___regBuiltin_Lean_Parser_Term_inaccessible_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__7; lean_object* l_Lean_Parser_Level_quot_parenthesizer___closed__5; lean_object* l_Lean_Parser_Term_funBinder_quot_parenthesizer___closed__2; +lean_object* l_Lean_Parser_Term_letrec___closed__10; lean_object* l___regBuiltin_Lean_Parser_Term_let_x21_formatter___closed__1; lean_object* l_Lean_Parser_Term_haveAssign_formatter___closed__2; lean_object* l_Lean_Parser_Term_paren_parenthesizer___closed__1; @@ -3882,6 +3935,7 @@ lean_object* l_Lean_Parser_Term_typeSpec___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_where_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__14; lean_object* l_Lean_Parser_Term_hole___closed__1; +lean_object* l_Lean_Parser_Term_letrec_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_type___closed__9; lean_object* l_Lean_Parser_Term_sub_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_fromTerm_formatter___closed__2; @@ -3912,6 +3966,7 @@ lean_object* l_Lean_Parser_Term_app___closed__3; lean_object* l_Lean_Parser_Term_tparser_x21; lean_object* l_Lean_Parser_Term_structInstLVal_formatter___closed__3; lean_object* l_Lean_Parser_Term_funBinder_quot_parenthesizer___closed__3; +lean_object* l_Lean_Parser_Term_letrec; lean_object* l_Lean_Parser_Term_fun_parenthesizer___closed__5; lean_object* l_Lean_Parser_Term_liftMethod_formatter___closed__1; uint8_t lean_nat_dec_lt(lean_object*, lean_object*); @@ -3926,6 +3981,7 @@ lean_object* l_Lean_Parser_Term_doId___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_explicitBinder_formatter___closed__5; lean_object* l_Lean_Parser_Term_namedArgument_formatter___closed__3; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_matchAlts___elambda__1___spec__7(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_letrec_formatter___closed__8; lean_object* l_Lean_Parser_Term_let_x21___closed__4; lean_object* l_Lean_Parser_Term_match_formatter___closed__5; lean_object* l_Lean_Parser_Term_doLet_formatter___closed__1; @@ -49100,6 +49156,1484 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } +lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letrec___elambda__1___spec__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; lean_object* x_7; lean_object* x_8; lean_object* x_24; lean_object* x_25; +x_3 = l_Lean_Parser_Term_letDecl; +x_4 = lean_ctor_get(x_3, 1); +lean_inc(x_4); +x_5 = lean_ctor_get(x_2, 0); +lean_inc(x_5); +x_6 = lean_array_get_size(x_5); +lean_dec(x_5); +x_7 = lean_ctor_get(x_2, 1); +lean_inc(x_7); +lean_inc(x_1); +x_24 = l_Lean_Parser_tokenFn(x_1, x_2); +x_25 = lean_ctor_get(x_24, 3); +lean_inc(x_25); +if (lean_obj_tag(x_25) == 0) +{ +lean_object* x_26; lean_object* x_27; +x_26 = lean_ctor_get(x_24, 0); +lean_inc(x_26); +x_27 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_26); +lean_dec(x_26); +if (lean_obj_tag(x_27) == 2) +{ +lean_object* x_28; lean_object* x_29; uint8_t x_30; +x_28 = lean_ctor_get(x_27, 1); +lean_inc(x_28); +lean_dec(x_27); +x_29 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_tupleTail___elambda__1___spec__2___closed__1; +x_30 = lean_string_dec_eq(x_28, x_29); +lean_dec(x_28); +if (x_30 == 0) +{ +lean_object* x_31; lean_object* x_32; +x_31 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_tupleTail___elambda__1___spec__2___closed__4; +lean_inc(x_7); +x_32 = l_Lean_Parser_ParserState_mkErrorsAt(x_24, x_31, x_7); +x_8 = x_32; +goto block_23; +} +else +{ +x_8 = x_24; +goto block_23; +} +} +else +{ +lean_object* x_33; lean_object* x_34; +lean_dec(x_27); +x_33 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_tupleTail___elambda__1___spec__2___closed__4; +lean_inc(x_7); +x_34 = l_Lean_Parser_ParserState_mkErrorsAt(x_24, x_33, x_7); +x_8 = x_34; +goto block_23; +} +} +else +{ +lean_object* x_35; lean_object* x_36; +lean_dec(x_25); +x_35 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_tupleTail___elambda__1___spec__2___closed__4; +lean_inc(x_7); +x_36 = l_Lean_Parser_ParserState_mkErrorsAt(x_24, x_35, x_7); +x_8 = x_36; +goto block_23; +} +block_23: +{ +lean_object* x_9; +x_9 = lean_ctor_get(x_8, 3); +lean_inc(x_9); +if (lean_obj_tag(x_9) == 0) +{ +lean_object* x_10; lean_object* x_11; +lean_inc(x_1); +x_10 = lean_apply_2(x_4, x_1, x_8); +x_11 = lean_ctor_get(x_10, 3); +lean_inc(x_11); +if (lean_obj_tag(x_11) == 0) +{ +lean_object* x_12; uint8_t x_13; +lean_dec(x_6); +x_12 = lean_ctor_get(x_10, 1); +lean_inc(x_12); +x_13 = lean_nat_dec_eq(x_7, x_12); +lean_dec(x_12); +lean_dec(x_7); +if (x_13 == 0) +{ +x_2 = x_10; +goto _start; +} +else +{ +lean_object* x_15; lean_object* x_16; +lean_dec(x_1); +x_15 = l_Lean_Parser_manyAux___main___closed__1; +x_16 = l_Lean_Parser_ParserState_mkUnexpectedError(x_10, x_15); +return x_16; +} +} +else +{ +lean_object* x_17; uint8_t x_18; +lean_dec(x_11); +lean_dec(x_1); +x_17 = lean_ctor_get(x_10, 1); +lean_inc(x_17); +x_18 = lean_nat_dec_eq(x_7, x_17); +lean_dec(x_17); +if (x_18 == 0) +{ +lean_dec(x_7); +lean_dec(x_6); +return x_10; +} +else +{ +lean_object* x_19; +x_19 = l_Lean_Parser_ParserState_restore(x_10, x_6, x_7); +lean_dec(x_6); +return x_19; +} +} +} +else +{ +lean_object* x_20; uint8_t x_21; +lean_dec(x_9); +lean_dec(x_4); +lean_dec(x_1); +x_20 = lean_ctor_get(x_8, 1); +lean_inc(x_20); +x_21 = lean_nat_dec_eq(x_7, x_20); +lean_dec(x_20); +if (x_21 == 0) +{ +lean_dec(x_7); +lean_dec(x_6); +return x_8; +} +else +{ +lean_object* x_22; +x_22 = l_Lean_Parser_ParserState_restore(x_8, x_6, x_7); +lean_dec(x_6); +return x_22; +} +} +} +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___elambda__1___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("letrec"); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___elambda__1___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_mkAppStx___closed__6; +x_2 = l_Lean_Parser_Term_letrec___elambda__1___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___elambda__1___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_letrec___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_Term_letrec___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_Term_letrec___elambda__1___closed__1; +x_2 = l_Lean_Parser_Term_letrec___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_Term_letrec___elambda__1___closed__5() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("letrec "); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___elambda__1___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_letrec___elambda__1___closed__5; +x_2 = l_String_trim(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___elambda__1___closed__7() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("partial "); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___elambda__1___closed__8() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_letrec___elambda__1___closed__7; +x_2 = l_String_trim(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___elambda__1___closed__9() { +_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_Term_letrec___elambda__1___closed__8; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___elambda__1___closed__10() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_letrec___elambda__1___closed__9; +x_2 = l_Char_HasRepr___closed__1; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___elambda__1___closed__11() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Parser_Term_letrec___elambda__1___closed__10; +x_3 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_3, 0, x_2); +lean_ctor_set(x_3, 1, x_1); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___elambda__1___closed__12() { +_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_Term_letrec___elambda__1___closed__6; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___elambda__1___closed__13() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_letrec___elambda__1___closed__12; +x_2 = l_Char_HasRepr___closed__1; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___elambda__1___closed__14() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Parser_Term_letrec___elambda__1___closed__13; +x_3 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_3, 0, x_2); +lean_ctor_set(x_3, 1, x_1); +return x_3; +} +} +lean_object* l_Lean_Parser_Term_letrec___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_Term_letDecl; +x_4 = lean_ctor_get(x_3, 1); +lean_inc(x_4); +x_5 = l_Lean_Parser_Term_letrec___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 = l_Lean_Parser_Term_leadPrec; +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_55; lean_object* x_88; lean_object* x_89; lean_object* x_90; +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_88 = lean_ctor_get(x_9, 1); +lean_inc(x_88); +lean_inc(x_1); +x_89 = l_Lean_Parser_tokenFn(x_1, x_9); +x_90 = lean_ctor_get(x_89, 3); +lean_inc(x_90); +if (lean_obj_tag(x_90) == 0) +{ +lean_object* x_91; lean_object* x_92; +x_91 = lean_ctor_get(x_89, 0); +lean_inc(x_91); +x_92 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_91); +lean_dec(x_91); +if (lean_obj_tag(x_92) == 2) +{ +lean_object* x_93; lean_object* x_94; uint8_t x_95; +x_93 = lean_ctor_get(x_92, 1); +lean_inc(x_93); +lean_dec(x_92); +x_94 = l_Lean_Parser_Term_letrec___elambda__1___closed__6; +x_95 = lean_string_dec_eq(x_93, x_94); +lean_dec(x_93); +if (x_95 == 0) +{ +lean_object* x_96; lean_object* x_97; +x_96 = l_Lean_Parser_Term_letrec___elambda__1___closed__14; +x_97 = l_Lean_Parser_ParserState_mkErrorsAt(x_89, x_96, x_88); +x_55 = x_97; +goto block_87; +} +else +{ +lean_dec(x_88); +x_55 = x_89; +goto block_87; +} +} +else +{ +lean_object* x_98; lean_object* x_99; +lean_dec(x_92); +x_98 = l_Lean_Parser_Term_letrec___elambda__1___closed__14; +x_99 = l_Lean_Parser_ParserState_mkErrorsAt(x_89, x_98, x_88); +x_55 = x_99; +goto block_87; +} +} +else +{ +lean_object* x_100; lean_object* x_101; +lean_dec(x_90); +x_100 = l_Lean_Parser_Term_letrec___elambda__1___closed__14; +x_101 = l_Lean_Parser_ParserState_mkErrorsAt(x_89, x_100, x_88); +x_55 = x_101; +goto block_87; +} +block_54: +{ +lean_object* x_14; +x_14 = lean_ctor_get(x_13, 3); +lean_inc(x_14); +if (lean_obj_tag(x_14) == 0) +{ +lean_object* x_15; lean_object* x_16; +lean_inc(x_1); +x_15 = lean_apply_2(x_4, x_1, x_13); +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; lean_object* x_20; lean_object* x_21; lean_object* x_22; +x_17 = lean_ctor_get(x_15, 0); +lean_inc(x_17); +x_18 = lean_array_get_size(x_17); +lean_dec(x_17); +lean_inc(x_1); +x_19 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letrec___elambda__1___spec__1(x_1, x_15); +x_20 = l_Lean_nullKind; +x_21 = l_Lean_Parser_ParserState_mkNode(x_19, x_20, x_18); +x_22 = lean_ctor_get(x_21, 3); +lean_inc(x_22); +if (lean_obj_tag(x_22) == 0) +{ +lean_object* x_23; lean_object* x_24; lean_object* x_25; +x_23 = lean_ctor_get(x_21, 1); +lean_inc(x_23); +lean_inc(x_1); +x_24 = l_Lean_Parser_tokenFn(x_1, x_21); +x_25 = lean_ctor_get(x_24, 3); +lean_inc(x_25); +if (lean_obj_tag(x_25) == 0) +{ +lean_object* x_26; lean_object* x_27; +x_26 = lean_ctor_get(x_24, 0); +lean_inc(x_26); +x_27 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_26); +lean_dec(x_26); +if (lean_obj_tag(x_27) == 2) +{ +lean_object* x_28; lean_object* x_29; uint8_t x_30; +x_28 = lean_ctor_get(x_27, 1); +lean_inc(x_28); +lean_dec(x_27); +x_29 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__1; +x_30 = lean_string_dec_eq(x_28, x_29); +lean_dec(x_28); +if (x_30 == 0) +{ +lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; +lean_dec(x_1); +x_31 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4; +x_32 = l_Lean_Parser_ParserState_mkErrorsAt(x_24, x_31, x_23); +x_33 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_34 = l_Lean_Parser_ParserState_mkNode(x_32, x_33, x_12); +return x_34; +} +else +{ +lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; +lean_dec(x_23); +x_35 = l_Lean_Parser_termParser___closed__2; +x_36 = lean_unsigned_to_nat(0u); +x_37 = l_Lean_Parser_categoryParser___elambda__1(x_35, x_36, x_1, x_24); +x_38 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_39 = l_Lean_Parser_ParserState_mkNode(x_37, x_38, x_12); +return x_39; +} +} +else +{ +lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; +lean_dec(x_27); +lean_dec(x_1); +x_40 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4; +x_41 = l_Lean_Parser_ParserState_mkErrorsAt(x_24, x_40, x_23); +x_42 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_43 = l_Lean_Parser_ParserState_mkNode(x_41, x_42, x_12); +return x_43; +} +} +else +{ +lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; +lean_dec(x_25); +lean_dec(x_1); +x_44 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4; +x_45 = l_Lean_Parser_ParserState_mkErrorsAt(x_24, x_44, x_23); +x_46 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_47 = l_Lean_Parser_ParserState_mkNode(x_45, x_46, x_12); +return x_47; +} +} +else +{ +lean_object* x_48; lean_object* x_49; +lean_dec(x_22); +lean_dec(x_1); +x_48 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_49 = l_Lean_Parser_ParserState_mkNode(x_21, x_48, x_12); +return x_49; +} +} +else +{ +lean_object* x_50; lean_object* x_51; +lean_dec(x_16); +lean_dec(x_1); +x_50 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_51 = l_Lean_Parser_ParserState_mkNode(x_15, x_50, x_12); +return x_51; +} +} +else +{ +lean_object* x_52; lean_object* x_53; +lean_dec(x_14); +lean_dec(x_4); +lean_dec(x_1); +x_52 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_53 = l_Lean_Parser_ParserState_mkNode(x_13, x_52, x_12); +return x_53; +} +} +block_87: +{ +lean_object* x_56; +x_56 = lean_ctor_get(x_55, 3); +lean_inc(x_56); +if (lean_obj_tag(x_56) == 0) +{ +lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_72; lean_object* x_73; +x_57 = lean_ctor_get(x_55, 0); +lean_inc(x_57); +x_58 = lean_array_get_size(x_57); +lean_dec(x_57); +x_59 = lean_ctor_get(x_55, 1); +lean_inc(x_59); +lean_inc(x_1); +x_72 = l_Lean_Parser_tokenFn(x_1, x_55); +x_73 = lean_ctor_get(x_72, 3); +lean_inc(x_73); +if (lean_obj_tag(x_73) == 0) +{ +lean_object* x_74; lean_object* x_75; +x_74 = lean_ctor_get(x_72, 0); +lean_inc(x_74); +x_75 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_74); +lean_dec(x_74); +if (lean_obj_tag(x_75) == 2) +{ +lean_object* x_76; lean_object* x_77; uint8_t x_78; +x_76 = lean_ctor_get(x_75, 1); +lean_inc(x_76); +lean_dec(x_75); +x_77 = l_Lean_Parser_Term_letrec___elambda__1___closed__8; +x_78 = lean_string_dec_eq(x_76, x_77); +lean_dec(x_76); +if (x_78 == 0) +{ +lean_object* x_79; lean_object* x_80; +x_79 = l_Lean_Parser_Term_letrec___elambda__1___closed__11; +lean_inc(x_59); +x_80 = l_Lean_Parser_ParserState_mkErrorsAt(x_72, x_79, x_59); +x_60 = x_80; +goto block_71; +} +else +{ +x_60 = x_72; +goto block_71; +} +} +else +{ +lean_object* x_81; lean_object* x_82; +lean_dec(x_75); +x_81 = l_Lean_Parser_Term_letrec___elambda__1___closed__11; +lean_inc(x_59); +x_82 = l_Lean_Parser_ParserState_mkErrorsAt(x_72, x_81, x_59); +x_60 = x_82; +goto block_71; +} +} +else +{ +lean_object* x_83; lean_object* x_84; +lean_dec(x_73); +x_83 = l_Lean_Parser_Term_letrec___elambda__1___closed__11; +lean_inc(x_59); +x_84 = l_Lean_Parser_ParserState_mkErrorsAt(x_72, x_83, x_59); +x_60 = x_84; +goto block_71; +} +block_71: +{ +lean_object* x_61; +x_61 = lean_ctor_get(x_60, 3); +lean_inc(x_61); +if (lean_obj_tag(x_61) == 0) +{ +lean_object* x_62; lean_object* x_63; +lean_dec(x_59); +x_62 = l_Lean_nullKind; +x_63 = l_Lean_Parser_ParserState_mkNode(x_60, x_62, x_58); +x_13 = x_63; +goto block_54; +} +else +{ +lean_object* x_64; uint8_t x_65; +lean_dec(x_61); +x_64 = lean_ctor_get(x_60, 1); +lean_inc(x_64); +x_65 = lean_nat_dec_eq(x_64, x_59); +lean_dec(x_64); +if (x_65 == 0) +{ +lean_object* x_66; lean_object* x_67; +lean_dec(x_59); +x_66 = l_Lean_nullKind; +x_67 = l_Lean_Parser_ParserState_mkNode(x_60, x_66, x_58); +x_13 = x_67; +goto block_54; +} +else +{ +lean_object* x_68; lean_object* x_69; lean_object* x_70; +x_68 = l_Lean_Parser_ParserState_restore(x_60, x_58, x_59); +x_69 = l_Lean_nullKind; +x_70 = l_Lean_Parser_ParserState_mkNode(x_68, x_69, x_58); +x_13 = x_70; +goto block_54; +} +} +} +} +else +{ +lean_object* x_85; lean_object* x_86; +lean_dec(x_56); +lean_dec(x_4); +lean_dec(x_1); +x_85 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_86 = l_Lean_Parser_ParserState_mkNode(x_55, x_85, x_12); +return x_86; +} +} +} +else +{ +lean_dec(x_10); +lean_dec(x_4); +lean_dec(x_1); +return x_9; +} +} +else +{ +lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; +x_102 = lean_ctor_get(x_2, 0); +lean_inc(x_102); +x_103 = lean_array_get_size(x_102); +lean_dec(x_102); +x_104 = lean_ctor_get(x_2, 1); +lean_inc(x_104); +lean_inc(x_1); +x_105 = lean_apply_2(x_6, x_1, x_2); +x_106 = lean_ctor_get(x_105, 3); +lean_inc(x_106); +if (lean_obj_tag(x_106) == 0) +{ +lean_dec(x_104); +lean_dec(x_103); +lean_dec(x_4); +lean_dec(x_1); +return x_105; +} +else +{ +lean_object* x_107; lean_object* x_108; uint8_t x_109; +x_107 = lean_ctor_get(x_106, 0); +lean_inc(x_107); +lean_dec(x_106); +x_108 = lean_ctor_get(x_105, 1); +lean_inc(x_108); +x_109 = lean_nat_dec_eq(x_108, x_104); +lean_dec(x_108); +if (x_109 == 0) +{ +lean_dec(x_107); +lean_dec(x_104); +lean_dec(x_103); +lean_dec(x_4); +lean_dec(x_1); +return x_105; +} +else +{ +lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; +lean_inc(x_104); +x_110 = l_Lean_Parser_ParserState_restore(x_105, x_103, x_104); +lean_dec(x_103); +x_111 = l_Lean_Parser_Term_leadPrec; +x_112 = l_Lean_Parser_checkPrecFn(x_111, x_1, x_110); +x_113 = lean_ctor_get(x_112, 3); +lean_inc(x_113); +if (lean_obj_tag(x_113) == 0) +{ +lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_165; lean_object* x_199; lean_object* x_200; lean_object* x_201; +x_114 = lean_ctor_get(x_112, 0); +lean_inc(x_114); +x_115 = lean_array_get_size(x_114); +lean_dec(x_114); +x_199 = lean_ctor_get(x_112, 1); +lean_inc(x_199); +lean_inc(x_1); +x_200 = l_Lean_Parser_tokenFn(x_1, x_112); +x_201 = lean_ctor_get(x_200, 3); +lean_inc(x_201); +if (lean_obj_tag(x_201) == 0) +{ +lean_object* x_202; lean_object* x_203; +x_202 = lean_ctor_get(x_200, 0); +lean_inc(x_202); +x_203 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_202); +lean_dec(x_202); +if (lean_obj_tag(x_203) == 2) +{ +lean_object* x_204; lean_object* x_205; uint8_t x_206; +x_204 = lean_ctor_get(x_203, 1); +lean_inc(x_204); +lean_dec(x_203); +x_205 = l_Lean_Parser_Term_letrec___elambda__1___closed__6; +x_206 = lean_string_dec_eq(x_204, x_205); +lean_dec(x_204); +if (x_206 == 0) +{ +lean_object* x_207; lean_object* x_208; +x_207 = l_Lean_Parser_Term_letrec___elambda__1___closed__14; +x_208 = l_Lean_Parser_ParserState_mkErrorsAt(x_200, x_207, x_199); +x_165 = x_208; +goto block_198; +} +else +{ +lean_dec(x_199); +x_165 = x_200; +goto block_198; +} +} +else +{ +lean_object* x_209; lean_object* x_210; +lean_dec(x_203); +x_209 = l_Lean_Parser_Term_letrec___elambda__1___closed__14; +x_210 = l_Lean_Parser_ParserState_mkErrorsAt(x_200, x_209, x_199); +x_165 = x_210; +goto block_198; +} +} +else +{ +lean_object* x_211; lean_object* x_212; +lean_dec(x_201); +x_211 = l_Lean_Parser_Term_letrec___elambda__1___closed__14; +x_212 = l_Lean_Parser_ParserState_mkErrorsAt(x_200, x_211, x_199); +x_165 = x_212; +goto block_198; +} +block_164: +{ +lean_object* x_117; +x_117 = lean_ctor_get(x_116, 3); +lean_inc(x_117); +if (lean_obj_tag(x_117) == 0) +{ +lean_object* x_118; lean_object* x_119; +lean_inc(x_1); +x_118 = lean_apply_2(x_4, x_1, x_116); +x_119 = lean_ctor_get(x_118, 3); +lean_inc(x_119); +if (lean_obj_tag(x_119) == 0) +{ +lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; +x_120 = lean_ctor_get(x_118, 0); +lean_inc(x_120); +x_121 = lean_array_get_size(x_120); +lean_dec(x_120); +lean_inc(x_1); +x_122 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letrec___elambda__1___spec__1(x_1, x_118); +x_123 = l_Lean_nullKind; +x_124 = l_Lean_Parser_ParserState_mkNode(x_122, x_123, x_121); +x_125 = lean_ctor_get(x_124, 3); +lean_inc(x_125); +if (lean_obj_tag(x_125) == 0) +{ +lean_object* x_126; lean_object* x_127; lean_object* x_128; +x_126 = lean_ctor_get(x_124, 1); +lean_inc(x_126); +lean_inc(x_1); +x_127 = l_Lean_Parser_tokenFn(x_1, x_124); +x_128 = lean_ctor_get(x_127, 3); +lean_inc(x_128); +if (lean_obj_tag(x_128) == 0) +{ +lean_object* x_129; lean_object* x_130; +x_129 = lean_ctor_get(x_127, 0); +lean_inc(x_129); +x_130 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_129); +lean_dec(x_129); +if (lean_obj_tag(x_130) == 2) +{ +lean_object* x_131; lean_object* x_132; uint8_t x_133; +x_131 = lean_ctor_get(x_130, 1); +lean_inc(x_131); +lean_dec(x_130); +x_132 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__1; +x_133 = lean_string_dec_eq(x_131, x_132); +lean_dec(x_131); +if (x_133 == 0) +{ +lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; +lean_dec(x_1); +x_134 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4; +x_135 = l_Lean_Parser_ParserState_mkErrorsAt(x_127, x_134, x_126); +x_136 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_137 = l_Lean_Parser_ParserState_mkNode(x_135, x_136, x_115); +x_138 = l_Lean_Parser_mergeOrElseErrors(x_137, x_107, x_104); +lean_dec(x_104); +return x_138; +} +else +{ +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_dec(x_126); +x_139 = l_Lean_Parser_termParser___closed__2; +x_140 = lean_unsigned_to_nat(0u); +x_141 = l_Lean_Parser_categoryParser___elambda__1(x_139, x_140, x_1, x_127); +x_142 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_143 = l_Lean_Parser_ParserState_mkNode(x_141, x_142, x_115); +x_144 = l_Lean_Parser_mergeOrElseErrors(x_143, x_107, x_104); +lean_dec(x_104); +return x_144; +} +} +else +{ +lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; +lean_dec(x_130); +lean_dec(x_1); +x_145 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4; +x_146 = l_Lean_Parser_ParserState_mkErrorsAt(x_127, x_145, x_126); +x_147 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_148 = l_Lean_Parser_ParserState_mkNode(x_146, x_147, x_115); +x_149 = l_Lean_Parser_mergeOrElseErrors(x_148, x_107, x_104); +lean_dec(x_104); +return x_149; +} +} +else +{ +lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; +lean_dec(x_128); +lean_dec(x_1); +x_150 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4; +x_151 = l_Lean_Parser_ParserState_mkErrorsAt(x_127, x_150, x_126); +x_152 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_153 = l_Lean_Parser_ParserState_mkNode(x_151, x_152, x_115); +x_154 = l_Lean_Parser_mergeOrElseErrors(x_153, x_107, x_104); +lean_dec(x_104); +return x_154; +} +} +else +{ +lean_object* x_155; lean_object* x_156; lean_object* x_157; +lean_dec(x_125); +lean_dec(x_1); +x_155 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_156 = l_Lean_Parser_ParserState_mkNode(x_124, x_155, x_115); +x_157 = l_Lean_Parser_mergeOrElseErrors(x_156, x_107, x_104); +lean_dec(x_104); +return x_157; +} +} +else +{ +lean_object* x_158; lean_object* x_159; lean_object* x_160; +lean_dec(x_119); +lean_dec(x_1); +x_158 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_159 = l_Lean_Parser_ParserState_mkNode(x_118, x_158, x_115); +x_160 = l_Lean_Parser_mergeOrElseErrors(x_159, x_107, x_104); +lean_dec(x_104); +return x_160; +} +} +else +{ +lean_object* x_161; lean_object* x_162; lean_object* x_163; +lean_dec(x_117); +lean_dec(x_4); +lean_dec(x_1); +x_161 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_162 = l_Lean_Parser_ParserState_mkNode(x_116, x_161, x_115); +x_163 = l_Lean_Parser_mergeOrElseErrors(x_162, x_107, x_104); +lean_dec(x_104); +return x_163; +} +} +block_198: +{ +lean_object* x_166; +x_166 = lean_ctor_get(x_165, 3); +lean_inc(x_166); +if (lean_obj_tag(x_166) == 0) +{ +lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_182; lean_object* x_183; +x_167 = lean_ctor_get(x_165, 0); +lean_inc(x_167); +x_168 = lean_array_get_size(x_167); +lean_dec(x_167); +x_169 = lean_ctor_get(x_165, 1); +lean_inc(x_169); +lean_inc(x_1); +x_182 = l_Lean_Parser_tokenFn(x_1, x_165); +x_183 = lean_ctor_get(x_182, 3); +lean_inc(x_183); +if (lean_obj_tag(x_183) == 0) +{ +lean_object* x_184; lean_object* x_185; +x_184 = lean_ctor_get(x_182, 0); +lean_inc(x_184); +x_185 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_184); +lean_dec(x_184); +if (lean_obj_tag(x_185) == 2) +{ +lean_object* x_186; lean_object* x_187; uint8_t x_188; +x_186 = lean_ctor_get(x_185, 1); +lean_inc(x_186); +lean_dec(x_185); +x_187 = l_Lean_Parser_Term_letrec___elambda__1___closed__8; +x_188 = lean_string_dec_eq(x_186, x_187); +lean_dec(x_186); +if (x_188 == 0) +{ +lean_object* x_189; lean_object* x_190; +x_189 = l_Lean_Parser_Term_letrec___elambda__1___closed__11; +lean_inc(x_169); +x_190 = l_Lean_Parser_ParserState_mkErrorsAt(x_182, x_189, x_169); +x_170 = x_190; +goto block_181; +} +else +{ +x_170 = x_182; +goto block_181; +} +} +else +{ +lean_object* x_191; lean_object* x_192; +lean_dec(x_185); +x_191 = l_Lean_Parser_Term_letrec___elambda__1___closed__11; +lean_inc(x_169); +x_192 = l_Lean_Parser_ParserState_mkErrorsAt(x_182, x_191, x_169); +x_170 = x_192; +goto block_181; +} +} +else +{ +lean_object* x_193; lean_object* x_194; +lean_dec(x_183); +x_193 = l_Lean_Parser_Term_letrec___elambda__1___closed__11; +lean_inc(x_169); +x_194 = l_Lean_Parser_ParserState_mkErrorsAt(x_182, x_193, x_169); +x_170 = x_194; +goto block_181; +} +block_181: +{ +lean_object* x_171; +x_171 = lean_ctor_get(x_170, 3); +lean_inc(x_171); +if (lean_obj_tag(x_171) == 0) +{ +lean_object* x_172; lean_object* x_173; +lean_dec(x_169); +x_172 = l_Lean_nullKind; +x_173 = l_Lean_Parser_ParserState_mkNode(x_170, x_172, x_168); +x_116 = x_173; +goto block_164; +} +else +{ +lean_object* x_174; uint8_t x_175; +lean_dec(x_171); +x_174 = lean_ctor_get(x_170, 1); +lean_inc(x_174); +x_175 = lean_nat_dec_eq(x_174, x_169); +lean_dec(x_174); +if (x_175 == 0) +{ +lean_object* x_176; lean_object* x_177; +lean_dec(x_169); +x_176 = l_Lean_nullKind; +x_177 = l_Lean_Parser_ParserState_mkNode(x_170, x_176, x_168); +x_116 = x_177; +goto block_164; +} +else +{ +lean_object* x_178; lean_object* x_179; lean_object* x_180; +x_178 = l_Lean_Parser_ParserState_restore(x_170, x_168, x_169); +x_179 = l_Lean_nullKind; +x_180 = l_Lean_Parser_ParserState_mkNode(x_178, x_179, x_168); +x_116 = x_180; +goto block_164; +} +} +} +} +else +{ +lean_object* x_195; lean_object* x_196; lean_object* x_197; +lean_dec(x_166); +lean_dec(x_4); +lean_dec(x_1); +x_195 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_196 = l_Lean_Parser_ParserState_mkNode(x_165, x_195, x_115); +x_197 = l_Lean_Parser_mergeOrElseErrors(x_196, x_107, x_104); +lean_dec(x_104); +return x_197; +} +} +} +else +{ +lean_object* x_213; +lean_dec(x_113); +lean_dec(x_4); +lean_dec(x_1); +x_213 = l_Lean_Parser_mergeOrElseErrors(x_112, x_107, x_104); +lean_dec(x_104); +return x_213; +} +} +} +} +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_letrec___elambda__1___closed__6; +x_2 = l_Lean_Parser_symbolInfo(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_letrec___elambda__1___closed__8; +x_2 = l_Lean_Parser_symbolInfo(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_letrec___closed__2; +x_2 = l_Lean_Parser_optionaInfo(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Term_letDecl; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Term_tupleTail___closed__1; +x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_letrec___closed__4; +x_2 = l_Lean_Parser_noFirstTokenInfo(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_letrec___closed__5; +x_2 = l_Lean_Parser_Term_let___closed__2; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Term_letDecl; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Term_letrec___closed__6; +x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__8() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_letrec___closed__3; +x_2 = l_Lean_Parser_Term_letrec___closed__7; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__9() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_letrec___closed__1; +x_2 = l_Lean_Parser_Term_letrec___closed__8; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__10() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_2 = l_Lean_Parser_Term_letrec___closed__9; +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__11() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_epsilonInfo; +x_2 = l_Lean_Parser_Term_letrec___closed__10; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__12() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Term_letrec___elambda__1___closed__4; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Term_letrec___closed__11; +x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__13() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_letrec___elambda__1), 2, 0); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec___closed__14() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_letrec___closed__12; +x_2 = l_Lean_Parser_Term_letrec___closed__13; +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_Term_letrec() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Parser_Term_letrec___closed__14; +return x_1; +} +} +lean_object* l___regBuiltinParser_Lean_Parser_Term_letrec(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; +x_2 = l_Lean_Parser_termParser___closed__2; +x_3 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_4 = 1; +x_5 = l_Lean_Parser_Term_letrec; +x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1); +return x_6; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_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_Term_letrec___elambda__1___closed__1; +x_2 = l_Lean_Parser_Term_letrec___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_Term_letrec_formatter___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_letrec___elambda__1___closed__5; +x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_symbol_formatter___boxed), 6, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_formatter___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_letrec___elambda__1___closed__7; +x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_symbol_formatter___boxed), 6, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_formatter___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_letrec_formatter___closed__3; +x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_optional_formatter), 6, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_formatter___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_tupleTail_formatter___closed__2; +x_2 = l_Lean_Parser_Term_let_formatter___closed__3; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_formatter___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_letrec_formatter___closed__5; +x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_many_formatter), 6, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_formatter___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_letrec_formatter___closed__6; +x_2 = l_Lean_Parser_Term_have_formatter___closed__7; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_formatter___closed__8() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_let_formatter___closed__3; +x_2 = l_Lean_Parser_Term_letrec_formatter___closed__7; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_formatter___closed__9() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_letrec_formatter___closed__4; +x_2 = l_Lean_Parser_Term_letrec_formatter___closed__8; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_formatter___closed__10() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_letrec_formatter___closed__2; +x_2 = l_Lean_Parser_Term_letrec_formatter___closed__9; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_formatter___closed__11() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_2 = l_Lean_Parser_Term_leadPrec; +x_3 = l_Lean_Parser_Term_letrec_formatter___closed__10; +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_Term_letrec_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_Term_letrec_formatter___closed__1; +x_7 = l_Lean_Parser_Term_letrec_formatter___closed__11; +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_Term_letrec_formatter___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_letrec_formatter), 5, 0); +return x_1; +} +} +lean_object* l___regBuiltin_Lean_Parser_Term_letrec_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_Term_letrec___elambda__1___closed__2; +x_4 = l___regBuiltin_Lean_Parser_Term_letrec_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_Term_letrec_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_Term_letrec___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_Term_letrec_parenthesizer___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3; +x_2 = l_Lean_Parser_Term_let_parenthesizer___closed__2; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_letrec_parenthesizer___closed__2; +x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_many_parenthesizer), 6, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_letrec_parenthesizer___closed__3; +x_2 = l_Lean_Parser_Term_typeAscription_parenthesizer___closed__2; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_let_parenthesizer___closed__2; +x_2 = l_Lean_Parser_Term_letrec_parenthesizer___closed__4; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_structInst_parenthesizer___closed__6; +x_2 = l_Lean_Parser_Term_letrec_parenthesizer___closed__5; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3; +x_2 = l_Lean_Parser_Term_letrec_parenthesizer___closed__6; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__8() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Term_letrec___elambda__1___closed__2; +x_2 = l_Lean_Parser_Term_leadPrec; +x_3 = l_Lean_Parser_Term_letrec_parenthesizer___closed__7; +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_Term_letrec_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_Term_letrec_parenthesizer___closed__1; +x_7 = l_Lean_Parser_Term_letrec_parenthesizer___closed__8; +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_Term_letrec_parenthesizer___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_letrec_parenthesizer), 5, 0); +return x_1; +} +} +lean_object* l___regBuiltin_Lean_Parser_Term_letrec_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_Term_letrec___elambda__1___closed__2; +x_4 = l___regBuiltin_Lean_Parser_Term_letrec_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_Term_leftArrow___elambda__1___closed__1() { _start: { @@ -53945,22 +55479,10 @@ return x_4; lean_object* _init_l_Lean_Parser_Term_doLet_parenthesizer___closed__2() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3; -x_2 = l_Lean_Parser_Term_let_parenthesizer___closed__2; -x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2); -lean_closure_set(x_3, 0, x_1); -lean_closure_set(x_3, 1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_doLet_parenthesizer___closed__3() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Term_doLet___elambda__1___closed__2; x_2 = lean_unsigned_to_nat(1024u); -x_3 = l_Lean_Parser_Term_doLet_parenthesizer___closed__2; +x_3 = l_Lean_Parser_Term_letrec_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); @@ -53973,7 +55495,7 @@ _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; x_6 = l_Lean_Parser_Term_doLet_parenthesizer___closed__1; -x_7 = l_Lean_Parser_Term_doLet_parenthesizer___closed__3; +x_7 = l_Lean_Parser_Term_doLet_parenthesizer___closed__2; x_8 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5); return x_8; } @@ -79469,6 +80991,115 @@ lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_let_x21_parenthesizer___clo res = l___regBuiltin_Lean_Parser_Term_let_x21_parenthesizer(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l_Lean_Parser_Term_letrec___elambda__1___closed__1 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__1); +l_Lean_Parser_Term_letrec___elambda__1___closed__2 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__2); +l_Lean_Parser_Term_letrec___elambda__1___closed__3 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__3); +l_Lean_Parser_Term_letrec___elambda__1___closed__4 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__4); +l_Lean_Parser_Term_letrec___elambda__1___closed__5 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__5); +l_Lean_Parser_Term_letrec___elambda__1___closed__6 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__6(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__6); +l_Lean_Parser_Term_letrec___elambda__1___closed__7 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__7(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__7); +l_Lean_Parser_Term_letrec___elambda__1___closed__8 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__8(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__8); +l_Lean_Parser_Term_letrec___elambda__1___closed__9 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__9(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__9); +l_Lean_Parser_Term_letrec___elambda__1___closed__10 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__10(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__10); +l_Lean_Parser_Term_letrec___elambda__1___closed__11 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__11(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__11); +l_Lean_Parser_Term_letrec___elambda__1___closed__12 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__12(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__12); +l_Lean_Parser_Term_letrec___elambda__1___closed__13 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__13(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__13); +l_Lean_Parser_Term_letrec___elambda__1___closed__14 = _init_l_Lean_Parser_Term_letrec___elambda__1___closed__14(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___elambda__1___closed__14); +l_Lean_Parser_Term_letrec___closed__1 = _init_l_Lean_Parser_Term_letrec___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__1); +l_Lean_Parser_Term_letrec___closed__2 = _init_l_Lean_Parser_Term_letrec___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__2); +l_Lean_Parser_Term_letrec___closed__3 = _init_l_Lean_Parser_Term_letrec___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__3); +l_Lean_Parser_Term_letrec___closed__4 = _init_l_Lean_Parser_Term_letrec___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__4); +l_Lean_Parser_Term_letrec___closed__5 = _init_l_Lean_Parser_Term_letrec___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__5); +l_Lean_Parser_Term_letrec___closed__6 = _init_l_Lean_Parser_Term_letrec___closed__6(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__6); +l_Lean_Parser_Term_letrec___closed__7 = _init_l_Lean_Parser_Term_letrec___closed__7(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__7); +l_Lean_Parser_Term_letrec___closed__8 = _init_l_Lean_Parser_Term_letrec___closed__8(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__8); +l_Lean_Parser_Term_letrec___closed__9 = _init_l_Lean_Parser_Term_letrec___closed__9(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__9); +l_Lean_Parser_Term_letrec___closed__10 = _init_l_Lean_Parser_Term_letrec___closed__10(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__10); +l_Lean_Parser_Term_letrec___closed__11 = _init_l_Lean_Parser_Term_letrec___closed__11(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__11); +l_Lean_Parser_Term_letrec___closed__12 = _init_l_Lean_Parser_Term_letrec___closed__12(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__12); +l_Lean_Parser_Term_letrec___closed__13 = _init_l_Lean_Parser_Term_letrec___closed__13(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__13); +l_Lean_Parser_Term_letrec___closed__14 = _init_l_Lean_Parser_Term_letrec___closed__14(); +lean_mark_persistent(l_Lean_Parser_Term_letrec___closed__14); +l_Lean_Parser_Term_letrec = _init_l_Lean_Parser_Term_letrec(); +lean_mark_persistent(l_Lean_Parser_Term_letrec); +res = l___regBuiltinParser_Lean_Parser_Term_letrec(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +l_Lean_Parser_Term_letrec_formatter___closed__1 = _init_l_Lean_Parser_Term_letrec_formatter___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_formatter___closed__1); +l_Lean_Parser_Term_letrec_formatter___closed__2 = _init_l_Lean_Parser_Term_letrec_formatter___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_formatter___closed__2); +l_Lean_Parser_Term_letrec_formatter___closed__3 = _init_l_Lean_Parser_Term_letrec_formatter___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_formatter___closed__3); +l_Lean_Parser_Term_letrec_formatter___closed__4 = _init_l_Lean_Parser_Term_letrec_formatter___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_formatter___closed__4); +l_Lean_Parser_Term_letrec_formatter___closed__5 = _init_l_Lean_Parser_Term_letrec_formatter___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_formatter___closed__5); +l_Lean_Parser_Term_letrec_formatter___closed__6 = _init_l_Lean_Parser_Term_letrec_formatter___closed__6(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_formatter___closed__6); +l_Lean_Parser_Term_letrec_formatter___closed__7 = _init_l_Lean_Parser_Term_letrec_formatter___closed__7(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_formatter___closed__7); +l_Lean_Parser_Term_letrec_formatter___closed__8 = _init_l_Lean_Parser_Term_letrec_formatter___closed__8(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_formatter___closed__8); +l_Lean_Parser_Term_letrec_formatter___closed__9 = _init_l_Lean_Parser_Term_letrec_formatter___closed__9(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_formatter___closed__9); +l_Lean_Parser_Term_letrec_formatter___closed__10 = _init_l_Lean_Parser_Term_letrec_formatter___closed__10(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_formatter___closed__10); +l_Lean_Parser_Term_letrec_formatter___closed__11 = _init_l_Lean_Parser_Term_letrec_formatter___closed__11(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_formatter___closed__11); +l___regBuiltin_Lean_Parser_Term_letrec_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Term_letrec_formatter___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_letrec_formatter___closed__1); +res = l___regBuiltin_Lean_Parser_Term_letrec_formatter(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +l_Lean_Parser_Term_letrec_parenthesizer___closed__1 = _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_parenthesizer___closed__1); +l_Lean_Parser_Term_letrec_parenthesizer___closed__2 = _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_parenthesizer___closed__2); +l_Lean_Parser_Term_letrec_parenthesizer___closed__3 = _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_parenthesizer___closed__3); +l_Lean_Parser_Term_letrec_parenthesizer___closed__4 = _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_parenthesizer___closed__4); +l_Lean_Parser_Term_letrec_parenthesizer___closed__5 = _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_parenthesizer___closed__5); +l_Lean_Parser_Term_letrec_parenthesizer___closed__6 = _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__6(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_parenthesizer___closed__6); +l_Lean_Parser_Term_letrec_parenthesizer___closed__7 = _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__7(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_parenthesizer___closed__7); +l_Lean_Parser_Term_letrec_parenthesizer___closed__8 = _init_l_Lean_Parser_Term_letrec_parenthesizer___closed__8(); +lean_mark_persistent(l_Lean_Parser_Term_letrec_parenthesizer___closed__8); +l___regBuiltin_Lean_Parser_Term_letrec_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Term_letrec_parenthesizer___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_letrec_parenthesizer___closed__1); +res = l___regBuiltin_Lean_Parser_Term_letrec_parenthesizer(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l_Lean_Parser_Term_leftArrow___elambda__1___closed__1 = _init_l_Lean_Parser_Term_leftArrow___elambda__1___closed__1(); lean_mark_persistent(l_Lean_Parser_Term_leftArrow___elambda__1___closed__1); l_Lean_Parser_Term_leftArrow___elambda__1___closed__2 = _init_l_Lean_Parser_Term_leftArrow___elambda__1___closed__2(); @@ -79836,8 +81467,6 @@ l_Lean_Parser_Term_doLet_parenthesizer___closed__1 = _init_l_Lean_Parser_Term_do lean_mark_persistent(l_Lean_Parser_Term_doLet_parenthesizer___closed__1); l_Lean_Parser_Term_doLet_parenthesizer___closed__2 = _init_l_Lean_Parser_Term_doLet_parenthesizer___closed__2(); lean_mark_persistent(l_Lean_Parser_Term_doLet_parenthesizer___closed__2); -l_Lean_Parser_Term_doLet_parenthesizer___closed__3 = _init_l_Lean_Parser_Term_doLet_parenthesizer___closed__3(); -lean_mark_persistent(l_Lean_Parser_Term_doLet_parenthesizer___closed__3); l_Lean_Parser_Term_doId_parenthesizer___closed__1 = _init_l_Lean_Parser_Term_doId_parenthesizer___closed__1(); lean_mark_persistent(l_Lean_Parser_Term_doId_parenthesizer___closed__1); l_Lean_Parser_Term_doId_parenthesizer___closed__2 = _init_l_Lean_Parser_Term_doId_parenthesizer___closed__2();