From aef998af725ccefeee93c3bfb0e08cce774e4f09 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Jan 2020 11:47:07 -0800 Subject: [PATCH] chore: update stage0 --- stage0/src/Init/Lean/Elab/Quotation.lean | 4 +- .../stdlib/Init/Lean/Elab/BuiltinNotation.c | 42 +- stage0/stdlib/Init/Lean/Elab/Quotation.c | 1418 ++++++++++------- stage0/stdlib/Init/Lean/Elab/Syntax.c | 14 +- 4 files changed, 895 insertions(+), 583 deletions(-) diff --git a/stage0/src/Init/Lean/Elab/Quotation.lean b/stage0/src/Init/Lean/Elab/Quotation.lean index c0842231a6..e72496f32a 100644 --- a/stage0/src/Init/Lean/Elab/Quotation.lean +++ b/stage0/src/Init/Lean/Elab/Quotation.lean @@ -106,7 +106,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax let preresolved := resolveGlobalName env currNamespace openDecls val ++ preresolved; let val := quote val; -- `scp` is bound in stxQuot.expand - `(Syntax.ident none $(quote rawVal) (addMacroScope $val scp) $(quote preresolved)) + `(Syntax.ident none $(quote rawVal) (addMacroScopeExt mainModule $val scp) $(quote preresolved)) -- if antiquotation, insert contents as-is, else recurse | stx@(Syntax.node k args) => if isAntiquot stx then @@ -137,7 +137,7 @@ let quoted := stx.getArg 1; including it literally in a syntax quotation. -/ -- TODO: simplify to `(do scp ← getCurrMacroScope; pure $(quoteSyntax quoted)) stx ← quoteSyntax (elimAntiquotChoices quoted); -`(bind getCurrMacroScope (fun scp => pure $stx)) +`(bind getCurrMacroScope (fun scp => bind getMainModule (fun mainModule => pure $stx))) /- NOTE: It may seem like the newly introduced binding `scp` may accidentally capture identifiers in an antiquotation introduced by `quoteSyntax`. However, note that the syntax quotation above enjoys the same hygiene guarantees as diff --git a/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c b/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c index bfe5df872a..6bfd0fa604 100644 --- a/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c +++ b/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c @@ -318,6 +318,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAppend___closed__3; lean_object* l_Lean_Elab_Term_elabLE(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabDollar___closed__1; extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31; +extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; lean_object* l_Lean_Elab_Term_elabOr___closed__1; extern lean_object* l_Lean_mkAppStx___closed__6; lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__3; @@ -500,7 +501,6 @@ lean_object* l_Lean_Elab_Term_elabGT___boxed(lean_object*, lean_object*, lean_ob lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHEq___closed__3; extern lean_object* l_Lean_Parser_Term_mapConst___elambda__1___closed__2; lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__15; -extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; lean_object* l_Lean_Elab_Term_elabHEq___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabOrM(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_addBuiltinTermElab(lean_object*, lean_object*, lean_object*, lean_object*); @@ -1449,7 +1449,7 @@ lean_ctor_set(x_118, 0, x_69); lean_ctor_set(x_118, 1, x_117); x_119 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_120 = lean_array_push(x_119, x_118); -x_121 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_121 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_122 = lean_array_push(x_120, x_121); x_123 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_124 = lean_alloc_ctor(1, 2, 0); @@ -1537,7 +1537,7 @@ lean_ctor_set(x_170, 0, x_69); lean_ctor_set(x_170, 1, x_169); x_171 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_172 = lean_array_push(x_171, x_170); -x_173 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_173 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_174 = lean_array_push(x_172, x_173); x_175 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_176 = lean_alloc_ctor(1, 2, 0); @@ -1895,7 +1895,7 @@ lean_ctor_set(x_40, 0, x_39); lean_ctor_set(x_40, 1, x_38); x_41 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_42 = lean_array_push(x_41, x_40); -x_43 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_43 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_44 = lean_array_push(x_42, x_43); x_45 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_46 = lean_alloc_ctor(1, 2, 0); @@ -1978,7 +1978,7 @@ lean_ctor_set(x_90, 0, x_89); lean_ctor_set(x_90, 1, x_88); x_91 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_92 = lean_array_push(x_91, x_90); -x_93 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_93 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_94 = lean_array_push(x_92, x_93); x_95 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_96 = lean_alloc_ctor(1, 2, 0); @@ -2147,7 +2147,7 @@ lean_ctor_set(x_164, 0, x_119); lean_ctor_set(x_164, 1, x_163); x_165 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_166 = lean_array_push(x_165, x_164); -x_167 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_167 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_168 = lean_array_push(x_166, x_167); x_169 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_170 = lean_alloc_ctor(1, 2, 0); @@ -2238,7 +2238,7 @@ lean_ctor_set(x_218, 0, x_119); lean_ctor_set(x_218, 1, x_217); x_219 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_220 = lean_array_push(x_219, x_218); -x_221 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_221 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_222 = lean_array_push(x_220, x_221); x_223 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_224 = lean_alloc_ctor(1, 2, 0); @@ -2953,7 +2953,7 @@ lean_ctor_set(x_30, 0, x_27); lean_ctor_set(x_30, 1, x_29); x_31 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_32 = lean_array_push(x_31, x_30); -x_33 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_33 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_34 = lean_array_push(x_32, x_33); x_35 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_36 = lean_alloc_ctor(1, 2, 0); @@ -3022,7 +3022,7 @@ lean_ctor_set(x_70, 0, x_67); lean_ctor_set(x_70, 1, x_69); x_71 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_72 = lean_array_push(x_71, x_70); -x_73 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_73 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_74 = lean_array_push(x_72, x_73); x_75 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_76 = lean_alloc_ctor(1, 2, 0); @@ -3298,7 +3298,7 @@ lean_ctor_set(x_42, 0, x_39); lean_ctor_set(x_42, 1, x_41); x_43 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_44 = lean_array_push(x_43, x_42); -x_45 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_45 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_46 = lean_array_push(x_44, x_45); x_47 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_48 = lean_alloc_ctor(1, 2, 0); @@ -3372,7 +3372,7 @@ lean_ctor_set(x_86, 0, x_83); lean_ctor_set(x_86, 1, x_85); x_87 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_88 = lean_array_push(x_87, x_86); -x_89 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_89 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_90 = lean_array_push(x_88, x_89); x_91 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_92 = lean_alloc_ctor(1, 2, 0); @@ -3488,7 +3488,7 @@ lean_ctor_set(x_145, 0, x_142); lean_ctor_set(x_145, 1, x_144); x_146 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_147 = lean_array_push(x_146, x_145); -x_148 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_148 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_149 = lean_array_push(x_147, x_148); x_150 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_151 = lean_alloc_ctor(1, 2, 0); @@ -3562,7 +3562,7 @@ lean_ctor_set(x_189, 0, x_186); lean_ctor_set(x_189, 1, x_188); x_190 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_191 = lean_array_push(x_190, x_189); -x_192 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_192 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_193 = lean_array_push(x_191, x_192); x_194 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_195 = lean_alloc_ctor(1, 2, 0); @@ -3713,7 +3713,7 @@ lean_ctor_set(x_259, 0, x_226); lean_ctor_set(x_259, 1, x_258); x_260 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_261 = lean_array_push(x_260, x_259); -x_262 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_262 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_263 = lean_array_push(x_261, x_262); x_264 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_265 = lean_alloc_ctor(1, 2, 0); @@ -3780,7 +3780,7 @@ lean_ctor_set(x_298, 0, x_226); lean_ctor_set(x_298, 1, x_297); x_299 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_300 = lean_array_push(x_299, x_298); -x_301 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_301 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_302 = lean_array_push(x_300, x_301); x_303 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_304 = lean_alloc_ctor(1, 2, 0); @@ -3891,7 +3891,7 @@ lean_ctor_set(x_354, 0, x_226); lean_ctor_set(x_354, 1, x_353); x_355 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_356 = lean_array_push(x_355, x_354); -x_357 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_357 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_358 = lean_array_push(x_356, x_357); x_359 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_360 = lean_alloc_ctor(1, 2, 0); @@ -3958,7 +3958,7 @@ lean_ctor_set(x_393, 0, x_226); lean_ctor_set(x_393, 1, x_392); x_394 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_395 = lean_array_push(x_394, x_393); -x_396 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_396 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_397 = lean_array_push(x_395, x_396); x_398 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_399 = lean_alloc_ctor(1, 2, 0); @@ -4814,7 +4814,7 @@ lean_ctor_set(x_88, 0, x_46); lean_ctor_set(x_88, 1, x_87); x_89 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_90 = lean_array_push(x_89, x_88); -x_91 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_91 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_92 = lean_array_push(x_90, x_91); x_93 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_94 = lean_alloc_ctor(1, 2, 0); @@ -4902,7 +4902,7 @@ lean_ctor_set(x_135, 0, x_46); lean_ctor_set(x_135, 1, x_134); x_136 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_137 = lean_array_push(x_136, x_135); -x_138 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_138 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_139 = lean_array_push(x_137, x_138); x_140 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_141 = lean_alloc_ctor(1, 2, 0); @@ -4995,7 +4995,7 @@ lean_ctor_set(x_184, 0, x_46); lean_ctor_set(x_184, 1, x_183); x_185 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_186 = lean_array_push(x_185, x_184); -x_187 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_187 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_188 = lean_array_push(x_186, x_187); x_189 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_190 = lean_alloc_ctor(1, 2, 0); @@ -5101,7 +5101,7 @@ lean_ctor_set(x_241, 0, x_46); lean_ctor_set(x_241, 1, x_240); x_242 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_243 = lean_array_push(x_242, x_241); -x_244 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_244 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_245 = lean_array_push(x_243, x_244); x_246 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_247 = lean_alloc_ctor(1, 2, 0); diff --git a/stage0/stdlib/Init/Lean/Elab/Quotation.c b/stage0/stdlib/Init/Lean/Elab/Quotation.c index c0735fe51d..4ae132e535 100644 --- a/stage0/stdlib/Init/Lean/Elab/Quotation.c +++ b/stage0/stdlib/Init/Lean/Elab/Quotation.c @@ -20,6 +20,7 @@ lean_object* l_List_head_x21___at___private_Init_Lean_Elab_Quotation_9__compileS lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__18; lean_object* l_Lean_Elab_Term_getEnv___rarg(lean_object*); lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___elambda__3___closed__3; +lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__30; lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_Quotation_7__getHeadInfo___spec__2(lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__38; lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__21; @@ -111,6 +112,7 @@ lean_object* l_Lean_Parser_mkParserState(lean_object*); lean_object* l_List_append___rarg(lean_object*, lean_object*); lean_object* l_Lean_Substring_HasQuote(lean_object*); lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__1___closed__3; +lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56; lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__2___closed__1; uint8_t l_Lean_Elab_Term_HeadInfo_generalizes(lean_object*, lean_object*); uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_isAntiquotSplicePat___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); @@ -119,6 +121,7 @@ extern lean_object* l_Lean_Parser_Level_num___elambda__1___closed__1; lean_object* l_Lean_Substring_HasQuote___closed__1; lean_object* l___private_Init_Lean_Elab_Quotation_2__quoteList(lean_object*); lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___elambda__1___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__28; lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__19; lean_object* l_Lean_Substring_HasQuote___boxed(lean_object*); lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__16; @@ -133,6 +136,7 @@ lean_object* lean_array_push(lean_object*, lean_object*); lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__1; lean_object* lean_array_get_size(lean_object*); lean_object* l___private_Init_Lean_Elab_Quotation_8__explodeHeadPat___lambda__1___closed__3; +lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__31; lean_object* l___private_Init_Lean_Elab_Quotation_13__exprPlaceholder; extern lean_object* l_Lean_Parser_Term_num___elambda__1___closed__1; lean_object* l_Lean_Elab_Term_match__syntax_expand___boxed(lean_object*, lean_object*, lean_object*); @@ -309,6 +313,7 @@ lean_object* l___private_Init_Lean_Elab_Quotation_15__oldRunTermElabM___rarg___c lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__16; lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31; extern lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__1; +lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; lean_object* l_List_filterAux___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__6___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_14__toPreterm___main___spec__7(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_mkAppStx___closed__6; @@ -395,11 +400,14 @@ lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__28; lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_letPatDecl___elambda__1___closed__2; +lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__33; lean_object* l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_14__toPreterm___main___spec__4(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_getLCtx(lean_object*, lean_object*); lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__17; lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*); lean_object* l_List_head_x21___at___private_Init_Lean_Elab_Quotation_7__getHeadInfo___spec__1(lean_object*); +lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__29; +lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__57; lean_object* lean_expand_stx_quot(lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_if___elambda__1___closed__2; lean_object* l___private_Init_Lean_Elab_Quotation_12__letBindRhss(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -500,6 +508,7 @@ lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Quotation_ extern lean_object* l_Lean_Syntax_getKind___closed__3; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot(lean_object*); lean_object* l_Array_findMAux___main___at___private_Init_Lean_Elab_Quotation_4__elimAntiquotChoices___main___spec__2(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__34; lean_object* l_List_mapM___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__8___closed__7; lean_object* l_Lean_addMacroScopeExt(lean_object*, lean_object*, lean_object*); lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_Quotation_4__elimAntiquotChoices___main___spec__1(lean_object*, lean_object*); @@ -522,6 +531,7 @@ lean_object* l_Lean_mkStrLit(lean_object*); lean_object* l_Lean_mkCTermIdFrom(lean_object*, lean_object*); lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__1; lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__32; extern lean_object* l_Lean_Meta_DiscrTree_Trie_format___main___rarg___closed__1; lean_object* l_Lean_Syntax_formatStxAux___main(lean_object*, lean_object*, lean_object*); lean_object* l_List_toArrayAux___main___rarg(lean_object*, lean_object*); @@ -536,6 +546,7 @@ lean_object* l_List_mapM___main___at___private_Init_Lean_Elab_Quotation_9__compi lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Prod_hasQuote___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58; lean_object* l___private_Init_Lean_Elab_Quotation_4__elimAntiquotChoices(lean_object*); lean_object* l_Lean_Syntax_HasQuote; lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*); @@ -2423,7 +2434,7 @@ lean_object* _init_l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___ _start: { lean_object* x_1; -x_1 = lean_mk_string("addMacroScope"); +x_1 = lean_mk_string("addMacroScopeExt"); return x_1; } } @@ -2498,7 +2509,7 @@ lean_object* _init_l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___ _start: { lean_object* x_1; -x_1 = lean_mk_string("scp"); +x_1 = lean_mk_string("mainModule"); return x_1; } } @@ -2538,6 +2549,47 @@ return x_3; lean_object* _init_l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55() { _start: { +lean_object* x_1; +x_1 = lean_mk_string("scp"); +return x_1; +} +} +lean_object* _init_l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_2 = lean_string_utf8_byte_size(x_1); +return x_2; +} +} +lean_object* _init_l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__57() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_2 = lean_unsigned_to_nat(0u); +x_3 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56; +x_4 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} +lean_object* _init_l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59() { +_start: +{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); x_2 = l_Option_HasRepr___rarg___closed__3; @@ -3132,7 +3184,7 @@ lean_dec(x_2); x_266 = !lean_is_exclusive(x_265); if (x_266 == 0) { -lean_object* x_267; lean_object* x_268; lean_object* x_269; lean_object* x_270; lean_object* x_271; lean_object* x_272; lean_object* x_273; lean_object* x_274; lean_object* x_275; lean_object* x_276; lean_object* x_277; lean_object* x_278; lean_object* x_279; lean_object* x_280; lean_object* x_281; lean_object* x_282; lean_object* x_283; lean_object* x_284; lean_object* x_285; lean_object* x_286; lean_object* x_287; lean_object* x_288; lean_object* x_289; lean_object* x_290; lean_object* x_291; lean_object* x_292; lean_object* x_293; lean_object* x_294; lean_object* x_295; lean_object* x_296; lean_object* x_297; lean_object* x_298; lean_object* x_299; lean_object* x_300; lean_object* x_301; lean_object* x_302; lean_object* x_303; lean_object* x_304; lean_object* x_305; lean_object* x_306; lean_object* x_307; lean_object* x_308; lean_object* x_309; lean_object* x_310; lean_object* x_311; lean_object* x_312; lean_object* x_313; lean_object* x_314; lean_object* x_315; lean_object* x_316; lean_object* x_317; lean_object* x_318; lean_object* x_319; lean_object* x_320; lean_object* x_321; lean_object* x_322; lean_object* x_323; lean_object* x_324; lean_object* x_325; lean_object* x_326; lean_object* x_327; lean_object* x_328; lean_object* x_329; lean_object* x_330; lean_object* x_331; lean_object* x_332; lean_object* x_333; lean_object* x_334; lean_object* x_335; lean_object* x_336; lean_object* x_337; lean_object* x_338; lean_object* x_339; lean_object* x_340; lean_object* x_341; +lean_object* x_267; lean_object* x_268; lean_object* x_269; lean_object* x_270; lean_object* x_271; lean_object* x_272; lean_object* x_273; lean_object* x_274; lean_object* x_275; lean_object* x_276; lean_object* x_277; lean_object* x_278; lean_object* x_279; lean_object* x_280; lean_object* x_281; lean_object* x_282; lean_object* x_283; lean_object* x_284; lean_object* x_285; lean_object* x_286; lean_object* x_287; lean_object* x_288; lean_object* x_289; lean_object* x_290; lean_object* x_291; lean_object* x_292; lean_object* x_293; lean_object* x_294; lean_object* x_295; lean_object* x_296; lean_object* x_297; lean_object* x_298; lean_object* x_299; lean_object* x_300; lean_object* x_301; lean_object* x_302; lean_object* x_303; lean_object* x_304; lean_object* x_305; lean_object* x_306; lean_object* x_307; lean_object* x_308; lean_object* x_309; lean_object* x_310; lean_object* x_311; lean_object* x_312; lean_object* x_313; lean_object* x_314; lean_object* x_315; lean_object* x_316; lean_object* x_317; lean_object* x_318; lean_object* x_319; lean_object* x_320; lean_object* x_321; lean_object* x_322; lean_object* x_323; lean_object* x_324; lean_object* x_325; lean_object* x_326; lean_object* x_327; lean_object* x_328; lean_object* x_329; lean_object* x_330; lean_object* x_331; lean_object* x_332; lean_object* x_333; lean_object* x_334; lean_object* x_335; lean_object* x_336; lean_object* x_337; lean_object* x_338; lean_object* x_339; lean_object* x_340; lean_object* x_341; lean_object* x_342; lean_object* x_343; lean_object* x_344; lean_object* x_345; lean_object* x_346; lean_object* x_347; lean_object* x_348; lean_object* x_349; x_267 = lean_ctor_get(x_265, 0); x_268 = lean_box(0); x_269 = lean_box(0); @@ -3187,392 +3239,437 @@ x_298 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_298, 0, x_279); lean_ctor_set(x_298, 1, x_297); x_299 = lean_array_push(x_275, x_298); -x_300 = lean_array_push(x_275, x_264); -x_301 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__54; -x_302 = l_Lean_addMacroScopeExt(x_269, x_301, x_267); -x_303 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__53; -x_304 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_304, 0, x_268); -lean_ctor_set(x_304, 1, x_303); -lean_ctor_set(x_304, 2, x_302); -lean_ctor_set(x_304, 3, x_272); -x_305 = lean_array_push(x_275, x_304); -x_306 = lean_array_push(x_305, x_277); -x_307 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_307, 0, x_279); -lean_ctor_set(x_307, 1, x_306); -x_308 = lean_array_push(x_300, x_307); -x_309 = l_Lean_nullKind___closed__2; -x_310 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_310, 0, x_309); -lean_ctor_set(x_310, 1, x_308); -x_311 = lean_array_push(x_299, x_310); -x_312 = l_Lean_mkAppStx___closed__8; -x_313 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_313, 0, x_312); -lean_ctor_set(x_313, 1, x_311); -x_314 = lean_array_push(x_275, x_313); -x_315 = lean_array_push(x_314, x_277); -x_316 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_316, 0, x_309); -lean_ctor_set(x_316, 1, x_315); -x_317 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; -x_318 = lean_array_push(x_317, x_316); -x_319 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; -x_320 = lean_array_push(x_318, x_319); -x_321 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; -x_322 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_322, 0, x_321); -lean_ctor_set(x_322, 1, x_320); -x_323 = l___private_Init_Lean_Elab_Quotation_2__quoteList___main___at___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___spec__2(x_263); -x_324 = lean_ctor_get(x_249, 0); -lean_inc(x_324); -x_325 = lean_ctor_get(x_249, 1); -lean_inc(x_325); -x_326 = lean_ctor_get(x_249, 2); -lean_inc(x_326); +x_300 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__54; +lean_inc(x_267); +x_301 = l_Lean_addMacroScopeExt(x_269, x_300, x_267); +x_302 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__53; +x_303 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_303, 0, x_268); +lean_ctor_set(x_303, 1, x_302); +lean_ctor_set(x_303, 2, x_301); +lean_ctor_set(x_303, 3, x_272); +x_304 = lean_array_push(x_275, x_303); +x_305 = lean_array_push(x_304, x_277); +x_306 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_306, 0, x_279); +lean_ctor_set(x_306, 1, x_305); +x_307 = lean_array_push(x_275, x_306); +x_308 = lean_array_push(x_307, x_264); +x_309 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58; +x_310 = l_Lean_addMacroScopeExt(x_269, x_309, x_267); +x_311 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__57; +x_312 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_312, 0, x_268); +lean_ctor_set(x_312, 1, x_311); +lean_ctor_set(x_312, 2, x_310); +lean_ctor_set(x_312, 3, x_272); +x_313 = lean_array_push(x_275, x_312); +x_314 = lean_array_push(x_313, x_277); +x_315 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_315, 0, x_279); +lean_ctor_set(x_315, 1, x_314); +x_316 = lean_array_push(x_308, x_315); +x_317 = l_Lean_nullKind___closed__2; +x_318 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_318, 0, x_317); +lean_ctor_set(x_318, 1, x_316); +x_319 = lean_array_push(x_299, x_318); +x_320 = l_Lean_mkAppStx___closed__8; +x_321 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_321, 0, x_320); +lean_ctor_set(x_321, 1, x_319); +x_322 = lean_array_push(x_275, x_321); +x_323 = lean_array_push(x_322, x_277); +x_324 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_324, 0, x_317); +lean_ctor_set(x_324, 1, x_323); +x_325 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; +x_326 = lean_array_push(x_325, x_324); +x_327 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; +x_328 = lean_array_push(x_326, x_327); +x_329 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; +x_330 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_330, 0, x_329); +lean_ctor_set(x_330, 1, x_328); +x_331 = l___private_Init_Lean_Elab_Quotation_2__quoteList___main___at___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___spec__2(x_263); +x_332 = lean_ctor_get(x_249, 0); +lean_inc(x_332); +x_333 = lean_ctor_get(x_249, 1); +lean_inc(x_333); +x_334 = lean_ctor_get(x_249, 2); +lean_inc(x_334); lean_dec(x_249); -x_327 = lean_string_utf8_extract(x_324, x_325, x_326); -lean_dec(x_326); -lean_dec(x_325); -lean_dec(x_324); -x_328 = l_Lean_mkStxStrLit(x_327, x_268); -x_329 = l_Lean_mkOptionalNode___closed__2; -x_330 = lean_array_push(x_329, x_328); -x_331 = l_Lean_Parser_Term_str___elambda__1___closed__2; -x_332 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_332, 0, x_331); -lean_ctor_set(x_332, 1, x_330); -x_333 = lean_array_push(x_329, x_332); -x_334 = l_Lean_Substring_HasQuote___closed__2; -x_335 = l_Lean_mkCAppStx(x_334, x_333); -x_336 = lean_array_push(x_290, x_335); -x_337 = lean_array_push(x_336, x_322); -x_338 = lean_array_push(x_337, x_323); -x_339 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_339, 0, x_309); -lean_ctor_set(x_339, 1, x_338); -x_340 = lean_array_push(x_281, x_339); -x_341 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_341, 0, x_312); -lean_ctor_set(x_341, 1, x_340); -lean_ctor_set(x_265, 0, x_341); +x_335 = lean_string_utf8_extract(x_332, x_333, x_334); +lean_dec(x_334); +lean_dec(x_333); +lean_dec(x_332); +x_336 = l_Lean_mkStxStrLit(x_335, x_268); +x_337 = l_Lean_mkOptionalNode___closed__2; +x_338 = lean_array_push(x_337, x_336); +x_339 = l_Lean_Parser_Term_str___elambda__1___closed__2; +x_340 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_340, 0, x_339); +lean_ctor_set(x_340, 1, x_338); +x_341 = lean_array_push(x_337, x_340); +x_342 = l_Lean_Substring_HasQuote___closed__2; +x_343 = l_Lean_mkCAppStx(x_342, x_341); +x_344 = lean_array_push(x_290, x_343); +x_345 = lean_array_push(x_344, x_330); +x_346 = lean_array_push(x_345, x_331); +x_347 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_347, 0, x_317); +lean_ctor_set(x_347, 1, x_346); +x_348 = lean_array_push(x_281, x_347); +x_349 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_349, 0, x_320); +lean_ctor_set(x_349, 1, x_348); +lean_ctor_set(x_265, 0, x_349); return x_265; } else { -lean_object* x_342; lean_object* x_343; lean_object* x_344; lean_object* x_345; lean_object* x_346; lean_object* x_347; lean_object* x_348; lean_object* x_349; lean_object* x_350; lean_object* x_351; lean_object* x_352; lean_object* x_353; lean_object* x_354; lean_object* x_355; lean_object* x_356; lean_object* x_357; lean_object* x_358; lean_object* x_359; lean_object* x_360; lean_object* x_361; lean_object* x_362; lean_object* x_363; lean_object* x_364; lean_object* x_365; lean_object* x_366; lean_object* x_367; lean_object* x_368; lean_object* x_369; lean_object* x_370; lean_object* x_371; lean_object* x_372; lean_object* x_373; lean_object* x_374; lean_object* x_375; lean_object* x_376; lean_object* x_377; lean_object* x_378; lean_object* x_379; lean_object* x_380; lean_object* x_381; lean_object* x_382; lean_object* x_383; lean_object* x_384; lean_object* x_385; lean_object* x_386; lean_object* x_387; lean_object* x_388; lean_object* x_389; lean_object* x_390; lean_object* x_391; lean_object* x_392; lean_object* x_393; lean_object* x_394; lean_object* x_395; lean_object* x_396; lean_object* x_397; lean_object* x_398; lean_object* x_399; lean_object* x_400; lean_object* x_401; lean_object* x_402; lean_object* x_403; lean_object* x_404; lean_object* x_405; lean_object* x_406; lean_object* x_407; lean_object* x_408; lean_object* x_409; lean_object* x_410; lean_object* x_411; lean_object* x_412; lean_object* x_413; lean_object* x_414; lean_object* x_415; lean_object* x_416; lean_object* x_417; lean_object* x_418; -x_342 = lean_ctor_get(x_265, 0); -x_343 = lean_ctor_get(x_265, 1); -lean_inc(x_343); -lean_inc(x_342); +lean_object* x_350; lean_object* x_351; lean_object* x_352; lean_object* x_353; lean_object* x_354; lean_object* x_355; lean_object* x_356; lean_object* x_357; lean_object* x_358; lean_object* x_359; lean_object* x_360; lean_object* x_361; lean_object* x_362; lean_object* x_363; lean_object* x_364; lean_object* x_365; lean_object* x_366; lean_object* x_367; lean_object* x_368; lean_object* x_369; lean_object* x_370; lean_object* x_371; lean_object* x_372; lean_object* x_373; lean_object* x_374; lean_object* x_375; lean_object* x_376; lean_object* x_377; lean_object* x_378; lean_object* x_379; lean_object* x_380; lean_object* x_381; lean_object* x_382; lean_object* x_383; lean_object* x_384; lean_object* x_385; lean_object* x_386; lean_object* x_387; lean_object* x_388; lean_object* x_389; lean_object* x_390; lean_object* x_391; lean_object* x_392; lean_object* x_393; lean_object* x_394; lean_object* x_395; lean_object* x_396; lean_object* x_397; lean_object* x_398; lean_object* x_399; lean_object* x_400; lean_object* x_401; lean_object* x_402; lean_object* x_403; lean_object* x_404; lean_object* x_405; lean_object* x_406; lean_object* x_407; lean_object* x_408; lean_object* x_409; lean_object* x_410; lean_object* x_411; lean_object* x_412; lean_object* x_413; lean_object* x_414; lean_object* x_415; lean_object* x_416; lean_object* x_417; lean_object* x_418; lean_object* x_419; lean_object* x_420; lean_object* x_421; lean_object* x_422; lean_object* x_423; lean_object* x_424; lean_object* x_425; lean_object* x_426; lean_object* x_427; lean_object* x_428; lean_object* x_429; lean_object* x_430; lean_object* x_431; lean_object* x_432; lean_object* x_433; lean_object* x_434; +x_350 = lean_ctor_get(x_265, 0); +x_351 = lean_ctor_get(x_265, 1); +lean_inc(x_351); +lean_inc(x_350); lean_dec(x_265); -x_344 = lean_box(0); -x_345 = lean_box(0); -x_346 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__38; -lean_inc(x_342); -x_347 = l_Lean_addMacroScopeExt(x_345, x_346, x_342); -x_348 = lean_box(0); -x_349 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__37; -x_350 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__41; -lean_ctor_set(x_1, 3, x_350); -lean_ctor_set(x_1, 2, x_347); -lean_ctor_set(x_1, 1, x_349); -lean_ctor_set(x_1, 0, x_344); -x_351 = l_Array_empty___closed__1; -x_352 = lean_array_push(x_351, x_1); -x_353 = l___private_Init_Lean_Elab_Term_5__expandCDot___closed__4; -x_354 = lean_array_push(x_352, x_353); -x_355 = l_Lean_mkTermIdFromIdent___closed__2; -x_356 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_356, 0, x_355); -lean_ctor_set(x_356, 1, x_354); -x_357 = lean_array_push(x_351, x_356); -x_358 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__32; -lean_inc(x_342); -x_359 = l_Lean_addMacroScopeExt(x_345, x_358, x_342); -x_360 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31; -x_361 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__34; -x_362 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_362, 0, x_344); -lean_ctor_set(x_362, 1, x_360); -lean_ctor_set(x_362, 2, x_359); -lean_ctor_set(x_362, 3, x_361); -x_363 = lean_array_push(x_351, x_362); -x_364 = lean_array_push(x_363, x_353); -x_365 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_365, 0, x_355); -lean_ctor_set(x_365, 1, x_364); -x_366 = lean_array_push(x_351, x_365); -x_367 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__47; -lean_inc(x_342); -x_368 = l_Lean_addMacroScopeExt(x_345, x_367, x_342); -x_369 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__46; -x_370 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__50; -x_371 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_371, 0, x_344); -lean_ctor_set(x_371, 1, x_369); -lean_ctor_set(x_371, 2, x_368); -lean_ctor_set(x_371, 3, x_370); -x_372 = lean_array_push(x_351, x_371); -x_373 = lean_array_push(x_372, x_353); -x_374 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_374, 0, x_355); -lean_ctor_set(x_374, 1, x_373); -x_375 = lean_array_push(x_351, x_374); -x_376 = lean_array_push(x_351, x_264); -x_377 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__54; -x_378 = l_Lean_addMacroScopeExt(x_345, x_377, x_342); -x_379 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__53; -x_380 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_380, 0, x_344); -lean_ctor_set(x_380, 1, x_379); -lean_ctor_set(x_380, 2, x_378); -lean_ctor_set(x_380, 3, x_348); -x_381 = lean_array_push(x_351, x_380); -x_382 = lean_array_push(x_381, x_353); -x_383 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_383, 0, x_355); -lean_ctor_set(x_383, 1, x_382); -x_384 = lean_array_push(x_376, x_383); -x_385 = l_Lean_nullKind___closed__2; -x_386 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_386, 0, x_385); -lean_ctor_set(x_386, 1, x_384); -x_387 = lean_array_push(x_375, x_386); -x_388 = l_Lean_mkAppStx___closed__8; -x_389 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_389, 0, x_388); -lean_ctor_set(x_389, 1, x_387); -x_390 = lean_array_push(x_351, x_389); -x_391 = lean_array_push(x_390, x_353); -x_392 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_392, 0, x_385); -lean_ctor_set(x_392, 1, x_391); -x_393 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; -x_394 = lean_array_push(x_393, x_392); -x_395 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; -x_396 = lean_array_push(x_394, x_395); -x_397 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; -x_398 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_398, 0, x_397); -lean_ctor_set(x_398, 1, x_396); -x_399 = l___private_Init_Lean_Elab_Quotation_2__quoteList___main___at___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___spec__2(x_263); -x_400 = lean_ctor_get(x_249, 0); -lean_inc(x_400); -x_401 = lean_ctor_get(x_249, 1); -lean_inc(x_401); -x_402 = lean_ctor_get(x_249, 2); -lean_inc(x_402); -lean_dec(x_249); -x_403 = lean_string_utf8_extract(x_400, x_401, x_402); -lean_dec(x_402); -lean_dec(x_401); -lean_dec(x_400); -x_404 = l_Lean_mkStxStrLit(x_403, x_344); -x_405 = l_Lean_mkOptionalNode___closed__2; -x_406 = lean_array_push(x_405, x_404); -x_407 = l_Lean_Parser_Term_str___elambda__1___closed__2; +x_352 = lean_box(0); +x_353 = lean_box(0); +x_354 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__38; +lean_inc(x_350); +x_355 = l_Lean_addMacroScopeExt(x_353, x_354, x_350); +x_356 = lean_box(0); +x_357 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__37; +x_358 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__41; +lean_ctor_set(x_1, 3, x_358); +lean_ctor_set(x_1, 2, x_355); +lean_ctor_set(x_1, 1, x_357); +lean_ctor_set(x_1, 0, x_352); +x_359 = l_Array_empty___closed__1; +x_360 = lean_array_push(x_359, x_1); +x_361 = l___private_Init_Lean_Elab_Term_5__expandCDot___closed__4; +x_362 = lean_array_push(x_360, x_361); +x_363 = l_Lean_mkTermIdFromIdent___closed__2; +x_364 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_364, 0, x_363); +lean_ctor_set(x_364, 1, x_362); +x_365 = lean_array_push(x_359, x_364); +x_366 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__32; +lean_inc(x_350); +x_367 = l_Lean_addMacroScopeExt(x_353, x_366, x_350); +x_368 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31; +x_369 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__34; +x_370 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_370, 0, x_352); +lean_ctor_set(x_370, 1, x_368); +lean_ctor_set(x_370, 2, x_367); +lean_ctor_set(x_370, 3, x_369); +x_371 = lean_array_push(x_359, x_370); +x_372 = lean_array_push(x_371, x_361); +x_373 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_373, 0, x_363); +lean_ctor_set(x_373, 1, x_372); +x_374 = lean_array_push(x_359, x_373); +x_375 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__47; +lean_inc(x_350); +x_376 = l_Lean_addMacroScopeExt(x_353, x_375, x_350); +x_377 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__46; +x_378 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__50; +x_379 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_379, 0, x_352); +lean_ctor_set(x_379, 1, x_377); +lean_ctor_set(x_379, 2, x_376); +lean_ctor_set(x_379, 3, x_378); +x_380 = lean_array_push(x_359, x_379); +x_381 = lean_array_push(x_380, x_361); +x_382 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_382, 0, x_363); +lean_ctor_set(x_382, 1, x_381); +x_383 = lean_array_push(x_359, x_382); +x_384 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__54; +lean_inc(x_350); +x_385 = l_Lean_addMacroScopeExt(x_353, x_384, x_350); +x_386 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__53; +x_387 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_387, 0, x_352); +lean_ctor_set(x_387, 1, x_386); +lean_ctor_set(x_387, 2, x_385); +lean_ctor_set(x_387, 3, x_356); +x_388 = lean_array_push(x_359, x_387); +x_389 = lean_array_push(x_388, x_361); +x_390 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_390, 0, x_363); +lean_ctor_set(x_390, 1, x_389); +x_391 = lean_array_push(x_359, x_390); +x_392 = lean_array_push(x_391, x_264); +x_393 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58; +x_394 = l_Lean_addMacroScopeExt(x_353, x_393, x_350); +x_395 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__57; +x_396 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_396, 0, x_352); +lean_ctor_set(x_396, 1, x_395); +lean_ctor_set(x_396, 2, x_394); +lean_ctor_set(x_396, 3, x_356); +x_397 = lean_array_push(x_359, x_396); +x_398 = lean_array_push(x_397, x_361); +x_399 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_399, 0, x_363); +lean_ctor_set(x_399, 1, x_398); +x_400 = lean_array_push(x_392, x_399); +x_401 = l_Lean_nullKind___closed__2; +x_402 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_402, 0, x_401); +lean_ctor_set(x_402, 1, x_400); +x_403 = lean_array_push(x_383, x_402); +x_404 = l_Lean_mkAppStx___closed__8; +x_405 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_405, 0, x_404); +lean_ctor_set(x_405, 1, x_403); +x_406 = lean_array_push(x_359, x_405); +x_407 = lean_array_push(x_406, x_361); x_408 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_408, 0, x_407); -lean_ctor_set(x_408, 1, x_406); -x_409 = lean_array_push(x_405, x_408); -x_410 = l_Lean_Substring_HasQuote___closed__2; -x_411 = l_Lean_mkCAppStx(x_410, x_409); -x_412 = lean_array_push(x_366, x_411); -x_413 = lean_array_push(x_412, x_398); -x_414 = lean_array_push(x_413, x_399); -x_415 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_415, 0, x_385); -lean_ctor_set(x_415, 1, x_414); -x_416 = lean_array_push(x_357, x_415); -x_417 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_417, 0, x_388); -lean_ctor_set(x_417, 1, x_416); -x_418 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_418, 0, x_417); -lean_ctor_set(x_418, 1, x_343); -return x_418; +lean_ctor_set(x_408, 0, x_401); +lean_ctor_set(x_408, 1, x_407); +x_409 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; +x_410 = lean_array_push(x_409, x_408); +x_411 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; +x_412 = lean_array_push(x_410, x_411); +x_413 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; +x_414 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_414, 0, x_413); +lean_ctor_set(x_414, 1, x_412); +x_415 = l___private_Init_Lean_Elab_Quotation_2__quoteList___main___at___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___spec__2(x_263); +x_416 = lean_ctor_get(x_249, 0); +lean_inc(x_416); +x_417 = lean_ctor_get(x_249, 1); +lean_inc(x_417); +x_418 = lean_ctor_get(x_249, 2); +lean_inc(x_418); +lean_dec(x_249); +x_419 = lean_string_utf8_extract(x_416, x_417, x_418); +lean_dec(x_418); +lean_dec(x_417); +lean_dec(x_416); +x_420 = l_Lean_mkStxStrLit(x_419, x_352); +x_421 = l_Lean_mkOptionalNode___closed__2; +x_422 = lean_array_push(x_421, x_420); +x_423 = l_Lean_Parser_Term_str___elambda__1___closed__2; +x_424 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_424, 0, x_423); +lean_ctor_set(x_424, 1, x_422); +x_425 = lean_array_push(x_421, x_424); +x_426 = l_Lean_Substring_HasQuote___closed__2; +x_427 = l_Lean_mkCAppStx(x_426, x_425); +x_428 = lean_array_push(x_374, x_427); +x_429 = lean_array_push(x_428, x_414); +x_430 = lean_array_push(x_429, x_415); +x_431 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_431, 0, x_401); +lean_ctor_set(x_431, 1, x_430); +x_432 = lean_array_push(x_365, x_431); +x_433 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_433, 0, x_404); +lean_ctor_set(x_433, 1, x_432); +x_434 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_434, 0, x_433); +lean_ctor_set(x_434, 1, x_351); +return x_434; } } else { -lean_object* x_419; lean_object* x_420; lean_object* x_421; lean_object* x_422; lean_object* x_423; lean_object* x_424; lean_object* x_425; lean_object* x_426; lean_object* x_427; lean_object* x_428; lean_object* x_429; lean_object* x_430; lean_object* x_431; lean_object* x_432; lean_object* x_433; lean_object* x_434; lean_object* x_435; lean_object* x_436; lean_object* x_437; lean_object* x_438; lean_object* x_439; lean_object* x_440; lean_object* x_441; lean_object* x_442; lean_object* x_443; lean_object* x_444; lean_object* x_445; lean_object* x_446; lean_object* x_447; lean_object* x_448; lean_object* x_449; lean_object* x_450; lean_object* x_451; lean_object* x_452; lean_object* x_453; lean_object* x_454; lean_object* x_455; lean_object* x_456; lean_object* x_457; lean_object* x_458; lean_object* x_459; lean_object* x_460; lean_object* x_461; lean_object* x_462; lean_object* x_463; lean_object* x_464; lean_object* x_465; lean_object* x_466; lean_object* x_467; lean_object* x_468; lean_object* x_469; lean_object* x_470; lean_object* x_471; lean_object* x_472; lean_object* x_473; lean_object* x_474; lean_object* x_475; lean_object* x_476; lean_object* x_477; lean_object* x_478; lean_object* x_479; lean_object* x_480; lean_object* x_481; lean_object* x_482; lean_object* x_483; lean_object* x_484; lean_object* x_485; lean_object* x_486; lean_object* x_487; lean_object* x_488; lean_object* x_489; lean_object* x_490; lean_object* x_491; lean_object* x_492; lean_object* x_493; lean_object* x_494; lean_object* x_495; lean_object* x_496; lean_object* x_497; lean_object* x_498; lean_object* x_499; lean_object* x_500; lean_object* x_501; lean_object* x_502; lean_object* x_503; lean_object* x_504; lean_object* x_505; lean_object* x_506; lean_object* x_507; lean_object* x_508; lean_object* x_509; lean_object* x_510; lean_object* x_511; lean_object* x_512; lean_object* x_513; -x_419 = lean_ctor_get(x_1, 1); -x_420 = lean_ctor_get(x_1, 2); -x_421 = lean_ctor_get(x_1, 3); -lean_inc(x_421); -lean_inc(x_420); -lean_inc(x_419); -lean_dec(x_1); -x_422 = l_Lean_Elab_Term_getEnv___rarg(x_3); -x_423 = lean_ctor_get(x_422, 0); -lean_inc(x_423); -x_424 = lean_ctor_get(x_422, 1); -lean_inc(x_424); -lean_dec(x_422); -x_425 = l_Lean_Elab_Term_getCurrNamespace(x_2, x_424); -x_426 = lean_ctor_get(x_425, 0); -lean_inc(x_426); -x_427 = lean_ctor_get(x_425, 1); -lean_inc(x_427); -lean_dec(x_425); -x_428 = l_Lean_Elab_Term_getOpenDecls(x_2, x_427); -x_429 = lean_ctor_get(x_428, 0); -lean_inc(x_429); -x_430 = lean_ctor_get(x_428, 1); -lean_inc(x_430); -lean_dec(x_428); -lean_inc(x_420); -x_431 = l_Lean_Elab_resolveGlobalName(x_423, x_426, x_429, x_420); -lean_dec(x_426); -x_432 = l_List_append___rarg(x_431, x_421); -x_433 = l___private_Init_Lean_Elab_Quotation_1__quoteName___main(x_420); -x_434 = l_Lean_Elab_Term_getCurrMacroScope(x_2, x_430); -lean_dec(x_2); -x_435 = lean_ctor_get(x_434, 0); -lean_inc(x_435); -x_436 = lean_ctor_get(x_434, 1); +lean_object* x_435; lean_object* x_436; lean_object* x_437; lean_object* x_438; lean_object* x_439; lean_object* x_440; lean_object* x_441; lean_object* x_442; lean_object* x_443; lean_object* x_444; lean_object* x_445; lean_object* x_446; lean_object* x_447; lean_object* x_448; lean_object* x_449; lean_object* x_450; lean_object* x_451; lean_object* x_452; lean_object* x_453; lean_object* x_454; lean_object* x_455; lean_object* x_456; lean_object* x_457; lean_object* x_458; lean_object* x_459; lean_object* x_460; lean_object* x_461; lean_object* x_462; lean_object* x_463; lean_object* x_464; lean_object* x_465; lean_object* x_466; lean_object* x_467; lean_object* x_468; lean_object* x_469; lean_object* x_470; lean_object* x_471; lean_object* x_472; lean_object* x_473; lean_object* x_474; lean_object* x_475; lean_object* x_476; lean_object* x_477; lean_object* x_478; lean_object* x_479; lean_object* x_480; lean_object* x_481; lean_object* x_482; lean_object* x_483; lean_object* x_484; lean_object* x_485; lean_object* x_486; lean_object* x_487; lean_object* x_488; lean_object* x_489; lean_object* x_490; lean_object* x_491; lean_object* x_492; lean_object* x_493; lean_object* x_494; lean_object* x_495; lean_object* x_496; lean_object* x_497; lean_object* x_498; lean_object* x_499; lean_object* x_500; lean_object* x_501; lean_object* x_502; lean_object* x_503; lean_object* x_504; lean_object* x_505; lean_object* x_506; lean_object* x_507; lean_object* x_508; lean_object* x_509; lean_object* x_510; lean_object* x_511; lean_object* x_512; lean_object* x_513; lean_object* x_514; lean_object* x_515; lean_object* x_516; lean_object* x_517; lean_object* x_518; lean_object* x_519; lean_object* x_520; lean_object* x_521; lean_object* x_522; lean_object* x_523; lean_object* x_524; lean_object* x_525; lean_object* x_526; lean_object* x_527; lean_object* x_528; lean_object* x_529; lean_object* x_530; lean_object* x_531; lean_object* x_532; lean_object* x_533; lean_object* x_534; lean_object* x_535; lean_object* x_536; lean_object* x_537; +x_435 = lean_ctor_get(x_1, 1); +x_436 = lean_ctor_get(x_1, 2); +x_437 = lean_ctor_get(x_1, 3); +lean_inc(x_437); lean_inc(x_436); -if (lean_is_exclusive(x_434)) { - lean_ctor_release(x_434, 0); - lean_ctor_release(x_434, 1); - x_437 = x_434; +lean_inc(x_435); +lean_dec(x_1); +x_438 = l_Lean_Elab_Term_getEnv___rarg(x_3); +x_439 = lean_ctor_get(x_438, 0); +lean_inc(x_439); +x_440 = lean_ctor_get(x_438, 1); +lean_inc(x_440); +lean_dec(x_438); +x_441 = l_Lean_Elab_Term_getCurrNamespace(x_2, x_440); +x_442 = lean_ctor_get(x_441, 0); +lean_inc(x_442); +x_443 = lean_ctor_get(x_441, 1); +lean_inc(x_443); +lean_dec(x_441); +x_444 = l_Lean_Elab_Term_getOpenDecls(x_2, x_443); +x_445 = lean_ctor_get(x_444, 0); +lean_inc(x_445); +x_446 = lean_ctor_get(x_444, 1); +lean_inc(x_446); +lean_dec(x_444); +lean_inc(x_436); +x_447 = l_Lean_Elab_resolveGlobalName(x_439, x_442, x_445, x_436); +lean_dec(x_442); +x_448 = l_List_append___rarg(x_447, x_437); +x_449 = l___private_Init_Lean_Elab_Quotation_1__quoteName___main(x_436); +x_450 = l_Lean_Elab_Term_getCurrMacroScope(x_2, x_446); +lean_dec(x_2); +x_451 = lean_ctor_get(x_450, 0); +lean_inc(x_451); +x_452 = lean_ctor_get(x_450, 1); +lean_inc(x_452); +if (lean_is_exclusive(x_450)) { + lean_ctor_release(x_450, 0); + lean_ctor_release(x_450, 1); + x_453 = x_450; } else { - lean_dec_ref(x_434); - x_437 = lean_box(0); + lean_dec_ref(x_450); + x_453 = lean_box(0); } -x_438 = lean_box(0); -x_439 = lean_box(0); -x_440 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__38; -lean_inc(x_435); -x_441 = l_Lean_addMacroScopeExt(x_439, x_440, x_435); -x_442 = lean_box(0); -x_443 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__37; -x_444 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__41; -x_445 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_445, 0, x_438); -lean_ctor_set(x_445, 1, x_443); -lean_ctor_set(x_445, 2, x_441); -lean_ctor_set(x_445, 3, x_444); -x_446 = l_Array_empty___closed__1; -x_447 = lean_array_push(x_446, x_445); -x_448 = l___private_Init_Lean_Elab_Term_5__expandCDot___closed__4; -x_449 = lean_array_push(x_447, x_448); -x_450 = l_Lean_mkTermIdFromIdent___closed__2; -x_451 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_451, 0, x_450); -lean_ctor_set(x_451, 1, x_449); -x_452 = lean_array_push(x_446, x_451); -x_453 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__32; -lean_inc(x_435); -x_454 = l_Lean_addMacroScopeExt(x_439, x_453, x_435); -x_455 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31; -x_456 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__34; -x_457 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_457, 0, x_438); -lean_ctor_set(x_457, 1, x_455); -lean_ctor_set(x_457, 2, x_454); -lean_ctor_set(x_457, 3, x_456); -x_458 = lean_array_push(x_446, x_457); -x_459 = lean_array_push(x_458, x_448); -x_460 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_460, 0, x_450); -lean_ctor_set(x_460, 1, x_459); -x_461 = lean_array_push(x_446, x_460); -x_462 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__47; -lean_inc(x_435); -x_463 = l_Lean_addMacroScopeExt(x_439, x_462, x_435); -x_464 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__46; -x_465 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__50; -x_466 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_466, 0, x_438); -lean_ctor_set(x_466, 1, x_464); -lean_ctor_set(x_466, 2, x_463); -lean_ctor_set(x_466, 3, x_465); -x_467 = lean_array_push(x_446, x_466); -x_468 = lean_array_push(x_467, x_448); -x_469 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_469, 0, x_450); -lean_ctor_set(x_469, 1, x_468); -x_470 = lean_array_push(x_446, x_469); -x_471 = lean_array_push(x_446, x_433); -x_472 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__54; -x_473 = l_Lean_addMacroScopeExt(x_439, x_472, x_435); -x_474 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__53; -x_475 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_475, 0, x_438); -lean_ctor_set(x_475, 1, x_474); -lean_ctor_set(x_475, 2, x_473); -lean_ctor_set(x_475, 3, x_442); -x_476 = lean_array_push(x_446, x_475); -x_477 = lean_array_push(x_476, x_448); -x_478 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_478, 0, x_450); -lean_ctor_set(x_478, 1, x_477); -x_479 = lean_array_push(x_471, x_478); -x_480 = l_Lean_nullKind___closed__2; -x_481 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_481, 0, x_480); -lean_ctor_set(x_481, 1, x_479); -x_482 = lean_array_push(x_470, x_481); -x_483 = l_Lean_mkAppStx___closed__8; -x_484 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_484, 0, x_483); -lean_ctor_set(x_484, 1, x_482); -x_485 = lean_array_push(x_446, x_484); -x_486 = lean_array_push(x_485, x_448); -x_487 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_487, 0, x_480); -lean_ctor_set(x_487, 1, x_486); -x_488 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; -x_489 = lean_array_push(x_488, x_487); -x_490 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; -x_491 = lean_array_push(x_489, x_490); -x_492 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; +x_454 = lean_box(0); +x_455 = lean_box(0); +x_456 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__38; +lean_inc(x_451); +x_457 = l_Lean_addMacroScopeExt(x_455, x_456, x_451); +x_458 = lean_box(0); +x_459 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__37; +x_460 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__41; +x_461 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_461, 0, x_454); +lean_ctor_set(x_461, 1, x_459); +lean_ctor_set(x_461, 2, x_457); +lean_ctor_set(x_461, 3, x_460); +x_462 = l_Array_empty___closed__1; +x_463 = lean_array_push(x_462, x_461); +x_464 = l___private_Init_Lean_Elab_Term_5__expandCDot___closed__4; +x_465 = lean_array_push(x_463, x_464); +x_466 = l_Lean_mkTermIdFromIdent___closed__2; +x_467 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_467, 0, x_466); +lean_ctor_set(x_467, 1, x_465); +x_468 = lean_array_push(x_462, x_467); +x_469 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__32; +lean_inc(x_451); +x_470 = l_Lean_addMacroScopeExt(x_455, x_469, x_451); +x_471 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31; +x_472 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__34; +x_473 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_473, 0, x_454); +lean_ctor_set(x_473, 1, x_471); +lean_ctor_set(x_473, 2, x_470); +lean_ctor_set(x_473, 3, x_472); +x_474 = lean_array_push(x_462, x_473); +x_475 = lean_array_push(x_474, x_464); +x_476 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_476, 0, x_466); +lean_ctor_set(x_476, 1, x_475); +x_477 = lean_array_push(x_462, x_476); +x_478 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__47; +lean_inc(x_451); +x_479 = l_Lean_addMacroScopeExt(x_455, x_478, x_451); +x_480 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__46; +x_481 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__50; +x_482 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_482, 0, x_454); +lean_ctor_set(x_482, 1, x_480); +lean_ctor_set(x_482, 2, x_479); +lean_ctor_set(x_482, 3, x_481); +x_483 = lean_array_push(x_462, x_482); +x_484 = lean_array_push(x_483, x_464); +x_485 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_485, 0, x_466); +lean_ctor_set(x_485, 1, x_484); +x_486 = lean_array_push(x_462, x_485); +x_487 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__54; +lean_inc(x_451); +x_488 = l_Lean_addMacroScopeExt(x_455, x_487, x_451); +x_489 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__53; +x_490 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_490, 0, x_454); +lean_ctor_set(x_490, 1, x_489); +lean_ctor_set(x_490, 2, x_488); +lean_ctor_set(x_490, 3, x_458); +x_491 = lean_array_push(x_462, x_490); +x_492 = lean_array_push(x_491, x_464); x_493 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_493, 0, x_492); -lean_ctor_set(x_493, 1, x_491); -x_494 = l___private_Init_Lean_Elab_Quotation_2__quoteList___main___at___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___spec__2(x_432); -x_495 = lean_ctor_get(x_419, 0); -lean_inc(x_495); -x_496 = lean_ctor_get(x_419, 1); -lean_inc(x_496); -x_497 = lean_ctor_get(x_419, 2); -lean_inc(x_497); -lean_dec(x_419); -x_498 = lean_string_utf8_extract(x_495, x_496, x_497); -lean_dec(x_497); -lean_dec(x_496); -lean_dec(x_495); -x_499 = l_Lean_mkStxStrLit(x_498, x_438); -x_500 = l_Lean_mkOptionalNode___closed__2; -x_501 = lean_array_push(x_500, x_499); -x_502 = l_Lean_Parser_Term_str___elambda__1___closed__2; -x_503 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_503, 0, x_502); -lean_ctor_set(x_503, 1, x_501); -x_504 = lean_array_push(x_500, x_503); -x_505 = l_Lean_Substring_HasQuote___closed__2; -x_506 = l_Lean_mkCAppStx(x_505, x_504); -x_507 = lean_array_push(x_461, x_506); -x_508 = lean_array_push(x_507, x_493); -x_509 = lean_array_push(x_508, x_494); -x_510 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_510, 0, x_480); -lean_ctor_set(x_510, 1, x_509); -x_511 = lean_array_push(x_452, x_510); -x_512 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_512, 0, x_483); -lean_ctor_set(x_512, 1, x_511); -if (lean_is_scalar(x_437)) { - x_513 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_493, 0, x_466); +lean_ctor_set(x_493, 1, x_492); +x_494 = lean_array_push(x_462, x_493); +x_495 = lean_array_push(x_494, x_449); +x_496 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58; +x_497 = l_Lean_addMacroScopeExt(x_455, x_496, x_451); +x_498 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__57; +x_499 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_499, 0, x_454); +lean_ctor_set(x_499, 1, x_498); +lean_ctor_set(x_499, 2, x_497); +lean_ctor_set(x_499, 3, x_458); +x_500 = lean_array_push(x_462, x_499); +x_501 = lean_array_push(x_500, x_464); +x_502 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_502, 0, x_466); +lean_ctor_set(x_502, 1, x_501); +x_503 = lean_array_push(x_495, x_502); +x_504 = l_Lean_nullKind___closed__2; +x_505 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_505, 0, x_504); +lean_ctor_set(x_505, 1, x_503); +x_506 = lean_array_push(x_486, x_505); +x_507 = l_Lean_mkAppStx___closed__8; +x_508 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_508, 0, x_507); +lean_ctor_set(x_508, 1, x_506); +x_509 = lean_array_push(x_462, x_508); +x_510 = lean_array_push(x_509, x_464); +x_511 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_511, 0, x_504); +lean_ctor_set(x_511, 1, x_510); +x_512 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; +x_513 = lean_array_push(x_512, x_511); +x_514 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; +x_515 = lean_array_push(x_513, x_514); +x_516 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; +x_517 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_517, 0, x_516); +lean_ctor_set(x_517, 1, x_515); +x_518 = l___private_Init_Lean_Elab_Quotation_2__quoteList___main___at___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___spec__2(x_448); +x_519 = lean_ctor_get(x_435, 0); +lean_inc(x_519); +x_520 = lean_ctor_get(x_435, 1); +lean_inc(x_520); +x_521 = lean_ctor_get(x_435, 2); +lean_inc(x_521); +lean_dec(x_435); +x_522 = lean_string_utf8_extract(x_519, x_520, x_521); +lean_dec(x_521); +lean_dec(x_520); +lean_dec(x_519); +x_523 = l_Lean_mkStxStrLit(x_522, x_454); +x_524 = l_Lean_mkOptionalNode___closed__2; +x_525 = lean_array_push(x_524, x_523); +x_526 = l_Lean_Parser_Term_str___elambda__1___closed__2; +x_527 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_527, 0, x_526); +lean_ctor_set(x_527, 1, x_525); +x_528 = lean_array_push(x_524, x_527); +x_529 = l_Lean_Substring_HasQuote___closed__2; +x_530 = l_Lean_mkCAppStx(x_529, x_528); +x_531 = lean_array_push(x_477, x_530); +x_532 = lean_array_push(x_531, x_517); +x_533 = lean_array_push(x_532, x_518); +x_534 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_534, 0, x_504); +lean_ctor_set(x_534, 1, x_533); +x_535 = lean_array_push(x_468, x_534); +x_536 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_536, 0, x_507); +lean_ctor_set(x_536, 1, x_535); +if (lean_is_scalar(x_453)) { + x_537 = lean_alloc_ctor(0, 2, 0); } else { - x_513 = x_437; + x_537 = x_453; } -lean_ctor_set(x_513, 0, x_512); -lean_ctor_set(x_513, 1, x_436); -return x_513; +lean_ctor_set(x_537, 0, x_536); +lean_ctor_set(x_537, 1, x_452); +return x_537; } } } @@ -3787,7 +3884,7 @@ lean_object* _init_l_Lean_Elab_Term_stxQuot_expand___closed__19() { _start: { lean_object* x_1; -x_1 = lean_mk_string("pure"); +x_1 = lean_mk_string("getMainModule"); return x_1; } } @@ -3827,9 +3924,11 @@ return x_3; lean_object* _init_l_Lean_Elab_Term_stxQuot_expand___closed__23() { _start: { -lean_object* x_1; -x_1 = lean_mk_string("HasPure"); -return x_1; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Term_stxQuot_expand___closed__15; +x_2 = l_Lean_Elab_Term_stxQuot_expand___closed__19; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; } } lean_object* _init_l_Lean_Elab_Term_stxQuot_expand___closed__24() { @@ -3838,7 +3937,9 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); x_2 = l_Lean_Elab_Term_stxQuot_expand___closed__23; -x_3 = lean_name_mk_string(x_1, x_2); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_2); +lean_ctor_set(x_3, 1, x_1); return x_3; } } @@ -3846,30 +3947,101 @@ lean_object* _init_l_Lean_Elab_Term_stxQuot_expand___closed__25() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Term_stxQuot_expand___closed__24; -x_2 = l_Lean_Elab_Term_stxQuot_expand___closed__19; -x_3 = lean_name_mk_string(x_1, x_2); +x_1 = lean_box(0); +x_2 = l_Lean_Elab_Term_stxQuot_expand___closed__24; +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_Elab_Term_stxQuot_expand___closed__26() { _start: { +lean_object* x_1; +x_1 = lean_mk_string("pure"); +return x_1; +} +} +lean_object* _init_l_Lean_Elab_Term_stxQuot_expand___closed__27() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Elab_Term_stxQuot_expand___closed__26; +x_2 = lean_string_utf8_byte_size(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Elab_Term_stxQuot_expand___closed__28() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Elab_Term_stxQuot_expand___closed__26; +x_2 = lean_unsigned_to_nat(0u); +x_3 = l_Lean_Elab_Term_stxQuot_expand___closed__27; +x_4 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Elab_Term_stxQuot_expand___closed__29() { +_start: +{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Elab_Term_stxQuot_expand___closed__25; +x_2 = l_Lean_Elab_Term_stxQuot_expand___closed__26; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Elab_Term_stxQuot_expand___closed__30() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("HasPure"); +return x_1; +} +} +lean_object* _init_l_Lean_Elab_Term_stxQuot_expand___closed__31() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Elab_Term_stxQuot_expand___closed__30; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Elab_Term_stxQuot_expand___closed__32() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Term_stxQuot_expand___closed__31; +x_2 = l_Lean_Elab_Term_stxQuot_expand___closed__26; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Elab_Term_stxQuot_expand___closed__33() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Elab_Term_stxQuot_expand___closed__32; x_3 = lean_alloc_ctor(0, 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_Elab_Term_stxQuot_expand___closed__27() { +lean_object* _init_l_Lean_Elab_Term_stxQuot_expand___closed__34() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Elab_Term_stxQuot_expand___closed__26; +x_2 = l_Lean_Elab_Term_stxQuot_expand___closed__33; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); @@ -3898,7 +4070,7 @@ lean_dec(x_2); x_11 = !lean_is_exclusive(x_10); if (x_11 == 0) { -lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; +lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; x_12 = lean_ctor_get(x_10, 0); x_13 = lean_box(0); x_14 = lean_box(0); @@ -3938,10 +4110,10 @@ x_35 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_35, 0, x_25); lean_ctor_set(x_35, 1, x_34); x_36 = lean_array_push(x_21, x_35); -x_37 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__54; +x_37 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58; lean_inc(x_12); x_38 = l_Lean_addMacroScopeExt(x_14, x_37, x_12); -x_39 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__53; +x_39 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__57; x_40 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_40, 0, x_13); lean_ctor_set(x_40, 1, x_39); @@ -3962,9 +4134,10 @@ x_48 = lean_array_push(x_47, x_46); x_49 = l_Lean_Elab_Term_expandCDot_x3f___closed__3; x_50 = lean_array_push(x_48, x_49); x_51 = l_Lean_Elab_Term_stxQuot_expand___closed__22; +lean_inc(x_12); x_52 = l_Lean_addMacroScopeExt(x_14, x_51, x_12); x_53 = l_Lean_Elab_Term_stxQuot_expand___closed__21; -x_54 = l_Lean_Elab_Term_stxQuot_expand___closed__27; +x_54 = l_Lean_Elab_Term_stxQuot_expand___closed__25; x_55 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_55, 0, x_13); lean_ctor_set(x_55, 1, x_53); @@ -3976,190 +4149,307 @@ x_58 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_58, 0, x_25); lean_ctor_set(x_58, 1, x_57); x_59 = lean_array_push(x_21, x_58); -x_60 = lean_array_push(x_21, x_8); -x_61 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_61, 0, x_45); -lean_ctor_set(x_61, 1, x_60); -x_62 = lean_array_push(x_59, x_61); -x_63 = l_Lean_mkAppStx___closed__8; -x_64 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_64, 0, x_63); -lean_ctor_set(x_64, 1, x_62); -x_65 = lean_array_push(x_50, x_64); -x_66 = l_Lean_Parser_Term_fun___elambda__1___closed__2; -x_67 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_67, 0, x_66); -lean_ctor_set(x_67, 1, x_65); -x_68 = lean_array_push(x_21, x_67); -x_69 = lean_array_push(x_68, x_23); -x_70 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_70, 0, x_45); -lean_ctor_set(x_70, 1, x_69); -x_71 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; -x_72 = lean_array_push(x_71, x_70); -x_73 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; -x_74 = lean_array_push(x_72, x_73); -x_75 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; -x_76 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_76, 0, x_75); -lean_ctor_set(x_76, 1, x_74); -x_77 = lean_array_push(x_36, x_76); +x_60 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__54; +lean_inc(x_12); +x_61 = l_Lean_addMacroScopeExt(x_14, x_60, x_12); +x_62 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__53; +x_63 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_63, 0, x_13); +lean_ctor_set(x_63, 1, x_62); +lean_ctor_set(x_63, 2, x_61); +lean_ctor_set(x_63, 3, x_17); +x_64 = lean_array_push(x_21, x_63); +x_65 = lean_array_push(x_64, x_23); +x_66 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_66, 0, x_25); +lean_ctor_set(x_66, 1, x_65); +x_67 = lean_array_push(x_21, x_66); +x_68 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_68, 0, x_45); +lean_ctor_set(x_68, 1, x_67); +x_69 = lean_array_push(x_47, x_68); +x_70 = lean_array_push(x_69, x_49); +x_71 = l_Lean_Elab_Term_stxQuot_expand___closed__29; +x_72 = l_Lean_addMacroScopeExt(x_14, x_71, x_12); +x_73 = l_Lean_Elab_Term_stxQuot_expand___closed__28; +x_74 = l_Lean_Elab_Term_stxQuot_expand___closed__34; +x_75 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_75, 0, x_13); +lean_ctor_set(x_75, 1, x_73); +lean_ctor_set(x_75, 2, x_72); +lean_ctor_set(x_75, 3, x_74); +x_76 = lean_array_push(x_21, x_75); +x_77 = lean_array_push(x_76, x_23); x_78 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_78, 0, x_45); +lean_ctor_set(x_78, 0, x_25); lean_ctor_set(x_78, 1, x_77); -x_79 = lean_array_push(x_27, x_78); -x_80 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_80, 0, x_63); -lean_ctor_set(x_80, 1, x_79); -lean_ctor_set(x_10, 0, x_80); +x_79 = lean_array_push(x_21, x_78); +x_80 = lean_array_push(x_21, x_8); +x_81 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_81, 0, x_45); +lean_ctor_set(x_81, 1, x_80); +x_82 = lean_array_push(x_79, x_81); +x_83 = l_Lean_mkAppStx___closed__8; +x_84 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_84, 0, x_83); +lean_ctor_set(x_84, 1, x_82); +x_85 = lean_array_push(x_70, x_84); +x_86 = l_Lean_Parser_Term_fun___elambda__1___closed__2; +x_87 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_87, 0, x_86); +lean_ctor_set(x_87, 1, x_85); +x_88 = lean_array_push(x_21, x_87); +x_89 = lean_array_push(x_88, x_23); +x_90 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_90, 0, x_45); +lean_ctor_set(x_90, 1, x_89); +x_91 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; +x_92 = lean_array_push(x_91, x_90); +x_93 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; +x_94 = lean_array_push(x_92, x_93); +x_95 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; +x_96 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_96, 0, x_95); +lean_ctor_set(x_96, 1, x_94); +x_97 = lean_array_push(x_59, x_96); +x_98 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_98, 0, x_45); +lean_ctor_set(x_98, 1, x_97); +lean_inc(x_27); +x_99 = lean_array_push(x_27, x_98); +x_100 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_100, 0, x_83); +lean_ctor_set(x_100, 1, x_99); +x_101 = lean_array_push(x_50, x_100); +x_102 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_102, 0, x_86); +lean_ctor_set(x_102, 1, x_101); +x_103 = lean_array_push(x_21, x_102); +x_104 = lean_array_push(x_103, x_23); +x_105 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_105, 0, x_45); +lean_ctor_set(x_105, 1, x_104); +x_106 = lean_array_push(x_91, x_105); +x_107 = lean_array_push(x_106, x_93); +x_108 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_108, 0, x_95); +lean_ctor_set(x_108, 1, x_107); +x_109 = lean_array_push(x_36, x_108); +x_110 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_110, 0, x_45); +lean_ctor_set(x_110, 1, x_109); +x_111 = lean_array_push(x_27, x_110); +x_112 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_112, 0, x_83); +lean_ctor_set(x_112, 1, x_111); +lean_ctor_set(x_10, 0, x_112); return x_10; } else { -lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; -x_81 = lean_ctor_get(x_10, 0); -x_82 = lean_ctor_get(x_10, 1); -lean_inc(x_82); -lean_inc(x_81); +lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172; lean_object* x_173; lean_object* x_174; lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; lean_object* x_186; lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; lean_object* x_191; lean_object* x_192; lean_object* x_193; lean_object* x_194; lean_object* x_195; lean_object* x_196; lean_object* x_197; lean_object* x_198; lean_object* x_199; lean_object* x_200; lean_object* x_201; lean_object* x_202; lean_object* x_203; lean_object* x_204; lean_object* x_205; lean_object* x_206; lean_object* x_207; lean_object* x_208; lean_object* x_209; lean_object* x_210; lean_object* x_211; lean_object* x_212; lean_object* x_213; lean_object* x_214; lean_object* x_215; +x_113 = lean_ctor_get(x_10, 0); +x_114 = lean_ctor_get(x_10, 1); +lean_inc(x_114); +lean_inc(x_113); lean_dec(x_10); -x_83 = lean_box(0); -x_84 = lean_box(0); -x_85 = l_Lean_Elab_Term_stxQuot_expand___closed__4; -lean_inc(x_81); -x_86 = l_Lean_addMacroScopeExt(x_84, x_85, x_81); -x_87 = lean_box(0); -x_88 = l_Lean_Elab_Term_stxQuot_expand___closed__3; -x_89 = l_Lean_Elab_Term_stxQuot_expand___closed__9; -x_90 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_90, 0, x_83); -lean_ctor_set(x_90, 1, x_88); -lean_ctor_set(x_90, 2, x_86); -lean_ctor_set(x_90, 3, x_89); -x_91 = l_Array_empty___closed__1; -x_92 = lean_array_push(x_91, x_90); -x_93 = l___private_Init_Lean_Elab_Term_5__expandCDot___closed__4; -x_94 = lean_array_push(x_92, x_93); -x_95 = l_Lean_mkTermIdFromIdent___closed__2; -x_96 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_96, 0, x_95); -lean_ctor_set(x_96, 1, x_94); -x_97 = lean_array_push(x_91, x_96); -x_98 = l_Lean_Elab_Term_stxQuot_expand___closed__13; -lean_inc(x_81); -x_99 = l_Lean_addMacroScopeExt(x_84, x_98, x_81); -x_100 = l_Lean_Elab_Term_stxQuot_expand___closed__12; -x_101 = l_Lean_Elab_Term_stxQuot_expand___closed__18; -x_102 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_102, 0, x_83); -lean_ctor_set(x_102, 1, x_100); -lean_ctor_set(x_102, 2, x_99); -lean_ctor_set(x_102, 3, x_101); -x_103 = lean_array_push(x_91, x_102); -x_104 = lean_array_push(x_103, x_93); -x_105 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_105, 0, x_95); -lean_ctor_set(x_105, 1, x_104); -x_106 = lean_array_push(x_91, x_105); -x_107 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__54; -lean_inc(x_81); -x_108 = l_Lean_addMacroScopeExt(x_84, x_107, x_81); -x_109 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__53; -x_110 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_110, 0, x_83); -lean_ctor_set(x_110, 1, x_109); -lean_ctor_set(x_110, 2, x_108); -lean_ctor_set(x_110, 3, x_87); -x_111 = lean_array_push(x_91, x_110); -x_112 = lean_array_push(x_111, x_93); -x_113 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_113, 0, x_95); -lean_ctor_set(x_113, 1, x_112); -x_114 = lean_array_push(x_91, x_113); -x_115 = l_Lean_nullKind___closed__2; -x_116 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_116, 0, x_115); -lean_ctor_set(x_116, 1, x_114); -x_117 = l_Lean_Elab_Term_expandCDot_x3f___closed__2; -x_118 = lean_array_push(x_117, x_116); -x_119 = l_Lean_Elab_Term_expandCDot_x3f___closed__3; -x_120 = lean_array_push(x_118, x_119); -x_121 = l_Lean_Elab_Term_stxQuot_expand___closed__22; -x_122 = l_Lean_addMacroScopeExt(x_84, x_121, x_81); -x_123 = l_Lean_Elab_Term_stxQuot_expand___closed__21; -x_124 = l_Lean_Elab_Term_stxQuot_expand___closed__27; -x_125 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_125, 0, x_83); -lean_ctor_set(x_125, 1, x_123); -lean_ctor_set(x_125, 2, x_122); -lean_ctor_set(x_125, 3, x_124); -x_126 = lean_array_push(x_91, x_125); -x_127 = lean_array_push(x_126, x_93); +x_115 = lean_box(0); +x_116 = lean_box(0); +x_117 = l_Lean_Elab_Term_stxQuot_expand___closed__4; +lean_inc(x_113); +x_118 = l_Lean_addMacroScopeExt(x_116, x_117, x_113); +x_119 = lean_box(0); +x_120 = l_Lean_Elab_Term_stxQuot_expand___closed__3; +x_121 = l_Lean_Elab_Term_stxQuot_expand___closed__9; +x_122 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_122, 0, x_115); +lean_ctor_set(x_122, 1, x_120); +lean_ctor_set(x_122, 2, x_118); +lean_ctor_set(x_122, 3, x_121); +x_123 = l_Array_empty___closed__1; +x_124 = lean_array_push(x_123, x_122); +x_125 = l___private_Init_Lean_Elab_Term_5__expandCDot___closed__4; +x_126 = lean_array_push(x_124, x_125); +x_127 = l_Lean_mkTermIdFromIdent___closed__2; x_128 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_128, 0, x_95); -lean_ctor_set(x_128, 1, x_127); -x_129 = lean_array_push(x_91, x_128); -x_130 = lean_array_push(x_91, x_8); -x_131 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_131, 0, x_115); -lean_ctor_set(x_131, 1, x_130); -x_132 = lean_array_push(x_129, x_131); -x_133 = l_Lean_mkAppStx___closed__8; -x_134 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_134, 0, x_133); +lean_ctor_set(x_128, 0, x_127); +lean_ctor_set(x_128, 1, x_126); +x_129 = lean_array_push(x_123, x_128); +x_130 = l_Lean_Elab_Term_stxQuot_expand___closed__13; +lean_inc(x_113); +x_131 = l_Lean_addMacroScopeExt(x_116, x_130, x_113); +x_132 = l_Lean_Elab_Term_stxQuot_expand___closed__12; +x_133 = l_Lean_Elab_Term_stxQuot_expand___closed__18; +x_134 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_134, 0, x_115); lean_ctor_set(x_134, 1, x_132); -x_135 = lean_array_push(x_120, x_134); -x_136 = l_Lean_Parser_Term_fun___elambda__1___closed__2; +lean_ctor_set(x_134, 2, x_131); +lean_ctor_set(x_134, 3, x_133); +x_135 = lean_array_push(x_123, x_134); +x_136 = lean_array_push(x_135, x_125); x_137 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_137, 0, x_136); -lean_ctor_set(x_137, 1, x_135); -x_138 = lean_array_push(x_91, x_137); -x_139 = lean_array_push(x_138, x_93); -x_140 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_140, 0, x_115); -lean_ctor_set(x_140, 1, x_139); -x_141 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; -x_142 = lean_array_push(x_141, x_140); -x_143 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; -x_144 = lean_array_push(x_142, x_143); -x_145 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; -x_146 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_146, 0, x_145); -lean_ctor_set(x_146, 1, x_144); -x_147 = lean_array_push(x_106, x_146); +lean_ctor_set(x_137, 0, x_127); +lean_ctor_set(x_137, 1, x_136); +x_138 = lean_array_push(x_123, x_137); +x_139 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58; +lean_inc(x_113); +x_140 = l_Lean_addMacroScopeExt(x_116, x_139, x_113); +x_141 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__57; +x_142 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_142, 0, x_115); +lean_ctor_set(x_142, 1, x_141); +lean_ctor_set(x_142, 2, x_140); +lean_ctor_set(x_142, 3, x_119); +x_143 = lean_array_push(x_123, x_142); +x_144 = lean_array_push(x_143, x_125); +x_145 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_145, 0, x_127); +lean_ctor_set(x_145, 1, x_144); +x_146 = lean_array_push(x_123, x_145); +x_147 = l_Lean_nullKind___closed__2; x_148 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_148, 0, x_115); -lean_ctor_set(x_148, 1, x_147); -x_149 = lean_array_push(x_97, x_148); -x_150 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_150, 0, x_133); -lean_ctor_set(x_150, 1, x_149); -x_151 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_151, 0, x_150); -lean_ctor_set(x_151, 1, x_82); -return x_151; +lean_ctor_set(x_148, 0, x_147); +lean_ctor_set(x_148, 1, x_146); +x_149 = l_Lean_Elab_Term_expandCDot_x3f___closed__2; +x_150 = lean_array_push(x_149, x_148); +x_151 = l_Lean_Elab_Term_expandCDot_x3f___closed__3; +x_152 = lean_array_push(x_150, x_151); +x_153 = l_Lean_Elab_Term_stxQuot_expand___closed__22; +lean_inc(x_113); +x_154 = l_Lean_addMacroScopeExt(x_116, x_153, x_113); +x_155 = l_Lean_Elab_Term_stxQuot_expand___closed__21; +x_156 = l_Lean_Elab_Term_stxQuot_expand___closed__25; +x_157 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_157, 0, x_115); +lean_ctor_set(x_157, 1, x_155); +lean_ctor_set(x_157, 2, x_154); +lean_ctor_set(x_157, 3, x_156); +x_158 = lean_array_push(x_123, x_157); +x_159 = lean_array_push(x_158, x_125); +x_160 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_160, 0, x_127); +lean_ctor_set(x_160, 1, x_159); +x_161 = lean_array_push(x_123, x_160); +x_162 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__54; +lean_inc(x_113); +x_163 = l_Lean_addMacroScopeExt(x_116, x_162, x_113); +x_164 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__53; +x_165 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_165, 0, x_115); +lean_ctor_set(x_165, 1, x_164); +lean_ctor_set(x_165, 2, x_163); +lean_ctor_set(x_165, 3, x_119); +x_166 = lean_array_push(x_123, x_165); +x_167 = lean_array_push(x_166, x_125); +x_168 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_168, 0, x_127); +lean_ctor_set(x_168, 1, x_167); +x_169 = lean_array_push(x_123, x_168); +x_170 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_170, 0, x_147); +lean_ctor_set(x_170, 1, x_169); +x_171 = lean_array_push(x_149, x_170); +x_172 = lean_array_push(x_171, x_151); +x_173 = l_Lean_Elab_Term_stxQuot_expand___closed__29; +x_174 = l_Lean_addMacroScopeExt(x_116, x_173, x_113); +x_175 = l_Lean_Elab_Term_stxQuot_expand___closed__28; +x_176 = l_Lean_Elab_Term_stxQuot_expand___closed__34; +x_177 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_177, 0, x_115); +lean_ctor_set(x_177, 1, x_175); +lean_ctor_set(x_177, 2, x_174); +lean_ctor_set(x_177, 3, x_176); +x_178 = lean_array_push(x_123, x_177); +x_179 = lean_array_push(x_178, x_125); +x_180 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_180, 0, x_127); +lean_ctor_set(x_180, 1, x_179); +x_181 = lean_array_push(x_123, x_180); +x_182 = lean_array_push(x_123, x_8); +x_183 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_183, 0, x_147); +lean_ctor_set(x_183, 1, x_182); +x_184 = lean_array_push(x_181, x_183); +x_185 = l_Lean_mkAppStx___closed__8; +x_186 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_186, 0, x_185); +lean_ctor_set(x_186, 1, x_184); +x_187 = lean_array_push(x_172, x_186); +x_188 = l_Lean_Parser_Term_fun___elambda__1___closed__2; +x_189 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_189, 0, x_188); +lean_ctor_set(x_189, 1, x_187); +x_190 = lean_array_push(x_123, x_189); +x_191 = lean_array_push(x_190, x_125); +x_192 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_192, 0, x_147); +lean_ctor_set(x_192, 1, x_191); +x_193 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; +x_194 = lean_array_push(x_193, x_192); +x_195 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; +x_196 = lean_array_push(x_194, x_195); +x_197 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; +x_198 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_198, 0, x_197); +lean_ctor_set(x_198, 1, x_196); +x_199 = lean_array_push(x_161, x_198); +x_200 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_200, 0, x_147); +lean_ctor_set(x_200, 1, x_199); +lean_inc(x_129); +x_201 = lean_array_push(x_129, x_200); +x_202 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_202, 0, x_185); +lean_ctor_set(x_202, 1, x_201); +x_203 = lean_array_push(x_152, x_202); +x_204 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_204, 0, x_188); +lean_ctor_set(x_204, 1, x_203); +x_205 = lean_array_push(x_123, x_204); +x_206 = lean_array_push(x_205, x_125); +x_207 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_207, 0, x_147); +lean_ctor_set(x_207, 1, x_206); +x_208 = lean_array_push(x_193, x_207); +x_209 = lean_array_push(x_208, x_195); +x_210 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_210, 0, x_197); +lean_ctor_set(x_210, 1, x_209); +x_211 = lean_array_push(x_138, x_210); +x_212 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_212, 0, x_147); +lean_ctor_set(x_212, 1, x_211); +x_213 = lean_array_push(x_129, x_212); +x_214 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_214, 0, x_185); +lean_ctor_set(x_214, 1, x_213); +x_215 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_215, 0, x_214); +lean_ctor_set(x_215, 1, x_114); +return x_215; } } else { -uint8_t x_152; +uint8_t x_216; lean_dec(x_2); -x_152 = !lean_is_exclusive(x_7); -if (x_152 == 0) +x_216 = !lean_is_exclusive(x_7); +if (x_216 == 0) { return x_7; } else { -lean_object* x_153; lean_object* x_154; lean_object* x_155; -x_153 = lean_ctor_get(x_7, 0); -x_154 = lean_ctor_get(x_7, 1); -lean_inc(x_154); -lean_inc(x_153); +lean_object* x_217; lean_object* x_218; lean_object* x_219; +x_217 = lean_ctor_get(x_7, 0); +x_218 = lean_ctor_get(x_7, 1); +lean_inc(x_218); +lean_inc(x_217); lean_dec(x_7); -x_155 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_155, 0, x_153); -lean_ctor_set(x_155, 1, x_154); -return x_155; +x_219 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_219, 0, x_217); +lean_ctor_set(x_219, 1, x_218); +return x_219; } } } @@ -9247,7 +9537,7 @@ lean_ctor_set(x_650, 0, x_619); lean_ctor_set(x_650, 1, x_649); x_651 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_652 = lean_array_push(x_651, x_650); -x_653 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_653 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_654 = lean_array_push(x_652, x_653); x_655 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_656 = lean_alloc_ctor(1, 2, 0); @@ -9605,7 +9895,7 @@ lean_ctor_set(x_837, 0, x_806); lean_ctor_set(x_837, 1, x_836); x_838 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_839 = lean_array_push(x_838, x_837); -x_840 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_840 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_841 = lean_array_push(x_839, x_840); x_842 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_843 = lean_alloc_ctor(1, 2, 0); @@ -10117,7 +10407,7 @@ lean_ctor_set(x_1046, 0, x_1015); lean_ctor_set(x_1046, 1, x_1045); x_1047 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43; x_1048 = lean_array_push(x_1047, x_1046); -x_1049 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_1049 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_1050 = lean_array_push(x_1048, x_1049); x_1051 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2; x_1052 = lean_alloc_ctor(1, 2, 0); @@ -11286,7 +11576,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__5; -x_2 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_2 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_3 = lean_array_push(x_1, x_2); return x_3; } @@ -25260,6 +25550,14 @@ l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__54 = _init_ lean_mark_persistent(l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__54); l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55 = _init_l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55(); lean_mark_persistent(l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55); +l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56 = _init_l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56(); +lean_mark_persistent(l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56); +l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__57 = _init_l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__57(); +lean_mark_persistent(l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__57); +l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58 = _init_l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58(); +lean_mark_persistent(l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58); +l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59 = _init_l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59(); +lean_mark_persistent(l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59); l_Lean_Elab_Term_stxQuot_expand___closed__1 = _init_l_Lean_Elab_Term_stxQuot_expand___closed__1(); lean_mark_persistent(l_Lean_Elab_Term_stxQuot_expand___closed__1); l_Lean_Elab_Term_stxQuot_expand___closed__2 = _init_l_Lean_Elab_Term_stxQuot_expand___closed__2(); @@ -25314,6 +25612,20 @@ l_Lean_Elab_Term_stxQuot_expand___closed__26 = _init_l_Lean_Elab_Term_stxQuot_ex lean_mark_persistent(l_Lean_Elab_Term_stxQuot_expand___closed__26); l_Lean_Elab_Term_stxQuot_expand___closed__27 = _init_l_Lean_Elab_Term_stxQuot_expand___closed__27(); lean_mark_persistent(l_Lean_Elab_Term_stxQuot_expand___closed__27); +l_Lean_Elab_Term_stxQuot_expand___closed__28 = _init_l_Lean_Elab_Term_stxQuot_expand___closed__28(); +lean_mark_persistent(l_Lean_Elab_Term_stxQuot_expand___closed__28); +l_Lean_Elab_Term_stxQuot_expand___closed__29 = _init_l_Lean_Elab_Term_stxQuot_expand___closed__29(); +lean_mark_persistent(l_Lean_Elab_Term_stxQuot_expand___closed__29); +l_Lean_Elab_Term_stxQuot_expand___closed__30 = _init_l_Lean_Elab_Term_stxQuot_expand___closed__30(); +lean_mark_persistent(l_Lean_Elab_Term_stxQuot_expand___closed__30); +l_Lean_Elab_Term_stxQuot_expand___closed__31 = _init_l_Lean_Elab_Term_stxQuot_expand___closed__31(); +lean_mark_persistent(l_Lean_Elab_Term_stxQuot_expand___closed__31); +l_Lean_Elab_Term_stxQuot_expand___closed__32 = _init_l_Lean_Elab_Term_stxQuot_expand___closed__32(); +lean_mark_persistent(l_Lean_Elab_Term_stxQuot_expand___closed__32); +l_Lean_Elab_Term_stxQuot_expand___closed__33 = _init_l_Lean_Elab_Term_stxQuot_expand___closed__33(); +lean_mark_persistent(l_Lean_Elab_Term_stxQuot_expand___closed__33); +l_Lean_Elab_Term_stxQuot_expand___closed__34 = _init_l_Lean_Elab_Term_stxQuot_expand___closed__34(); +lean_mark_persistent(l_Lean_Elab_Term_stxQuot_expand___closed__34); l_Lean_Elab_Term_elabStxQuot___closed__1 = _init_l_Lean_Elab_Term_elabStxQuot___closed__1(); lean_mark_persistent(l_Lean_Elab_Term_elabStxQuot___closed__1); l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabStxQuot___closed__1(); diff --git a/stage0/stdlib/Init/Lean/Elab/Syntax.c b/stage0/stdlib/Init/Lean/Elab/Syntax.c index ff72b8b98e..e00a94ca4c 100644 --- a/stage0/stdlib/Init/Lean/Elab/Syntax.c +++ b/stage0/stdlib/Init/Lean/Elab/Syntax.c @@ -266,6 +266,7 @@ lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__ lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__93; lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__121; lean_object* l___private_Init_Lean_Elab_Command_6__mkTermContext(lean_object*, lean_object*, lean_object*); +extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; lean_object* l_Lean_Elab_Command_elabSyntax___closed__28; extern lean_object* l_Lean_Elab_Term_elabArrow___lambda__1___closed__6; extern lean_object* l_Lean_Parser_Term_match__syntax___elambda__1___closed__1; @@ -427,7 +428,6 @@ lean_object* l_Lean_Elab_Command_elabSyntax___closed__13; lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__57; lean_object* l___private_Init_Lean_Elab_Syntax_5__withNoPushLeading___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__122; -extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__94; lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__8; lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__65; @@ -11767,7 +11767,7 @@ lean_ctor_set(x_50, 1, x_48); x_51 = lean_array_push(x_42, x_50); x_52 = l_Lean_Elab_Command_elabNotation___lambda__1___closed__6; x_53 = lean_array_push(x_52, x_29); -x_54 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_54 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_55 = lean_array_push(x_53, x_54); x_56 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2; x_57 = lean_alloc_ctor(1, 2, 0); @@ -11843,7 +11843,7 @@ lean_ctor_set(x_96, 1, x_94); x_97 = lean_array_push(x_88, x_96); x_98 = l_Lean_Elab_Command_elabNotation___lambda__1___closed__6; x_99 = lean_array_push(x_98, x_29); -x_100 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_100 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_101 = lean_array_push(x_99, x_100); x_102 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2; x_103 = lean_alloc_ctor(1, 2, 0); @@ -12751,7 +12751,7 @@ lean_ctor_set(x_60, 1, x_58); x_61 = lean_array_push(x_52, x_60); x_62 = l_Lean_Elab_Command_elabNotation___lambda__1___closed__6; x_63 = lean_array_push(x_62, x_34); -x_64 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_64 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_65 = lean_array_push(x_63, x_64); x_66 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2; x_67 = lean_alloc_ctor(1, 2, 0); @@ -12826,7 +12826,7 @@ lean_ctor_set(x_106, 1, x_104); x_107 = lean_array_push(x_98, x_106); x_108 = l_Lean_Elab_Command_elabNotation___lambda__1___closed__6; x_109 = lean_array_push(x_108, x_34); -x_110 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_110 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_111 = lean_array_push(x_109, x_110); x_112 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2; x_113 = lean_alloc_ctor(1, 2, 0); @@ -12911,7 +12911,7 @@ lean_ctor_set(x_157, 1, x_155); x_158 = lean_array_push(x_149, x_157); x_159 = l_Lean_Elab_Command_elabNotation___lambda__1___closed__6; x_160 = lean_array_push(x_159, x_34); -x_161 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_161 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_162 = lean_array_push(x_160, x_161); x_163 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2; x_164 = lean_alloc_ctor(1, 2, 0); @@ -12981,7 +12981,7 @@ lean_ctor_set(x_200, 1, x_198); x_201 = lean_array_push(x_192, x_200); x_202 = l_Lean_Elab_Command_elabNotation___lambda__1___closed__6; x_203 = lean_array_push(x_202, x_34); -x_204 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55; +x_204 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59; x_205 = lean_array_push(x_203, x_204); x_206 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2; x_207 = lean_alloc_ctor(1, 2, 0);