From bbdf1f39eddd701867441a796dd8edcb9951c33e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 May 2020 16:15:19 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Init/LeanInit.lean | 4 +- stage0/src/Lean/Elab/Syntax.lean | 1 + stage0/src/Lean/Parser/Command.lean | 16 +- stage0/src/Lean/Parser/Parser.lean | 8 +- stage0/src/Lean/Parser/Syntax.lean | 12 +- stage0/src/Lean/Parser/Tactic.lean | 10 +- stage0/src/Lean/Parser/Term.lean | 22 +- stage0/stdlib/Init/LeanInit.c | 8 +- stage0/stdlib/Lean/Elab/Syntax.c | 4 +- stage0/stdlib/Lean/Parser/Command.c | 316 +++++----- stage0/stdlib/Lean/Parser/Level.c | 62 +- stage0/stdlib/Lean/Parser/Module.c | 19 +- stage0/stdlib/Lean/Parser/Parser.c | 210 ++++--- stage0/stdlib/Lean/Parser/Syntax.c | 181 +++--- stage0/stdlib/Lean/Parser/Tactic.c | 191 +++--- stage0/stdlib/Lean/Parser/Term.c | 575 ++++++++---------- .../stdlib/Lean/PrettyPrinter/Parenthesizer.c | 30 +- 17 files changed, 793 insertions(+), 876 deletions(-) diff --git a/stage0/src/Init/LeanInit.lean b/stage0/src/Init/LeanInit.lean index e9766bf9f7..6895bd8890 100644 --- a/stage0/src/Init/LeanInit.lean +++ b/stage0/src/Init/LeanInit.lean @@ -148,7 +148,7 @@ inductive ParserDescr | sepBy1 : ParserDescr → ParserDescr → ParserDescr | node : Name → ParserDescr → ParserDescr | trailingNode : Name → ParserDescr → ParserDescr -| symbol : String → Option Nat → ParserDescr +| symbol : String → Nat → ParserDescr | nonReservedSymbol : String → Bool → ParserDescr | numLit : ParserDescr | strLit : ParserDescr @@ -157,7 +157,7 @@ inductive ParserDescr | ident : ParserDescr | parser : Name → Nat → ParserDescr -instance ParserDescr.inhabited : Inhabited ParserDescr := ⟨ParserDescr.symbol "" none⟩ +instance ParserDescr.inhabited : Inhabited ParserDescr := ⟨ParserDescr.symbol "" 0⟩ abbrev TrailingParserDescr := ParserDescr /- Syntax -/ diff --git a/stage0/src/Lean/Elab/Syntax.lean b/stage0/src/Lean/Elab/Syntax.lean index dba38bf277..5de5d9c38d 100644 --- a/stage0/src/Lean/Elab/Syntax.lean +++ b/stage0/src/Lean/Elab/Syntax.lean @@ -102,6 +102,7 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax if ctx.leadingIdentAsSymbol && rbp?.isNone then `(ParserDescr.nonReservedSymbol $(quote atom) false) else + -- TODO: fix (quote rbp?) `(ParserDescr.symbol $(quote atom) $(quote rbp?)) | none => liftM throwUnsupportedSyntax else if kind == `Lean.Parser.Syntax.num then diff --git a/stage0/src/Lean/Parser/Command.lean b/stage0/src/Lean/Parser/Command.lean index d636427401..5a4bcd658a 100644 --- a/stage0/src/Lean/Parser/Command.lean +++ b/stage0/src/Lean/Parser/Command.lean @@ -54,15 +54,15 @@ def «constant» := parser! "constant " >> declId >> declSig >> optional d def «instance» := parser! "instance " >> optional declId >> declSig >> declVal def «axiom» := parser! "axiom " >> declId >> declSig def «example» := parser! "example " >> declSig >> declVal -def inferMod := parser! try ("{" >> "}") +def inferMod := parser! try (symbol "{" appPrec >> "}") def introRule := parser! " | " >> ident >> optional inferMod >> optDeclSig def «inductive» := parser! "inductive " >> declId >> optDeclSig >> many introRule def classInductive := parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many introRule -def structExplicitBinder := parser! "(" >> many ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")" -def structImplicitBinder := parser! "{" >> many ident >> optional inferMod >> optDeclSig >> "}" -def structInstBinder := parser! "[" >> many ident >> optional inferMod >> optDeclSig >> "]" +def structExplicitBinder := parser! symbol "(" appPrec >> many ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")" +def structImplicitBinder := parser! symbol "{" appPrec >> many ident >> optional inferMod >> optDeclSig >> "}" +def structInstBinder := parser! symbol "[" appPrec >> many ident >> optional inferMod >> optDeclSig >> "]" def structFields := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder) -def structCtor := parser! ident >> optional inferMod >> " :: " +def structCtor := parser! ident >> optional inferMod >> symbol " :: " 67 def structureTk := parser! "structure " def classTk := parser! "class " def «extends» := parser! " extends " >> sepBy1 termParser ", " @@ -85,12 +85,12 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> « @[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident @[builtinCommandParser] def «init_quot» := parser! "init_quot" @[builtinCommandParser] def «set_option» := parser! "set_option " >> ident >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit) -@[builtinCommandParser] def «attribute» := parser! optional "local " >> "attribute " >> "[" >> sepBy1 attrInstance ", " >> "]" >> many1 ident -@[builtinCommandParser] def «export» := parser! "export " >> ident >> "(" >> many1 ident >> ")" +@[builtinCommandParser] def «attribute» := parser! optional "local " >> "attribute " >> symbol "[" appPrec >> sepBy1 attrInstance ", " >> "]" >> many1 ident +@[builtinCommandParser] def «export» := parser! "export " >> ident >> symbol "(" appPrec >> many1 ident >> ")" def openHiding := parser! try (ident >> "hiding") >> many1 ident def openRenamingItem := parser! ident >> unicodeSymbol "→" "->" >> ident def openRenaming := parser! try (ident >> "renaming") >> sepBy1 openRenamingItem ", " -def openOnly := parser! try (ident >> "(") >> many1 ident >> ")" +def openOnly := parser! try (ident >> symbol "(" appPrec) >> many1 ident >> ")" def openSimple := parser! many1 ident @[builtinCommandParser] def «open» := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple) diff --git a/stage0/src/Lean/Parser/Parser.lean b/stage0/src/Lean/Parser/Parser.lean index ab53fd5f71..1730f0eac3 100644 --- a/stage0/src/Lean/Parser/Parser.lean +++ b/stage0/src/Lean/Parser/Parser.lean @@ -1153,7 +1153,7 @@ def unquotedSymbol : Parser := { fn := unquotedSymbolFn } instance stringToParserCoe : HasCoe String Parser := -⟨symbolAux⟩ +⟨fun s => symbol s 0⟩ namespace ParserState @@ -1423,7 +1423,7 @@ def pushNone : Parser := { fn := fun c s => s.pushSyntax mkNullNode } -- We support two kinds of antiquotations: `$id` and `$(t)`, where `id` is a term identifier and `t` is a term. -def antiquotNestedExpr : Parser := node `antiquotNestedExpr ("(" >> termParser >> ")") +def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbol "(" appPrec >> termParser >> ")") def antiquotExpr : Parser := identNoAntiquot <|> antiquotNestedExpr /-- @@ -1444,7 +1444,7 @@ node kind $ try $ many (checkNoWsBefore "" >> dollarSymbol) >> checkNoWsBefore "no space before spliced term" >> antiquotExpr >> nameP >> - optional (checkNoWsBefore "" >> "*") + optional (checkNoWsBefore "" >> symbolAux "*" none) def tryAnti (c : ParserContext) (s : ParserState) : Bool := let (s, stx?) := peekToken c s; @@ -1725,7 +1725,7 @@ def compileParserDescr (categories : ParserCategories) : ParserDescr → Except | ParserDescr.sepBy1 d₁ d₂ => sepBy1 <$> compileParserDescr d₁ <*> compileParserDescr d₂ | ParserDescr.node k d => node k <$> compileParserDescr d | ParserDescr.trailingNode k d => trailingNode k <$> compileParserDescr d -| ParserDescr.symbol tk lbp => pure $ symbolAux tk lbp +| ParserDescr.symbol tk lbp => pure $ symbol tk lbp | ParserDescr.numLit => pure $ numLit | ParserDescr.strLit => pure $ strLit | ParserDescr.charLit => pure $ charLit diff --git a/stage0/src/Lean/Parser/Syntax.lean b/stage0/src/Lean/Parser/Syntax.lean index aa16e738b1..04a8d5082b 100644 --- a/stage0/src/Lean/Parser/Syntax.lean +++ b/stage0/src/Lean/Parser/Syntax.lean @@ -23,7 +23,7 @@ def «precedence» := parser! ":" >> precedenceLit def optPrecedence := optional (try «precedence») namespace Syntax -@[builtinSyntaxParser] def paren := parser! "(" >> many1 syntaxParser >> ")" +@[builtinSyntaxParser] def paren := parser! symbol "(" appPrec >> many1 syntaxParser >> ")" @[builtinSyntaxParser] def cat := parser! ident >> optPrecedence @[builtinSyntaxParser] def atom := parser! strLit >> optPrecedence @[builtinSyntaxParser] def num := parser! nonReservedSymbol "num" @@ -38,7 +38,7 @@ namespace Syntax @[builtinSyntaxParser] def optional := tparser! symbolAux "?" none @[builtinSyntaxParser] def many := tparser! symbolAux "*" none @[builtinSyntaxParser] def many1 := tparser! symbolAux "+" none -@[builtinSyntaxParser] def orelse := tparser! " <|> " >> syntaxParser 1 +@[builtinSyntaxParser] def orelse := tparser! symbol " <|> " 2 >> syntaxParser 1 end Syntax @@ -59,7 +59,7 @@ def mixfixSymbol := quotedSymbolPrec <|> unquotedSymbol def strLitPrec := parser! strLit >> optPrecedence def identPrec := parser! ident >> optPrecedence -def optKind : Parser := optional ("[" >> ident >> "]") +def optKind : Parser := optional (symbol "[" appPrec >> ident >> "]") -- TODO: remove " := " after old frontend is gone @[builtinCommandParser] def «notation» := parser! "notation" >> many (strLitPrec <|> quotedSymbolPrec <|> identPrec) >> (" := " <|> darrow) >> termParser @[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> optKind >> Term.matchAlts @@ -69,9 +69,9 @@ def macroArgType := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> macroArgType def macroArg := try strLitPrec <|> try macroArgSimple def macroHead := macroArg <|> try identPrec -def macroTailTactic : Parser := try (" : " >> identEq "tactic") >> darrow >> "`(" >> sepBy1 tacticParser "; " true true >> ")" -def macroTailCommand : Parser := try (" : " >> identEq "command") >> darrow >> "`(" >> many1 commandParser true >> ")" -def macroTailDefault : Parser := try (" : " >> ident) >> darrow >> (("`(" >> categoryParserOfStack 2 >> ")") <|> termParser) +def macroTailTactic : Parser := try (" : " >> identEq "tactic") >> darrow >> symbol "`(" appPrec >> sepBy1 tacticParser "; " true true >> ")" +def macroTailCommand : Parser := try (" : " >> identEq "command") >> darrow >> symbol "`(" appPrec >> many1 commandParser true >> ")" +def macroTailDefault : Parser := try (" : " >> ident) >> darrow >> ((symbol "`(" appPrec >> categoryParserOfStack 2 >> ")") <|> termParser) def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault @[builtinCommandParser] def «macro» := parser! "macro " >> macroHead >> many macroArg >> macroTail diff --git a/stage0/src/Lean/Parser/Tactic.lean b/stage0/src/Lean/Parser/Tactic.lean index d027c72800..d129c79044 100644 --- a/stage0/src/Lean/Parser/Tactic.lean +++ b/stage0/src/Lean/Parser/Tactic.lean @@ -37,7 +37,7 @@ def ident' : Parser := ident <|> underscore @[builtinTacticParser] def «skip» := parser! nonReservedSymbol "skip" @[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState" @[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> tacticParser -@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize" >> optional (try (ident >> " : ")) >> termParser 50 >> " = " >> ident +@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize" >> optional (try (ident >> " : ")) >> termParser 50 >> symbol " = " 50 >> ident def majorPremise := parser! optional (try (ident >> " : ")) >> termParser def inductionAlt : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> (Term.hole <|> Term.namedHole <|> tacticParser) def inductionAlts : Parser := withPosition $ fun pos => "|" >> sepBy1 inductionAlt (checkColGe pos.column "alternatives must be indented" >> "|") @@ -48,10 +48,10 @@ def generalizingVars := optional (" generalizing " >> many1 ident) @[builtinTacticParser] def «cases» := parser! nonReservedSymbol "cases " >> majorPremise >> withAlts def withIds : Parser := optional (" with " >> many1 ident') @[builtinTacticParser] def «injection» := parser! nonReservedSymbol "injection " >> termParser >> withIds -@[builtinTacticParser] def paren := parser! "(" >> nonEmptySeq >> ")" -@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end" -@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}" -@[builtinTacticParser] def orelse := tparser! " <|> " >> tacticParser 1 +@[builtinTacticParser] def paren := parser! symbol "(" appPrec >> nonEmptySeq >> ")" +@[builtinTacticParser] def nestedTacticBlock := parser! symbol "begin " appPrec >> seq >> "end" +@[builtinTacticParser] def nestedTacticBlockCurly := parser! symbol "{" appPrec >> seq >> "}" +@[builtinTacticParser] def orelse := tparser! symbol " <|> " 2 >> tacticParser 1 end Tactic end Parser diff --git a/stage0/src/Lean/Parser/Term.lean b/stage0/src/Lean/Parser/Term.lean index a7175a1853..bdc492d43e 100644 --- a/stage0/src/Lean/Parser/Term.lean +++ b/stage0/src/Lean/Parser/Term.lean @@ -47,7 +47,7 @@ def leadPrec := appPrec - 1 -- NOTE: `checkNoWsBefore` should be used *before* `parser!` so that it is also applied to the generated -- antiquotation. def explicitUniv := checkNoWsBefore "no space before '.{'" >> parser! ".{" >> sepBy1 levelParser ", " >> "}" -def namedPattern := checkNoWsBefore "no space before '@'" >> parser! "@" >> termParser appPrec +def namedPattern := checkNoWsBefore "no space before '@'" >> parser! symbol "@" appPrec >> termParser appPrec @[builtinTermParser] def id := parser! ident >> optional (explicitUniv <|> namedPattern) @[builtinTermParser] def num : Parser := parser! numLit @[builtinTermParser] def str : Parser := parser! strLit @@ -72,7 +72,7 @@ def haveAssign := parser! " := " >> termParser @[builtinTermParser] def «have» := parser! symbol "have " leadPrec >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> termParser @[builtinTermParser] def «suffices» := parser! symbol "suffices " leadPrec >> optIdent >> termParser >> fromTerm >> "; " >> termParser @[builtinTermParser] def «show» := parser! symbol "show " leadPrec >> termParser >> fromTerm -def structInstArrayRef := parser! "[" >> termParser >>"]" +def structInstArrayRef := parser! symbol "[" appPrec >> termParser >>"]" def structInstLVal := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef) def structInstField := parser! structInstLVal >> " := " >> termParser @[builtinTermParser] def structInst := parser! symbol "{" appPrec >> optional (try (termParser >> "with")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> "}" @@ -85,11 +85,11 @@ def optType : Parser := optional typeSpec @[builtinTermParser] def inaccessible := parser! symbol ".(" appPrec >> termParser >> ")" def binderIdent : Parser := ident <|> hole def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser) -def binderTactic := parser! try (" := " >> " by ") >> Tactic.nonEmptySeq +def binderTactic := parser! try (" := " >> symbol " by " leadPrec) >> Tactic.nonEmptySeq def binderDefault := parser! " := " >> termParser -def explicitBinder (requireType := false) := parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")" -def implicitBinder (requireType := false) := parser! "{" >> many1 binderIdent >> binderType requireType >> "}" -def instBinder := parser! "[" >> optIdent >> termParser >> "]" +def explicitBinder (requireType := false) := parser! symbol "(" appPrec >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")" +def implicitBinder (requireType := false) := parser! symbol "{" appPrec >> many1 binderIdent >> binderType requireType >> "}" +def instBinder := parser! symbol "[" appPrec >> optIdent >> termParser >> "]" def bracketedBinder (requireType := false) := explicitBinder requireType <|> implicitBinder requireType <|> instBinder @[builtinTermParser] def depArrow := parser! bracketedBinder true >> checkRBPGreater 25 "expected parentheses around dependent arrow" >> unicodeSymbol " → " " -> " >> termParser def simpleBinder := parser! many1 binderIdent @@ -126,13 +126,13 @@ def letDecl := letIdDecl <|> letPatDecl <|> letEqnsDecl @[builtinTermParser] def «let!» := parser! symbol "let! " leadPrec >> letDecl >> "; " >> termParser def leftArrow : Parser := unicodeSymbol " ← " " <- " -def doLet := parser! "let " >> letDecl +def doLet := parser! symbol "let " leadPrec >> letDecl def doId := parser! try (ident >> optType >> leftArrow) >> termParser def doPat := parser! try (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser) def doExpr := parser! termParser def doElem := doLet <|> doId <|> doPat <|> doExpr def doSeq := sepBy1 doElem "; " -def bracketedDoSeq := parser! "{" >> doSeq >> "}" +def bracketedDoSeq := parser! symbol "{" appPrec >> doSeq >> "}" @[builtinTermParser] def liftMethod := parser! leftArrow >> termParser @[builtinTermParser] def «do» := parser! symbol "do " leadPrec >> (bracketedDoSeq <|> doSeq) @@ -145,7 +145,7 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}" -- symbol precedence should be higher, but must match the one of `sub` below @[builtinTermParser] def uminus := parser! symbol "-" 65 >> termParser 100 -def namedArgument := parser! try ("(" >> ident >> " := ") >> termParser >> ")" +def namedArgument := parser! try (symbol "(" appPrec >> ident >> " := ") >> termParser >> ")" @[builtinTermParser] def app := tparser! many1 (namedArgument <|> termParser appPrec) def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type || stx.isOfKind `Lean.Parser.Term.sort) @@ -157,7 +157,7 @@ def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type @[builtinTermParser] def dollar := tparser! try (dollarSymbol >> checkWsBefore "space expected") >> termParser 0 @[builtinTermParser] def dollarProj := tparser! symbol "$." 1 >> (fieldIdx <|> ident) -@[builtinTermParser] def «where» := tparser! symbol " where " 1 >> sepBy1 letDecl (group ("; " >> " where ")) +@[builtinTermParser] def «where» := tparser! symbol " where " 1 >> sepBy1 letDecl (group ("; " >> symbol " where " 1)) @[builtinTermParser] def fcomp := tparser! infixR " ∘ " 90 @@ -182,7 +182,7 @@ def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type @[builtinTermParser] def heq := tparser! unicodeInfixL " ≅ " " ~= " 50 @[builtinTermParser] def equiv := tparser! infixL " ≈ " 50 -@[builtinTermParser] def subst := tparser! symbol " ▸ " 75 >> sepBy1 (termParser 75) " ▸ " +@[builtinTermParser] def subst := tparser! symbol " ▸ " 75 >> sepBy1 (termParser 75) (symbol " ▸ " 75) @[builtinTermParser] def and := tparser! unicodeInfixR " ∧ " " /\\ " 35 @[builtinTermParser] def or := tparser! unicodeInfixR " ∨ " " \\/ " 30 diff --git a/stage0/stdlib/Init/LeanInit.c b/stage0/stdlib/Init/LeanInit.c index 0391405d5d..88dbb472c9 100644 --- a/stage0/stdlib/Init/LeanInit.c +++ b/stage0/stdlib/Init/LeanInit.c @@ -1484,11 +1484,11 @@ lean_object* _init_l_Lean_ParserDescr_inhabited___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_String_splitAux___main___closed__1; +x_1 = l_String_splitAux___main___closed__1; +x_2 = lean_unsigned_to_nat(0u); x_3 = lean_alloc_ctor(11, 2, 0); -lean_ctor_set(x_3, 0, x_2); -lean_ctor_set(x_3, 1, x_1); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); return x_3; } } diff --git a/stage0/stdlib/Lean/Elab/Syntax.c b/stage0/stdlib/Lean/Elab/Syntax.c index 40ba96babd..5030a34af8 100644 --- a/stage0/stdlib/Lean/Elab/Syntax.c +++ b/stage0/stdlib/Lean/Elab/Syntax.c @@ -207,6 +207,7 @@ extern lean_object* l_Lean_Parser_Command_strLitPrec___elambda__1___closed__2; extern lean_object* l_Lean_Parser_Syntax_num___elambda__1___closed__1; lean_object* l___private_Lean_Elab_Syntax_8__regTraceClasses___closed__1; lean_object* l_Lean_Elab_Term_throwUnsupportedSyntax___rarg(lean_object*); +extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__1; extern lean_object* l_Lean_Expr_isSyntheticSorry___closed__1; lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__87; lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__68; @@ -559,7 +560,6 @@ lean_object* l_Array_umapMAux___main___at_Lean_Elab_Command_expandMacro___spec__ lean_object* l_Lean_Elab_Command_elabSyntax___closed__31; lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__31; lean_object* l___regBuiltin_Lean_Elab_Command_elabSyntax___closed__1; -extern lean_object* l_Lean_Parser_Level_paren___closed__1; uint8_t lean_string_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__8; uint8_t lean_nat_dec_lt(lean_object*, lean_object*); @@ -587,7 +587,7 @@ lean_dec(x_6); if (lean_obj_tag(x_8) == 0) { lean_object* x_9; -x_9 = l_Lean_Parser_Level_paren___closed__1; +x_9 = l_Lean_Parser_antiquotNestedExpr___closed__1; return x_9; } else diff --git a/stage0/stdlib/Lean/Parser/Command.c b/stage0/stdlib/Lean/Parser/Command.c index 1a08ce1452..31bc29d242 100644 --- a/stage0/stdlib/Lean/Parser/Command.c +++ b/stage0/stdlib/Lean/Parser/Command.c @@ -24,6 +24,7 @@ lean_object* l_Lean_Parser_Command_def___closed__5; lean_object* l_Lean_Parser_Command_structure___closed__7; lean_object* l_Lean_Parser_Command_section___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_open___closed__3; +lean_object* l_Lean_Parser_Command_structCtor___closed__8; lean_object* l_Lean_Parser_Command_check___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_structCtor___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_structImplicitBinder___closed__8; @@ -62,6 +63,7 @@ lean_object* l_Lean_Parser_Term_stxQuot___closed__8; extern lean_object* l_Lean_Parser_Term_matchAlt___closed__3; lean_object* l_Lean_Parser_Command_structImplicitBinder___closed__2; lean_object* l_Lean_Parser_Command_extends___elambda__1___closed__7; +extern lean_object* l_Lean_Parser_Term_structInst___closed__1; lean_object* l_Lean_Parser_Command_end___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_openRenamingItem___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_extends___closed__1; @@ -476,6 +478,7 @@ lean_object* l_Lean_Parser_Command_attrArg; extern lean_object* l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__4; lean_object* l_Lean_Parser_Command_variables___closed__4; extern lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__1; +extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__4; lean_object* l_Lean_Parser_Command_protected___elambda__1___closed__5; lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__15; lean_object* l_Lean_Parser_Command_openSimple___closed__3; @@ -929,7 +932,6 @@ lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_axiom___closed__1; lean_object* l_Lean_Parser_Command_exit___closed__3; lean_object* l_Lean_Parser_Command_unsafe___elambda__1(lean_object*, lean_object*); -extern lean_object* l_Lean_Parser_Term_implicitBinder___closed__1; lean_object* l_Lean_Parser_Command_private___elambda__1___closed__7; lean_object* l_Lean_Parser_Command_noncomputable___elambda__1___closed__6; lean_object* l_Lean_Parser_Command_structure___closed__13; @@ -1037,6 +1039,7 @@ lean_object* l_Lean_Parser_Command_axiom___elambda__1___closed__5; lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_axiom; lean_object* l_Lean_Parser_Command_exit___closed__2; +extern lean_object* l_Lean_Syntax_decodeNatLitVal___closed__1; lean_object* l_Lean_Parser_Command_openOnly___closed__4; lean_object* l_Lean_Parser_Command_noncomputable___closed__2; lean_object* l_Lean_Parser_Command_theorem___elambda__1___closed__3; @@ -1131,7 +1134,6 @@ lean_object* l_Lean_Parser_Command_declValEqns; lean_object* l_Lean_Parser_Command_declModifiers___closed__9; lean_object* l_Lean_Parser_Command_declaration___closed__14; lean_object* l_Lean_Parser_Command_example___closed__1; -extern lean_object* l_Lean_Parser_Level_paren___closed__1; lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__3; lean_object* l___regBuiltinParser_Lean_Parser_Command_synth(lean_object*); lean_object* l_Lean_Parser_Command_attributes___elambda__1___closed__1; @@ -2011,7 +2013,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__4; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -2033,7 +2035,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj x_1 = l_Lean_Parser_Term_stxQuot___closed__2; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_3 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_4 = lean_ctor_get(x_3, 0); lean_inc(x_4); x_5 = l_Lean_Parser_orelseInfo(x_4, x_2); @@ -2045,7 +2047,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_stxQuot___closed__3; -x_2 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__4; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } @@ -2530,9 +2532,9 @@ lean_object* _init_l_Lean_Parser_Command_docComment___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_docComment___elambda__1___closed__8; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_docComment___elambda__1___closed__8; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -3761,9 +3763,9 @@ lean_object* _init_l_Lean_Parser_Command_attributes___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_attributes___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_attributes___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -4167,9 +4169,9 @@ lean_object* _init_l_Lean_Parser_Command_private___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_private___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_private___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -4515,9 +4517,9 @@ lean_object* _init_l_Lean_Parser_Command_protected___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_protected___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_protected___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -4958,9 +4960,9 @@ lean_object* _init_l_Lean_Parser_Command_noncomputable___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_noncomputable___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_noncomputable___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -5306,9 +5308,9 @@ lean_object* _init_l_Lean_Parser_Command_unsafe___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_unsafe___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_unsafe___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -5654,9 +5656,9 @@ lean_object* _init_l_Lean_Parser_Command_partial___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_partial___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -9086,9 +9088,9 @@ lean_object* _init_l_Lean_Parser_Command_abbrev___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_abbrev___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_abbrev___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -9576,9 +9578,9 @@ lean_object* _init_l_Lean_Parser_Command_def___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_def___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_def___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -10040,9 +10042,9 @@ lean_object* _init_l_Lean_Parser_Command_theorem___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_theorem___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_theorem___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -10622,9 +10624,9 @@ lean_object* _init_l_Lean_Parser_Command_constant___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_constant___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_constant___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -11353,9 +11355,9 @@ lean_object* _init_l_Lean_Parser_Command_instance___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_instance___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_instance___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -11802,9 +11804,9 @@ lean_object* _init_l_Lean_Parser_Command_axiom___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_axiom___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_axiom___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -12244,9 +12246,9 @@ lean_object* _init_l_Lean_Parser_Command_example___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_example___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_example___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -12853,7 +12855,7 @@ lean_object* _init_l_Lean_Parser_Command_inferMod___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_implicitBinder___closed__1; +x_1 = l_Lean_Parser_Term_structInst___closed__1; x_2 = l_Lean_Parser_Term_explicitUniv___closed__4; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; @@ -13981,9 +13983,9 @@ lean_object* _init_l_Lean_Parser_Command_inductive___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_inductive___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_inductive___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -14794,9 +14796,9 @@ lean_object* _init_l_Lean_Parser_Command_classInductive___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_classInductive___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_classInductive___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -15692,7 +15694,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Command_structExplicitBinder___closed__2; -x_2 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__4; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } @@ -15733,7 +15735,7 @@ lean_object* _init_l_Lean_Parser_Command_structExplicitBinder___closed__7() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__1; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; x_2 = l_Lean_Parser_Command_structExplicitBinder___closed__6; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; @@ -16426,7 +16428,7 @@ lean_object* _init_l_Lean_Parser_Command_structImplicitBinder___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_implicitBinder___closed__1; +x_1 = l_Lean_Parser_Term_structInst___closed__1; x_2 = l_Lean_Parser_Command_structImplicitBinder___closed__3; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; @@ -17983,58 +17985,68 @@ return x_94; lean_object* _init_l_Lean_Parser_Command_structCtor___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_structCtor___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); -return x_3; +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(67u); +x_2 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; } } lean_object* _init_l_Lean_Parser_Command_structCtor___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_introRule___closed__1; +x_1 = l_Lean_Parser_Command_structCtor___elambda__1___closed__5; x_2 = l_Lean_Parser_Command_structCtor___closed__1; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } lean_object* _init_l_Lean_Parser_Command_structCtor___closed__3() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_ident; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_Command_structCtor___closed__2; -x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); -return x_4; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Command_introRule___closed__1; +x_2 = l_Lean_Parser_Command_structCtor___closed__2; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; } } lean_object* _init_l_Lean_Parser_Command_structCtor___closed__4() { _start: { +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_ident; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Command_structCtor___closed__3; +x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Command_structCtor___closed__5() { +_start: +{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Command_structCtor___elambda__1___closed__2; -x_2 = l_Lean_Parser_Command_structCtor___closed__3; +x_2 = l_Lean_Parser_Command_structCtor___closed__4; x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Command_structCtor___closed__5() { +lean_object* _init_l_Lean_Parser_Command_structCtor___closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Command_structCtor___elambda__1___closed__4; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Command_structCtor___closed__4; +x_3 = l_Lean_Parser_Command_structCtor___closed__5; x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_Command_structCtor___closed__6() { +lean_object* _init_l_Lean_Parser_Command_structCtor___closed__7() { _start: { lean_object* x_1; @@ -18042,12 +18054,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_structCtor___elambda__1), return x_1; } } -lean_object* _init_l_Lean_Parser_Command_structCtor___closed__7() { +lean_object* _init_l_Lean_Parser_Command_structCtor___closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_structCtor___closed__5; -x_2 = l_Lean_Parser_Command_structCtor___closed__6; +x_1 = l_Lean_Parser_Command_structCtor___closed__6; +x_2 = l_Lean_Parser_Command_structCtor___closed__7; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -18058,7 +18070,7 @@ lean_object* _init_l_Lean_Parser_Command_structCtor() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Command_structCtor___closed__7; +x_1 = l_Lean_Parser_Command_structCtor___closed__8; return x_1; } } @@ -18354,9 +18366,9 @@ lean_object* _init_l_Lean_Parser_Command_structureTk___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_structureTk___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_structureTk___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -19027,9 +19039,9 @@ lean_object* _init_l_Lean_Parser_Command_extends___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_extends___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_extends___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -21907,9 +21919,9 @@ lean_object* _init_l_Lean_Parser_Command_section___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_section___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_section___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -22322,9 +22334,9 @@ lean_object* _init_l_Lean_Parser_Command_namespace___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_namespace___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_namespace___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -22812,9 +22824,9 @@ lean_object* _init_l_Lean_Parser_Command_end___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_end___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_end___elambda__1___closed__5; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -23223,9 +23235,9 @@ lean_object* _init_l_Lean_Parser_Command_variable___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_variable___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_variable___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -23692,9 +23704,9 @@ lean_object* _init_l_Lean_Parser_Command_variables___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_variables___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_variables___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -24098,9 +24110,9 @@ lean_object* _init_l_Lean_Parser_Command_universe___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_universe___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_universe___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -24556,9 +24568,9 @@ lean_object* _init_l_Lean_Parser_Command_universes___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_universes___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_universes___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -24966,9 +24978,9 @@ lean_object* _init_l_Lean_Parser_Command_check___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_check___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_check___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -24976,7 +24988,7 @@ lean_object* _init_l_Lean_Parser_Command_check___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Command_check___closed__1; @@ -25376,9 +25388,9 @@ lean_object* _init_l_Lean_Parser_Command_check__failure___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_check__failure___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_check__failure___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -25386,7 +25398,7 @@ lean_object* _init_l_Lean_Parser_Command_check__failure___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Command_check__failure___closed__1; @@ -25786,9 +25798,9 @@ lean_object* _init_l_Lean_Parser_Command_synth___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_synth___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_synth___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -25796,7 +25808,7 @@ lean_object* _init_l_Lean_Parser_Command_synth___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Command_synth___closed__1; @@ -26158,9 +26170,9 @@ lean_object* _init_l_Lean_Parser_Command_exit___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_exit___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_exit___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -26552,9 +26564,9 @@ lean_object* _init_l_Lean_Parser_Command_resolve__name___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_resolve__name___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_resolve__name___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -26916,9 +26928,9 @@ lean_object* _init_l_Lean_Parser_Command_init__quot___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_init__quot___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_init__quot___elambda__1___closed__5; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -27730,9 +27742,9 @@ lean_object* _init_l_Lean_Parser_Command_set__option___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_set__option___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_set__option___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -28872,9 +28884,9 @@ lean_object* _init_l_Lean_Parser_Command_attribute___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_attribute___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -28891,9 +28903,9 @@ lean_object* _init_l_Lean_Parser_Command_attribute___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_attribute___elambda__1___closed__8; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__8; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -29737,9 +29749,9 @@ lean_object* _init_l_Lean_Parser_Command_export___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_export___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_export___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -29750,7 +29762,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_ident; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_3 = l_Lean_Parser_antiquotNestedExpr___closed__4; x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); return x_4; } @@ -29759,7 +29771,7 @@ lean_object* _init_l_Lean_Parser_Command_export___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__1; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; x_2 = l_Lean_Parser_Command_export___closed__2; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; @@ -30413,9 +30425,9 @@ lean_object* _init_l_Lean_Parser_Command_openHiding___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_openHiding___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_openHiding___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -31601,9 +31613,9 @@ lean_object* _init_l_Lean_Parser_Command_openRenaming___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_openRenaming___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_openRenaming___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -32395,7 +32407,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_ident; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_antiquotNestedExpr___closed__1; +x_3 = l_Lean_Parser_antiquotNestedExpr___closed__2; x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); return x_4; } @@ -33325,9 +33337,9 @@ lean_object* _init_l_Lean_Parser_Command_open___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_open___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_open___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -34423,6 +34435,8 @@ l_Lean_Parser_Command_structCtor___closed__6 = _init_l_Lean_Parser_Command_struc lean_mark_persistent(l_Lean_Parser_Command_structCtor___closed__6); l_Lean_Parser_Command_structCtor___closed__7 = _init_l_Lean_Parser_Command_structCtor___closed__7(); lean_mark_persistent(l_Lean_Parser_Command_structCtor___closed__7); +l_Lean_Parser_Command_structCtor___closed__8 = _init_l_Lean_Parser_Command_structCtor___closed__8(); +lean_mark_persistent(l_Lean_Parser_Command_structCtor___closed__8); l_Lean_Parser_Command_structCtor = _init_l_Lean_Parser_Command_structCtor(); lean_mark_persistent(l_Lean_Parser_Command_structCtor); l_Lean_Parser_Command_structureTk___elambda__1___closed__1 = _init_l_Lean_Parser_Command_structureTk___elambda__1___closed__1(); diff --git a/stage0/stdlib/Lean/Parser/Level.c b/stage0/stdlib/Lean/Parser/Level.c index a6501f8f94..41c9f088f4 100644 --- a/stage0/stdlib/Lean/Parser/Level.c +++ b/stage0/stdlib/Lean/Parser/Level.c @@ -77,12 +77,15 @@ extern lean_object* l_Lean_Nat_HasQuote___closed__1; lean_object* l_Lean_Parser_nodeInfo(lean_object*, lean_object*); lean_object* l_Lean_Parser_Level_addLit___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__2; +extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__1; +extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__2; lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*, uint8_t); lean_object* l_Lean_Parser_Level_paren; lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__2; lean_object* l_Lean_Parser_Level_num___elambda__1(lean_object*, lean_object*); uint8_t l_Lean_Parser_tryAnti(lean_object*, lean_object*); lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__4; +extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__4; lean_object* l_Lean_Parser_Level_max___closed__6; lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__1; lean_object* l_Lean_Parser_Level_imax; @@ -102,12 +105,10 @@ lean_object* l_Lean_Parser_Level_addLit___closed__5; lean_object* l_Lean_Parser_Level_addLit___closed__3; lean_object* l_Lean_Parser_Level_imax___closed__2; lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*); -extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__3; lean_object* l_Lean_Parser_Level_ident___elambda__1___closed__1; lean_object* l_Lean_Parser_Level_paren___closed__4; lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__3; extern lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__7; -lean_object* l_Lean_Parser_Level_paren___closed__9; lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__6; lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__2; lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__1; @@ -158,7 +159,6 @@ lean_object* l_Lean_Parser_Level_paren___closed__6; lean_object* l___regBuiltinParser_Lean_Parser_Level_imax(lean_object*); lean_object* l_Lean_Parser_Level_imax___closed__4; lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__7; -lean_object* l_Lean_Parser_Level_paren___closed__8; lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__4; lean_object* l_Lean_Parser_Level_hole___closed__4; lean_object* l_Lean_Parser_Level_addLit___closed__1; @@ -676,26 +676,6 @@ return x_103; lean_object* _init_l_Lean_Parser_Level_paren___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_appPrec; -x_2 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_2, 0, x_1); -return x_2; -} -} -lean_object* _init_l_Lean_Parser_Level_paren___closed__2() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__3; -x_2 = l_Lean_Parser_Level_paren___closed__1; -x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Level_paren___closed__3() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_regBuiltinLevelParserAttr___closed__4; x_2 = lean_unsigned_to_nat(0u); @@ -703,51 +683,51 @@ x_3 = l_Lean_Parser_categoryParser(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Level_paren___closed__4() { +lean_object* _init_l_Lean_Parser_Level_paren___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Level_paren___closed__3; +x_1 = l_Lean_Parser_Level_paren___closed__1; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_3 = l_Lean_Parser_antiquotNestedExpr___closed__4; x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_Level_paren___closed__5() { +lean_object* _init_l_Lean_Parser_Level_paren___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Level_paren___closed__2; -x_2 = l_Lean_Parser_Level_paren___closed__4; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_2 = l_Lean_Parser_Level_paren___closed__2; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Level_paren___closed__6() { +lean_object* _init_l_Lean_Parser_Level_paren___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Level_paren___elambda__1___closed__4; -x_2 = l_Lean_Parser_Level_paren___closed__5; +x_2 = l_Lean_Parser_Level_paren___closed__3; x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Level_paren___closed__7() { +lean_object* _init_l_Lean_Parser_Level_paren___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Level_paren___elambda__1___closed__6; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Level_paren___closed__6; +x_3 = l_Lean_Parser_Level_paren___closed__4; x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_Level_paren___closed__8() { +lean_object* _init_l_Lean_Parser_Level_paren___closed__6() { _start: { lean_object* x_1; @@ -755,12 +735,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Level_paren___elambda__1), 2, 0); return x_1; } } -lean_object* _init_l_Lean_Parser_Level_paren___closed__9() { +lean_object* _init_l_Lean_Parser_Level_paren___closed__7() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Level_paren___closed__7; -x_2 = l_Lean_Parser_Level_paren___closed__8; +x_1 = l_Lean_Parser_Level_paren___closed__5; +x_2 = l_Lean_Parser_Level_paren___closed__6; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -771,7 +751,7 @@ lean_object* _init_l_Lean_Parser_Level_paren() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Level_paren___closed__9; +x_1 = l_Lean_Parser_Level_paren___closed__7; return x_1; } } @@ -1798,7 +1778,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Level_hole___elambda__1___closed__4; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -2497,10 +2477,6 @@ l_Lean_Parser_Level_paren___closed__6 = _init_l_Lean_Parser_Level_paren___closed lean_mark_persistent(l_Lean_Parser_Level_paren___closed__6); l_Lean_Parser_Level_paren___closed__7 = _init_l_Lean_Parser_Level_paren___closed__7(); lean_mark_persistent(l_Lean_Parser_Level_paren___closed__7); -l_Lean_Parser_Level_paren___closed__8 = _init_l_Lean_Parser_Level_paren___closed__8(); -lean_mark_persistent(l_Lean_Parser_Level_paren___closed__8); -l_Lean_Parser_Level_paren___closed__9 = _init_l_Lean_Parser_Level_paren___closed__9(); -lean_mark_persistent(l_Lean_Parser_Level_paren___closed__9); l_Lean_Parser_Level_paren = _init_l_Lean_Parser_Level_paren(); lean_mark_persistent(l_Lean_Parser_Level_paren); res = l___regBuiltinParser_Lean_Parser_Level_paren(lean_io_mk_world()); diff --git a/stage0/stdlib/Lean/Parser/Module.c b/stage0/stdlib/Lean/Parser/Module.c index 04d9aae329..0a173c98d1 100644 --- a/stage0/stdlib/Lean/Parser/Module.c +++ b/stage0/stdlib/Lean/Parser/Module.c @@ -168,6 +168,7 @@ uint8_t l_PersistentArray_anyM___at_Lean_MessageLog_hasErrors___spec__1(lean_obj lean_object* l_Lean_Parser_Module_prelude___elambda__1___closed__3; lean_object* l_Lean_Syntax_formatStxAux___main(lean_object*, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Module_import___elambda__1___closed__9; +extern lean_object* l_Lean_Syntax_decodeNatLitVal___closed__1; lean_object* l_PersistentArray_forM___at___private_Lean_Parser_Module_4__testModuleParserAux___main___spec__6(lean_object*, lean_object*, lean_object*); lean_object* l_IO_FS_Handle_readToEndAux___main___at_Lean_Parser_parseFile___spec__2(lean_object*, lean_object*, lean_object*); lean_object* l_IO_FS_Handle_mk___at_IO_FS_withFile___spec__1(lean_object*, uint8_t, uint8_t, lean_object*); @@ -493,9 +494,9 @@ lean_object* _init_l_Lean_Parser_Module_prelude___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Module_prelude___elambda__1___closed__7; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Module_prelude___elambda__1___closed__7; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -1236,9 +1237,9 @@ lean_object* _init_l_Lean_Parser_Module_import___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Module_import___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Module_import___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -1246,9 +1247,9 @@ lean_object* _init_l_Lean_Parser_Module_import___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Module_import___elambda__1___closed__8; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Module_import___elambda__1___closed__8; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } diff --git a/stage0/stdlib/Lean/Parser/Parser.c b/stage0/stdlib/Lean/Parser/Parser.c index cdfbfba0f0..f19cea5158 100644 --- a/stage0/stdlib/Lean/Parser/Parser.c +++ b/stage0/stdlib/Lean/Parser/Parser.c @@ -405,6 +405,7 @@ lean_object* l_Lean_Parser_hasAndthen; lean_object* l_Lean_Parser_satisfyFn___at_Lean_Parser_rawCh___elambda__1___spec__1(uint32_t, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_ident___closed__2; uint8_t lean_nat_dec_eq(lean_object*, lean_object*); +lean_object* l_Lean_Parser_antiquotNestedExpr___closed__9; lean_object* l_Lean_Parser_Error_HasBeq___closed__1; lean_object* l_Lean_Parser_nonReservedSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Syntax_foldSepArgsM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -1030,6 +1031,7 @@ lean_object* l_Lean_Parser_unicodeSymbolInfo(lean_object*, lean_object*, lean_ob lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_identNoAntiquot; lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*); +extern lean_object* l_Lean_Syntax_decodeNatLitVal___closed__1; lean_object* l_Lean_Parser_mkCategoryParserFnRef(lean_object*); lean_object* l_Lean_Parser_ParserState_keepPrevError___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_strAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -12074,12 +12076,12 @@ lean_object* l_Lean_Parser_stringToParserCoe(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; -x_2 = lean_box(0); -x_3 = l_String_trim(x_1); -lean_inc(x_3); -x_4 = l_Lean_Parser_symbolInfo(x_3, x_2); +x_2 = l_String_trim(x_1); +x_3 = l_Lean_Syntax_decodeNatLitVal___closed__1; +lean_inc(x_2); +x_4 = l_Lean_Parser_symbolInfo(x_2, x_3); x_5 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1); -lean_closure_set(x_5, 0, x_3); +lean_closure_set(x_5, 0, x_2); x_6 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_6, 0, x_4); lean_ctor_set(x_6, 1, x_5); @@ -25843,79 +25845,89 @@ return x_36; lean_object* _init_l_Lean_Parser_antiquotNestedExpr___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__3; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); -return x_3; +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_appPrec; +x_2 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; } } lean_object* _init_l_Lean_Parser_antiquotNestedExpr___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__3; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_antiquotNestedExpr___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_termParser___closed__2; x_2 = lean_unsigned_to_nat(0u); x_3 = l_Lean_Parser_categoryParser(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_antiquotNestedExpr___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__4; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); -return x_3; -} -} lean_object* _init_l_Lean_Parser_antiquotNestedExpr___closed__4() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_antiquotNestedExpr___closed__3; -x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); -return x_4; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__4; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); +return x_3; } } lean_object* _init_l_Lean_Parser_antiquotNestedExpr___closed__5() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__1; -x_2 = l_Lean_Parser_antiquotNestedExpr___closed__4; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); -return x_3; +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_antiquotNestedExpr___closed__4; +x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); +return x_4; } } lean_object* _init_l_Lean_Parser_antiquotNestedExpr___closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; x_2 = l_Lean_Parser_antiquotNestedExpr___closed__5; -x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } } lean_object* _init_l_Lean_Parser_antiquotNestedExpr___closed__7() { _start: { +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__2; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__6; +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_antiquotNestedExpr___closed__8() { +_start: +{ lean_object* x_1; x_1 = lean_alloc_closure((void*)(l_Lean_Parser_antiquotNestedExpr___elambda__1), 2, 0); return x_1; } } -lean_object* _init_l_Lean_Parser_antiquotNestedExpr___closed__8() { +lean_object* _init_l_Lean_Parser_antiquotNestedExpr___closed__9() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__6; -x_2 = l_Lean_Parser_antiquotNestedExpr___closed__7; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__7; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__8; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -25926,7 +25938,7 @@ lean_object* _init_l_Lean_Parser_antiquotNestedExpr() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__8; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__9; return x_1; } } @@ -32223,106 +32235,108 @@ return x_275; } case 11: { -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_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_dec(x_1); x_276 = lean_ctor_get(x_2, 0); lean_inc(x_276); x_277 = lean_ctor_get(x_2, 1); lean_inc(x_277); lean_dec(x_2); -x_278 = l_String_trim(x_276); +x_278 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_278, 0, x_277); +x_279 = l_String_trim(x_276); lean_dec(x_276); -lean_inc(x_278); -x_279 = l_Lean_Parser_symbolInfo(x_278, x_277); -x_280 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1); -lean_closure_set(x_280, 0, x_278); -x_281 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_281, 0, x_279); -lean_ctor_set(x_281, 1, x_280); -x_282 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_282, 0, x_281); -return x_282; +lean_inc(x_279); +x_280 = l_Lean_Parser_symbolInfo(x_279, x_278); +x_281 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1); +lean_closure_set(x_281, 0, x_279); +x_282 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_282, 0, x_280); +lean_ctor_set(x_282, 1, x_281); +x_283 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_283, 0, x_282); +return x_283; } case 12: { -lean_object* x_283; uint8_t 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_284; uint8_t x_285; lean_object* x_286; lean_object* x_287; lean_object* x_288; lean_object* x_289; lean_object* x_290; lean_dec(x_1); -x_283 = lean_ctor_get(x_2, 0); -lean_inc(x_283); -x_284 = lean_ctor_get_uint8(x_2, sizeof(void*)*1); +x_284 = lean_ctor_get(x_2, 0); +lean_inc(x_284); +x_285 = lean_ctor_get_uint8(x_2, sizeof(void*)*1); lean_dec(x_2); -x_285 = l_String_trim(x_283); -lean_dec(x_283); -lean_inc(x_285); -x_286 = l_Lean_Parser_nonReservedSymbolInfo(x_285, x_284); -x_287 = lean_alloc_closure((void*)(l_Lean_Parser_nonReservedSymbolFn), 3, 1); -lean_closure_set(x_287, 0, x_285); -x_288 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_288, 0, x_286); -lean_ctor_set(x_288, 1, x_287); -x_289 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_289, 0, x_288); -return x_289; +x_286 = l_String_trim(x_284); +lean_dec(x_284); +lean_inc(x_286); +x_287 = l_Lean_Parser_nonReservedSymbolInfo(x_286, x_285); +x_288 = lean_alloc_closure((void*)(l_Lean_Parser_nonReservedSymbolFn), 3, 1); +lean_closure_set(x_288, 0, x_286); +x_289 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_289, 0, x_287); +lean_ctor_set(x_289, 1, x_288); +x_290 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_290, 0, x_289); +return x_290; } case 13: { -lean_object* x_290; +lean_object* x_291; lean_dec(x_1); -x_290 = l_Lean_Parser_compileParserDescr___main___closed__1; -return x_290; +x_291 = l_Lean_Parser_compileParserDescr___main___closed__1; +return x_291; } case 14: { -lean_object* x_291; +lean_object* x_292; lean_dec(x_1); -x_291 = l_Lean_Parser_compileParserDescr___main___closed__2; -return x_291; +x_292 = l_Lean_Parser_compileParserDescr___main___closed__2; +return x_292; } case 15: { -lean_object* x_292; +lean_object* x_293; lean_dec(x_1); -x_292 = l_Lean_Parser_compileParserDescr___main___closed__3; -return x_292; +x_293 = l_Lean_Parser_compileParserDescr___main___closed__3; +return x_293; } case 16: { -lean_object* x_293; +lean_object* x_294; lean_dec(x_1); -x_293 = l_Lean_Parser_compileParserDescr___main___closed__4; -return x_293; +x_294 = l_Lean_Parser_compileParserDescr___main___closed__4; +return x_294; } case 17: { -lean_object* x_294; +lean_object* x_295; lean_dec(x_1); -x_294 = l_Lean_Parser_compileParserDescr___main___closed__5; -return x_294; +x_295 = l_Lean_Parser_compileParserDescr___main___closed__5; +return x_295; } default: { -lean_object* x_295; lean_object* x_296; lean_object* x_297; -x_295 = lean_ctor_get(x_2, 0); -lean_inc(x_295); -x_296 = lean_ctor_get(x_2, 1); +lean_object* x_296; lean_object* x_297; lean_object* x_298; +x_296 = lean_ctor_get(x_2, 0); lean_inc(x_296); +x_297 = lean_ctor_get(x_2, 1); +lean_inc(x_297); lean_dec(x_2); -x_297 = l_PersistentHashMap_find_x3f___at_Lean_Parser_addLeadingParser___spec__1(x_1, x_295); -if (lean_obj_tag(x_297) == 0) +x_298 = l_PersistentHashMap_find_x3f___at_Lean_Parser_addLeadingParser___spec__1(x_1, x_296); +if (lean_obj_tag(x_298) == 0) { -lean_object* x_298; -lean_dec(x_296); -x_298 = l_Lean_Parser_throwUnknownParserCategory___rarg(x_295); -return x_298; +lean_object* x_299; +lean_dec(x_297); +x_299 = l_Lean_Parser_throwUnknownParserCategory___rarg(x_296); +return x_299; } else { -lean_object* x_299; lean_object* x_300; -lean_dec(x_297); -x_299 = l_Lean_Parser_categoryParser(x_295, x_296); -x_300 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_300, 0, x_299); -return x_300; +lean_object* x_300; lean_object* x_301; +lean_dec(x_298); +x_300 = l_Lean_Parser_categoryParser(x_296, x_297); +x_301 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_301, 0, x_300); +return x_301; } } } @@ -38239,6 +38253,8 @@ l_Lean_Parser_antiquotNestedExpr___closed__7 = _init_l_Lean_Parser_antiquotNeste lean_mark_persistent(l_Lean_Parser_antiquotNestedExpr___closed__7); l_Lean_Parser_antiquotNestedExpr___closed__8 = _init_l_Lean_Parser_antiquotNestedExpr___closed__8(); lean_mark_persistent(l_Lean_Parser_antiquotNestedExpr___closed__8); +l_Lean_Parser_antiquotNestedExpr___closed__9 = _init_l_Lean_Parser_antiquotNestedExpr___closed__9(); +lean_mark_persistent(l_Lean_Parser_antiquotNestedExpr___closed__9); l_Lean_Parser_antiquotNestedExpr = _init_l_Lean_Parser_antiquotNestedExpr(); lean_mark_persistent(l_Lean_Parser_antiquotNestedExpr); l_Lean_Parser_antiquotExpr___closed__1 = _init_l_Lean_Parser_antiquotExpr___closed__1(); diff --git a/stage0/stdlib/Lean/Parser/Syntax.c b/stage0/stdlib/Lean/Parser/Syntax.c index b8a918d689..212a59650a 100644 --- a/stage0/stdlib/Lean/Parser/Syntax.c +++ b/stage0/stdlib/Lean/Parser/Syntax.c @@ -19,6 +19,7 @@ lean_object* l_Lean_Parser_Command_macroHead___closed__3; lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__6; lean_object* l_Lean_Parser_categoryParserOfStack___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Syntax_orelse___closed__5; +extern lean_object* l_Lean_Parser_Tactic_orelse___closed__2; lean_object* l_Lean_Parser_Syntax_many___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__8; lean_object* l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__1; @@ -51,7 +52,6 @@ lean_object* l_Lean_Parser_Syntax_try___elambda__1___closed__1; lean_object* l_Lean_Parser_Syntax_try___closed__3; lean_object* l_Lean_Parser_Syntax_many1___elambda__1___closed__1; extern lean_object* l_Lean_nullKind; -extern lean_object* l_Lean_Parser_Tactic_orelse___closed__1; lean_object* l_Lean_Parser_Syntax_paren___closed__6; lean_object* l_Lean_Parser_Command_syntax___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Syntax_str___elambda__1___closed__5; @@ -199,7 +199,6 @@ lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__5; lean_object* l_Lean_Parser_Syntax_paren___closed__1; lean_object* l_Lean_Parser_Command_macroArg; lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__1; -extern lean_object* l_Lean_Parser_mkAntiquot___closed__5; lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_infix___closed__4; lean_object* l_Lean_Parser_Syntax_char___elambda__1___closed__3; @@ -254,7 +253,6 @@ lean_object* lean_nat_sub(lean_object*, lean_object*); lean_object* l_Lean_Parser_Syntax_sepBy1___closed__2; lean_object* l_Lean_Parser_precedence___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Syntax_try___elambda__1___closed__4; -extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__1; lean_object* l_Lean_Parser_Command_postfix; lean_object* l_Lean_Parser_Command_infix___closed__2; extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__2; @@ -302,6 +300,7 @@ extern lean_object* l_Lean_Parser_Term_tacticStxQuot___closed__2; extern lean_object* l_Lean_Parser_Term_namedHole___elambda__1___closed__8; lean_object* l_Lean_Parser_Syntax_paren___closed__5; extern lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__1; +extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__4; lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__3; lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__1; lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__4; @@ -556,6 +555,7 @@ lean_object* l_Lean_Parser_Command_infixr___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_optKind___closed__1; lean_object* l_Lean_Parser_Syntax_paren___closed__7; lean_object* l_Lean_Parser_Command_optKind; +lean_object* l_Lean_Parser_precedence___closed__6; extern lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_macroTailTactic___closed__2; lean_object* l_Lean_Parser_Syntax_str; @@ -596,6 +596,7 @@ lean_object* l_Lean_Parser_Syntax_lookahead; lean_object* l_Lean_Parser_Command_optKind___closed__5; lean_object* l_Lean_Parser_Command_infix___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_macro__rules___closed__2; +extern lean_object* l_Lean_Parser_Term_stxQuot___closed__1; lean_object* l_Lean_Parser_Command_syntax___closed__9; lean_object* l_Lean_Parser_Command_macroTailDefault___closed__2; extern lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9; @@ -606,6 +607,7 @@ extern lean_object* l_Lean_Parser_regBuiltinTacticParserAttr___closed__4; lean_object* l_Lean_Parser_Command_optKind___closed__3; lean_object* l_Lean_Parser_Command_infixr___closed__4; lean_object* l_Lean_Parser_Syntax_try___elambda__1___closed__3; +extern lean_object* l_Lean_Syntax_decodeNatLitVal___closed__1; lean_object* l_Lean_Parser_Command_macroTailDefault___closed__4; lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__6; lean_object* l_Lean_Parser_Command_identPrec___closed__1; @@ -649,7 +651,6 @@ lean_object* l_Lean_Parser_Command_syntax___closed__8; lean_object* l_Lean_Parser_precedence___closed__4; lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__4; lean_object* l_Lean_Parser_Syntax_num___elambda__1___closed__3; -lean_object* l_Lean_Parser_Command_macroTailTactic___closed__7; lean_object* l_Lean_Parser_Command_infixr___elambda__1___closed__2; lean_object* l_Lean_Parser_optPrecedence___closed__2; lean_object* l___regBuiltinParser_Lean_Parser_Syntax_many1(lean_object*); @@ -1360,38 +1361,48 @@ return x_49; lean_object* _init_l_Lean_Parser_precedence___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_precedenceLit; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_mkAntiquot___closed__5; -x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); -return x_4; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_mkAntiquot___closed__4; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); +return x_3; } } lean_object* _init_l_Lean_Parser_precedence___closed__2() { _start: { +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_precedenceLit; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_precedence___closed__1; +x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_precedence___closed__3() { +_start: +{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_precedence___elambda__1___closed__2; -x_2 = l_Lean_Parser_precedence___closed__1; +x_2 = l_Lean_Parser_precedence___closed__2; x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_precedence___closed__3() { +lean_object* _init_l_Lean_Parser_precedence___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_precedence___elambda__1___closed__4; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_precedence___closed__2; +x_3 = l_Lean_Parser_precedence___closed__3; x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_precedence___closed__4() { +lean_object* _init_l_Lean_Parser_precedence___closed__5() { _start: { lean_object* x_1; @@ -1399,12 +1410,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_precedence___elambda__1), 2, 0); return x_1; } } -lean_object* _init_l_Lean_Parser_precedence___closed__5() { +lean_object* _init_l_Lean_Parser_precedence___closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_precedence___closed__3; -x_2 = l_Lean_Parser_precedence___closed__4; +x_1 = l_Lean_Parser_precedence___closed__4; +x_2 = l_Lean_Parser_precedence___closed__5; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -1415,7 +1426,7 @@ lean_object* _init_l_Lean_Parser_precedence() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_precedence___closed__5; +x_1 = l_Lean_Parser_precedence___closed__6; return x_1; } } @@ -2129,7 +2140,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Syntax_paren___closed__1; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_3 = l_Lean_Parser_antiquotNestedExpr___closed__4; x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); return x_4; } @@ -2138,7 +2149,7 @@ lean_object* _init_l_Lean_Parser_Syntax_paren___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__1; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; x_2 = l_Lean_Parser_Syntax_paren___closed__2; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; @@ -5376,7 +5387,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Syntax_orelse___closed__1; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Tactic_orelse___closed__1; +x_3 = l_Lean_Parser_Tactic_orelse___closed__2; x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); return x_4; } @@ -5934,9 +5945,9 @@ lean_object* _init_l_Lean_Parser_Command_prefix___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_prefix___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_prefix___elambda__1___closed__5; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -6274,9 +6285,9 @@ lean_object* _init_l_Lean_Parser_Command_infix___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_infix___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_infix___elambda__1___closed__5; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -6614,9 +6625,9 @@ lean_object* _init_l_Lean_Parser_Command_infixl___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_infixl___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_infixl___elambda__1___closed__5; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -6954,9 +6965,9 @@ lean_object* _init_l_Lean_Parser_Command_infixr___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_infixr___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_infixr___elambda__1___closed__5; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -7294,9 +7305,9 @@ lean_object* _init_l_Lean_Parser_Command_postfix___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_postfix___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_postfix___elambda__1___closed__5; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -7987,9 +7998,9 @@ lean_object* _init_l_Lean_Parser_Command_reserve___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_reserve___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_reserve___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -8649,7 +8660,7 @@ lean_object* _init_l_Lean_Parser_Command_mixfix___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Command_mixfix___closed__1; @@ -10187,9 +10198,9 @@ lean_object* _init_l_Lean_Parser_Command_notation___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_notation___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_notation___elambda__1___closed__5; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -10673,9 +10684,9 @@ lean_object* _init_l_Lean_Parser_Command_macro__rules___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_macro__rules___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_macro__rules___elambda__1___closed__5; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -11345,9 +11356,9 @@ lean_object* _init_l_Lean_Parser_Command_syntax___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_syntax___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_syntax___elambda__1___closed__5; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -11785,9 +11796,9 @@ lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -12494,7 +12505,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Command_macroArgType; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_mkAntiquot___closed__5; +x_3 = l_Lean_Parser_precedence___closed__1; x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); return x_4; } @@ -13321,45 +13332,35 @@ lean_object* _init_l_Lean_Parser_Command_macroTailTactic___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__4; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_stxQuot___closed__1; +x_2 = l_Lean_Parser_Term_tacticStxQuot___closed__2; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } } lean_object* _init_l_Lean_Parser_Command_macroTailTactic___closed__3() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_macroTailTactic___closed__2; -x_2 = l_Lean_Parser_Term_tacticStxQuot___closed__2; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); -return x_3; +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_darrow; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Command_macroTailTactic___closed__2; +x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); +return x_4; } } lean_object* _init_l_Lean_Parser_Command_macroTailTactic___closed__4() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_darrow; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_Command_macroTailTactic___closed__3; -x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); -return x_4; -} -} -lean_object* _init_l_Lean_Parser_Command_macroTailTactic___closed__5() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Command_macroTailTactic___closed__1; -x_2 = l_Lean_Parser_Command_macroTailTactic___closed__4; +x_2 = l_Lean_Parser_Command_macroTailTactic___closed__3; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Command_macroTailTactic___closed__6() { +lean_object* _init_l_Lean_Parser_Command_macroTailTactic___closed__5() { _start: { lean_object* x_1; @@ -13367,12 +13368,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_macroTailTactic___elambda return x_1; } } -lean_object* _init_l_Lean_Parser_Command_macroTailTactic___closed__7() { +lean_object* _init_l_Lean_Parser_Command_macroTailTactic___closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_macroTailTactic___closed__5; -x_2 = l_Lean_Parser_Command_macroTailTactic___closed__6; +x_1 = l_Lean_Parser_Command_macroTailTactic___closed__4; +x_2 = l_Lean_Parser_Command_macroTailTactic___closed__5; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -13383,7 +13384,7 @@ lean_object* _init_l_Lean_Parser_Command_macroTailTactic() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Command_macroTailTactic___closed__7; +x_1 = l_Lean_Parser_Command_macroTailTactic___closed__6; return x_1; } } @@ -13810,7 +13811,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Term_stxQuot___closed__2; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_3 = l_Lean_Parser_antiquotNestedExpr___closed__4; x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); return x_4; } @@ -13819,7 +13820,7 @@ lean_object* _init_l_Lean_Parser_Command_macroTailCommand___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_macroTailTactic___closed__2; +x_1 = l_Lean_Parser_Term_stxQuot___closed__1; x_2 = l_Lean_Parser_Command_macroTailCommand___closed__1; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; @@ -14296,7 +14297,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Command_macroTailDefault___closed__1; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_3 = l_Lean_Parser_antiquotNestedExpr___closed__4; x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); return x_4; } @@ -14305,7 +14306,7 @@ lean_object* _init_l_Lean_Parser_Command_macroTailDefault___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_macroTailTactic___closed__2; +x_1 = l_Lean_Parser_Term_stxQuot___closed__1; x_2 = l_Lean_Parser_Command_macroTailDefault___closed__2; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; @@ -14315,7 +14316,7 @@ lean_object* _init_l_Lean_Parser_Command_macroTailDefault___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Command_macroTailDefault___closed__3; @@ -14998,9 +14999,9 @@ lean_object* _init_l_Lean_Parser_Command_macro___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Command_macro___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Command_macro___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -15193,6 +15194,8 @@ l_Lean_Parser_precedence___closed__4 = _init_l_Lean_Parser_precedence___closed__ lean_mark_persistent(l_Lean_Parser_precedence___closed__4); l_Lean_Parser_precedence___closed__5 = _init_l_Lean_Parser_precedence___closed__5(); lean_mark_persistent(l_Lean_Parser_precedence___closed__5); +l_Lean_Parser_precedence___closed__6 = _init_l_Lean_Parser_precedence___closed__6(); +lean_mark_persistent(l_Lean_Parser_precedence___closed__6); l_Lean_Parser_precedence = _init_l_Lean_Parser_precedence(); lean_mark_persistent(l_Lean_Parser_precedence); l_Lean_Parser_optPrecedence___closed__1 = _init_l_Lean_Parser_optPrecedence___closed__1(); @@ -16108,8 +16111,6 @@ l_Lean_Parser_Command_macroTailTactic___closed__5 = _init_l_Lean_Parser_Command_ lean_mark_persistent(l_Lean_Parser_Command_macroTailTactic___closed__5); l_Lean_Parser_Command_macroTailTactic___closed__6 = _init_l_Lean_Parser_Command_macroTailTactic___closed__6(); lean_mark_persistent(l_Lean_Parser_Command_macroTailTactic___closed__6); -l_Lean_Parser_Command_macroTailTactic___closed__7 = _init_l_Lean_Parser_Command_macroTailTactic___closed__7(); -lean_mark_persistent(l_Lean_Parser_Command_macroTailTactic___closed__7); l_Lean_Parser_Command_macroTailTactic = _init_l_Lean_Parser_Command_macroTailTactic(); lean_mark_persistent(l_Lean_Parser_Command_macroTailTactic); l_Lean_Parser_Command_macroTailCommand___closed__1 = _init_l_Lean_Parser_Command_macroTailCommand___closed__1(); diff --git a/stage0/stdlib/Lean/Parser/Tactic.c b/stage0/stdlib/Lean/Parser/Tactic.c index 4bc1c60bad..a37138ce1c 100644 --- a/stage0/stdlib/Lean/Parser/Tactic.c +++ b/stage0/stdlib/Lean/Parser/Tactic.c @@ -41,6 +41,7 @@ lean_object* l_Lean_Parser_Tactic_case___closed__6; lean_object* l_Lean_Parser_andthenInfo(lean_object*, lean_object*); lean_object* l_Lean_Parser_ParserState_mkError(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_apply___closed__2; +extern lean_object* l_Lean_Parser_Term_structInst___closed__1; lean_object* l_Lean_Parser_Tactic_clear___elambda__1___closed__2; lean_object* l_Lean_Parser_Tactic_generalize___closed__2; lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1(lean_object*, lean_object*); @@ -68,7 +69,6 @@ lean_object* l_Lean_Parser_Tactic_subst___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_traceState___elambda__1___closed__5; lean_object* l_Lean_Parser_Tactic_intro___closed__4; lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__3; -extern lean_object* l_Lean_Parser_Term_tacticBlock___closed__3; lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__7; lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__8; lean_object* l___regBuiltinParser_Lean_Parser_Tactic_nestedTacticBlock(lean_object*); @@ -102,6 +102,7 @@ lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__4; lean_object* l_Lean_Parser_Tactic_inductionAlt; lean_object* l_Lean_Parser_Tactic_clear___elambda__1___closed__7; lean_object* l_Lean_Parser_Tactic_usingRec___closed__1; +lean_object* l_Lean_Parser_Tactic_orelse___closed__7; extern lean_object* l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__2___closed__6; lean_object* l_Lean_Parser_Tactic_underscore; lean_object* l_Lean_Parser_Tactic_traceState___elambda__1___closed__4; @@ -225,12 +226,12 @@ lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__5; lean_object* l_Lean_Parser_nodeInfo(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__5; lean_object* l_Lean_Parser_Tactic_assumption___closed__1; +lean_object* l_Lean_Parser_Tactic_generalize___closed__12; lean_object* l_Lean_Parser_Tactic_apply___closed__3; lean_object* l_Lean_Parser_Tactic_clear___closed__5; lean_object* lean_nat_sub(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__2; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__7(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); -extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__1; lean_object* l_Lean_Parser_Tactic_revert; lean_object* l_Lean_Parser_Tactic_generalize; lean_object* l_Lean_Parser_Tactic_failIfSuccess___closed__3; @@ -263,6 +264,7 @@ lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__7; lean_object* l_Lean_Parser_optionaInfo(lean_object*); lean_object* l_Lean_Parser_Tactic_cases___closed__2; lean_object* l_Lean_Parser_Tactic_generalize___elambda__1(lean_object*, lean_object*); +extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__4; lean_object* l_Lean_Parser_Tactic_induction___closed__7; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_revert___closed__5; @@ -298,7 +300,6 @@ extern lean_object* l_Lean_Parser_termParser___closed__2; lean_object* lean_name_mk_string(lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_match___closed__2; lean_object* l_Lean_Parser_Tactic_usingRec___elambda__1___closed__5; -lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___closed__6; lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__7; lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__10; lean_object* l_Lean_Parser_Tactic_majorPremise___closed__5; @@ -448,6 +449,7 @@ extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__11; lean_object* l_Lean_Parser_Tactic_majorPremise___elambda__1___closed__4; lean_object* l_Lean_Parser_categoryParser___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_generalizingVars___closed__2; +extern lean_object* l_Lean_Parser_Term_tacticBlock___closed__4; lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__11; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_generalizingVars___elambda__1___closed__1; @@ -479,7 +481,6 @@ lean_object* l_String_trim(lean_object*); lean_object* l_Lean_Parser_Tactic_nonEmptySeq___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_apply___closed__1; lean_object* l___regBuiltinParser_Lean_Parser_Tactic_assumption(lean_object*); -extern lean_object* l_Lean_Parser_Term_implicitBinder___closed__1; extern lean_object* l_Lean_Parser_Term_matchAlts___closed__1; lean_object* l_Lean_Parser_Tactic_underscoreFn___closed__2; lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__13; @@ -498,7 +499,6 @@ lean_object* l_Lean_Parser_Tactic_intro___closed__2; lean_object* l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__4(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__17; lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t); -lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___closed__5; lean_object* l_Lean_Parser_Tactic_cases___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_underscoreFn___closed__1; lean_object* l_Lean_Parser_Tactic_failIfSuccess___elambda__1___closed__4; @@ -528,6 +528,7 @@ lean_object* l_Lean_Parser_Tactic_revert___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_orelse___closed__6; lean_object* l_Lean_Parser_Tactic_intro___closed__5; lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__1; +extern lean_object* l_Lean_Syntax_decodeNatLitVal___closed__1; lean_object* l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__7; lean_object* l___regBuiltinParser_Lean_Parser_Tactic_skip(lean_object*); @@ -3071,7 +3072,7 @@ lean_object* _init_l_Lean_Parser_Tactic_apply___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Tactic_apply___closed__1; @@ -3357,7 +3358,7 @@ lean_object* _init_l_Lean_Parser_Tactic_exact___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Tactic_exact___closed__1; @@ -3643,7 +3644,7 @@ lean_object* _init_l_Lean_Parser_Tactic_refine___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Tactic_refine___closed__1; @@ -6302,52 +6303,52 @@ return x_3; lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__3() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); -return x_3; +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(50u); +x_2 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; } } lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__4() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_ident; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_Tactic_generalize___closed__3; -x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); -return x_4; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__6; +x_2 = l_Lean_Parser_Tactic_generalize___closed__3; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); +return x_3; } } lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Tactic_generalize___closed__2; +x_1 = l_Lean_Parser_ident; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Tactic_generalize___closed__4; -x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); +x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); return x_4; } } lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__6() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_optIdent___closed__2; -x_2 = l_Lean_Parser_Tactic_generalize___closed__5; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); -return x_3; +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_generalize___closed__2; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Tactic_generalize___closed__5; +x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); +return x_4; } } lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__7() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Tactic_generalize___closed__1; +x_1 = l_Lean_Parser_Term_optIdent___closed__2; x_2 = l_Lean_Parser_Tactic_generalize___closed__6; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; @@ -6357,25 +6358,35 @@ lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_1 = l_Lean_Parser_Tactic_generalize___closed__1; x_2 = l_Lean_Parser_Tactic_generalize___closed__7; -x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } } lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__9() { _start: { +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_2 = l_Lean_Parser_Tactic_generalize___closed__8; +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__10() { +_start: +{ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__4; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Tactic_generalize___closed__8; +x_3 = l_Lean_Parser_Tactic_generalize___closed__9; x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__10() { +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__11() { _start: { lean_object* x_1; @@ -6383,12 +6394,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_generalize___elambda__1), return x_1; } } -lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__11() { +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__12() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Tactic_generalize___closed__9; -x_2 = l_Lean_Parser_Tactic_generalize___closed__10; +x_1 = l_Lean_Parser_Tactic_generalize___closed__10; +x_2 = l_Lean_Parser_Tactic_generalize___closed__11; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -6399,7 +6410,7 @@ lean_object* _init_l_Lean_Parser_Tactic_generalize() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Tactic_generalize___closed__11; +x_1 = l_Lean_Parser_Tactic_generalize___closed__12; return x_1; } } @@ -7047,7 +7058,7 @@ lean_object* _init_l_Lean_Parser_Tactic_majorPremise___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_optIdent___closed__2; @@ -9662,9 +9673,9 @@ lean_object* _init_l_Lean_Parser_Tactic_usingRec___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Tactic_usingRec___elambda__1___closed__2; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Tactic_usingRec___elambda__1___closed__2; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -9961,9 +9972,9 @@ lean_object* _init_l_Lean_Parser_Tactic_generalizingVars___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Tactic_generalizingVars___elambda__1___closed__2; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Tactic_generalizingVars___elambda__1___closed__2; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -11264,7 +11275,7 @@ lean_object* _init_l_Lean_Parser_Tactic_injection___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Tactic_withIds; @@ -11772,7 +11783,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Tactic_nonEmptySeq; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_3 = l_Lean_Parser_antiquotNestedExpr___closed__4; x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); return x_4; } @@ -11781,7 +11792,7 @@ lean_object* _init_l_Lean_Parser_Tactic_paren___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__1; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; x_2 = l_Lean_Parser_Tactic_paren___closed__1; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; @@ -12280,45 +12291,25 @@ lean_object* _init_l_Lean_Parser_Tactic_nestedTacticBlock___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_tacticBlock___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__2; +x_2 = l_Lean_Parser_Term_tacticBlock___closed__4; +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } lean_object* _init_l_Lean_Parser_Tactic_nestedTacticBlock___closed__2() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Tactic_nestedTacticBlock___closed__1; -x_2 = l_Lean_Parser_Term_tacticBlock___closed__3; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Tactic_nestedTacticBlock___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__2; -x_2 = l_Lean_Parser_Tactic_nestedTacticBlock___closed__2; -x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Tactic_nestedTacticBlock___closed__4() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__4; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Tactic_nestedTacticBlock___closed__3; +x_3 = l_Lean_Parser_Tactic_nestedTacticBlock___closed__1; x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_Tactic_nestedTacticBlock___closed__5() { +lean_object* _init_l_Lean_Parser_Tactic_nestedTacticBlock___closed__3() { _start: { lean_object* x_1; @@ -12326,12 +12317,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_nestedTacticBlock___elambd return x_1; } } -lean_object* _init_l_Lean_Parser_Tactic_nestedTacticBlock___closed__6() { +lean_object* _init_l_Lean_Parser_Tactic_nestedTacticBlock___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Tactic_nestedTacticBlock___closed__4; -x_2 = l_Lean_Parser_Tactic_nestedTacticBlock___closed__5; +x_1 = l_Lean_Parser_Tactic_nestedTacticBlock___closed__2; +x_2 = l_Lean_Parser_Tactic_nestedTacticBlock___closed__3; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -12342,7 +12333,7 @@ lean_object* _init_l_Lean_Parser_Tactic_nestedTacticBlock() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Tactic_nestedTacticBlock___closed__6; +x_1 = l_Lean_Parser_Tactic_nestedTacticBlock___closed__4; return x_1; } } @@ -12801,7 +12792,7 @@ lean_object* _init_l_Lean_Parser_Tactic_nestedTacticBlockCurly___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_implicitBinder___closed__1; +x_1 = l_Lean_Parser_Term_structInst___closed__1; x_2 = l_Lean_Parser_Tactic_nestedTacticBlockCurly___closed__1; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; @@ -13016,46 +13007,56 @@ return x_13; lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__2; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); -return x_3; +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(2u); +x_2 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; } } lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__2; +x_2 = l_Lean_Parser_Tactic_orelse___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_regBuiltinTacticParserAttr___closed__4; x_2 = lean_unsigned_to_nat(1u); x_3 = l_Lean_Parser_categoryParser(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__3() { +lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Tactic_orelse___closed__2; +x_1 = l_Lean_Parser_Tactic_orelse___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Tactic_orelse___closed__1; +x_3 = l_Lean_Parser_Tactic_orelse___closed__2; x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); return x_4; } } -lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__4() { +lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__1; -x_2 = l_Lean_Parser_Tactic_orelse___closed__3; +x_2 = l_Lean_Parser_Tactic_orelse___closed__4; x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__5() { +lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__6() { _start: { lean_object* x_1; @@ -13063,12 +13064,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_orelse___elambda__1), 2, 0 return x_1; } } -lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__6() { +lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__7() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Tactic_orelse___closed__4; -x_2 = l_Lean_Parser_Tactic_orelse___closed__5; +x_1 = l_Lean_Parser_Tactic_orelse___closed__5; +x_2 = l_Lean_Parser_Tactic_orelse___closed__6; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -13079,7 +13080,7 @@ lean_object* _init_l_Lean_Parser_Tactic_orelse() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Tactic_orelse___closed__6; +x_1 = l_Lean_Parser_Tactic_orelse___closed__7; return x_1; } } @@ -13624,6 +13625,8 @@ l_Lean_Parser_Tactic_generalize___closed__10 = _init_l_Lean_Parser_Tactic_genera lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__10); l_Lean_Parser_Tactic_generalize___closed__11 = _init_l_Lean_Parser_Tactic_generalize___closed__11(); lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__11); +l_Lean_Parser_Tactic_generalize___closed__12 = _init_l_Lean_Parser_Tactic_generalize___closed__12(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__12); l_Lean_Parser_Tactic_generalize = _init_l_Lean_Parser_Tactic_generalize(); lean_mark_persistent(l_Lean_Parser_Tactic_generalize); res = l___regBuiltinParser_Lean_Parser_Tactic_generalize(lean_io_mk_world()); @@ -13907,10 +13910,6 @@ l_Lean_Parser_Tactic_nestedTacticBlock___closed__3 = _init_l_Lean_Parser_Tactic_ lean_mark_persistent(l_Lean_Parser_Tactic_nestedTacticBlock___closed__3); l_Lean_Parser_Tactic_nestedTacticBlock___closed__4 = _init_l_Lean_Parser_Tactic_nestedTacticBlock___closed__4(); lean_mark_persistent(l_Lean_Parser_Tactic_nestedTacticBlock___closed__4); -l_Lean_Parser_Tactic_nestedTacticBlock___closed__5 = _init_l_Lean_Parser_Tactic_nestedTacticBlock___closed__5(); -lean_mark_persistent(l_Lean_Parser_Tactic_nestedTacticBlock___closed__5); -l_Lean_Parser_Tactic_nestedTacticBlock___closed__6 = _init_l_Lean_Parser_Tactic_nestedTacticBlock___closed__6(); -lean_mark_persistent(l_Lean_Parser_Tactic_nestedTacticBlock___closed__6); l_Lean_Parser_Tactic_nestedTacticBlock = _init_l_Lean_Parser_Tactic_nestedTacticBlock(); lean_mark_persistent(l_Lean_Parser_Tactic_nestedTacticBlock); res = l___regBuiltinParser_Lean_Parser_Tactic_nestedTacticBlock(lean_io_mk_world()); @@ -13963,6 +13962,8 @@ l_Lean_Parser_Tactic_orelse___closed__5 = _init_l_Lean_Parser_Tactic_orelse___cl lean_mark_persistent(l_Lean_Parser_Tactic_orelse___closed__5); l_Lean_Parser_Tactic_orelse___closed__6 = _init_l_Lean_Parser_Tactic_orelse___closed__6(); lean_mark_persistent(l_Lean_Parser_Tactic_orelse___closed__6); +l_Lean_Parser_Tactic_orelse___closed__7 = _init_l_Lean_Parser_Tactic_orelse___closed__7(); +lean_mark_persistent(l_Lean_Parser_Tactic_orelse___closed__7); l_Lean_Parser_Tactic_orelse = _init_l_Lean_Parser_Tactic_orelse(); lean_mark_persistent(l_Lean_Parser_Tactic_orelse); res = l___regBuiltinParser_Lean_Parser_Tactic_orelse(lean_io_mk_world()); diff --git a/stage0/stdlib/Lean/Parser/Term.c b/stage0/stdlib/Lean/Parser/Term.c index 65a709e3fc..de086ed00c 100644 --- a/stage0/stdlib/Lean/Parser/Term.c +++ b/stage0/stdlib/Lean/Parser/Term.c @@ -43,7 +43,6 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_iff(lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Term_suffices(lean_object*); lean_object* l_Lean_Parser_Term_arrayLit___closed__3; lean_object* l_Lean_Parser_Term_explicit___elambda__1___closed__4; -lean_object* l_Lean_Parser_Term_doLet___closed__6; lean_object* l_Lean_Parser_Term_if___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_subst; lean_object* l_Lean_Parser_darrow___elambda__1___closed__2; @@ -274,7 +273,6 @@ extern lean_object* l_Lean_Parser_pushNone; lean_object* l_Lean_Parser_Term_subst___elambda__1___closed__1; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_match___elambda__1___closed__8; -lean_object* l_Lean_Parser_Term_subst___closed__9; lean_object* l_Lean_Parser_Term_binderTactic___closed__7; lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_show___elambda__1___closed__2; @@ -457,12 +455,10 @@ lean_object* l_Lean_Parser_Term_parenSpecial___closed__1; lean_object* l_Lean_Parser_Term_not___elambda__1___closed__5; lean_object* l_Lean_Parser_Tactic_seq___closed__6; lean_object* l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__3; -lean_object* l_Lean_Parser_Term_listLit___closed__9; lean_object* l_Lean_Parser_Term_structInstLVal___closed__9; lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_show___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_tupleTail___elambda__1(lean_object*, lean_object*); -extern lean_object* l_Lean_Parser_Level_paren___closed__3; lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_forall___closed__7; lean_object* l___regBuiltinParser_Lean_Parser_Term_tparser_x21(lean_object*); @@ -822,7 +818,6 @@ lean_object* l_Lean_Parser_Term_le___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_div___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_borrowed___elambda__1(lean_object*, lean_object*); lean_object* l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__3; -lean_object* l_Lean_Parser_Term_where___closed__9; lean_object* l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_subst___elambda__1___spec__2___closed__3; lean_object* l_Lean_Parser_Term_bracketedDoSeq___closed__4; lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1(lean_object*, lean_object*, lean_object*); @@ -989,6 +984,7 @@ lean_object* l_Lean_Parser_strAux___main(lean_object*, lean_object*, lean_object lean_object* l_Lean_Parser_Term_fun___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___closed__8; lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__9; +extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__5; lean_object* l_Lean_Parser_Term_cdot___closed__5; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_tupleTail___elambda__1___spec__1(uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_num___closed__1; @@ -1276,7 +1272,6 @@ lean_object* l_Lean_Parser_Term_iff___elambda__1___closed__4; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_matchAlts___elambda__1___spec__5(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__9; lean_object* l_Lean_Parser_Term_typeAscription___closed__3; -extern lean_object* l_Lean_Parser_Level_paren___closed__4; lean_object* l_Lean_Parser_Term_have___closed__10; lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__15; lean_object* l_Lean_Parser_Term_borrowed___closed__7; @@ -1410,7 +1405,6 @@ lean_object* l_Lean_Parser_ident___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_byTactic___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_binderIdent; lean_object* l_Lean_Parser_Term_simpleBinder___elambda__1(lean_object*, lean_object*); -lean_object* l_Lean_Parser_Term_implicitBinder___closed__3; lean_object* l_Lean_Parser_Term_infixR(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_seqLeft___closed__3; lean_object* l_Lean_Parser_charLit___elambda__1(lean_object*, lean_object*); @@ -1728,7 +1722,6 @@ lean_object* l_Lean_Parser_Term_beq___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_binderDefault___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_haveAssign; lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__3; -lean_object* l_Lean_Parser_Term_explicit___closed__6; lean_object* l_Lean_Parser_Term_suffices___closed__5; lean_object* l_Lean_Parser_Term_parser_x21___closed__2; lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__3; @@ -1942,7 +1935,6 @@ lean_object* l_Lean_Parser_Term_map___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_sort___elambda__1___closed__9; lean_object* l___regBuiltinParser_Lean_Parser_Term_gt(lean_object*); lean_object* l_Lean_Parser_Term_app___closed__2; -lean_object* l_Lean_Parser_Term_explicit___closed__5; lean_object* l_Lean_Parser_Term_do___elambda__1___closed__5; lean_object* l_Lean_Parser_regBuiltinTacticParserAttr___closed__4; lean_object* l_Lean_Parser_Term_mapConstRev___closed__2; @@ -1960,6 +1952,7 @@ lean_object* l_Lean_Parser_Term_mapRev___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_uminus___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_bindOp___elambda__1___closed__1; +extern lean_object* l_Lean_Syntax_decodeNatLitVal___closed__1; lean_object* l_Lean_Parser_Term_suffices; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_matchAlts___elambda__1___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_mapConstRev; @@ -2577,9 +2570,9 @@ lean_object* _init_l_Lean_Parser_Tactic_seq___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__1; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__1; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -2858,9 +2851,9 @@ lean_object* _init_l_Lean_Parser_darrow___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_darrow___elambda__1___closed__2; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_darrow___elambda__1___closed__2; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -3989,9 +3982,9 @@ lean_object* _init_l_Lean_Parser_Term_explicitUniv___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -3999,9 +3992,9 @@ lean_object* _init_l_Lean_Parser_Term_explicitUniv___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__1; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__1; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -4009,7 +4002,7 @@ lean_object* _init_l_Lean_Parser_Term_explicitUniv___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Level_paren___closed__3; +x_1 = l_Lean_Parser_Level_paren___closed__1; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_explicitUniv___closed__2; @@ -4021,9 +4014,9 @@ lean_object* _init_l_Lean_Parser_Term_explicitUniv___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__7; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__7; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -4486,9 +4479,9 @@ lean_object* _init_l_Lean_Parser_Term_namedPattern___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_namedPattern___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_namedPattern___elambda__1___closed__6; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -5808,7 +5801,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_type___elambda__1___closed__6; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -6168,7 +6161,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_sort___elambda__1___closed__6; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -6528,7 +6521,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_prop___elambda__1___closed__6; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -7197,7 +7190,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_namedHole___elambda__1___closed__5; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -7561,7 +7554,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_sorry___elambda__1___closed__5; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -7921,7 +7914,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_cdot___elambda__1___closed__6; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -8281,7 +8274,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_emptyC___elambda__1___closed__6; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -8670,9 +8663,9 @@ lean_object* _init_l_Lean_Parser_Term_typeAscription___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__5; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -8680,7 +8673,7 @@ lean_object* _init_l_Lean_Parser_Term_typeAscription___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_typeAscription___closed__1; @@ -9243,7 +9236,7 @@ lean_object* _init_l_Lean_Parser_Term_tupleTail___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_explicitUniv___closed__2; @@ -10070,7 +10063,7 @@ lean_object* _init_l_Lean_Parser_Term_paren___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_parenSpecial; @@ -10094,7 +10087,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_paren___closed__2; -x_2 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__4; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } @@ -10103,7 +10096,7 @@ lean_object* _init_l_Lean_Parser_Term_paren___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Level_paren___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; x_2 = l_Lean_Parser_Term_paren___closed__3; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; @@ -10701,7 +10694,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__5; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -10710,7 +10703,7 @@ lean_object* _init_l_Lean_Parser_Term_anonymousCtor___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_explicitUniv___closed__2; @@ -10722,9 +10715,9 @@ lean_object* _init_l_Lean_Parser_Term_anonymousCtor___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -11927,9 +11920,9 @@ lean_object* _init_l_Lean_Parser_Term_if___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_if___elambda__1___closed__8; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_if___elambda__1___closed__8; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -11937,9 +11930,9 @@ lean_object* _init_l_Lean_Parser_Term_if___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_if___elambda__1___closed__10; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_if___elambda__1___closed__10; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -11947,7 +11940,7 @@ lean_object* _init_l_Lean_Parser_Term_if___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_if___closed__4; @@ -11959,7 +11952,7 @@ lean_object* _init_l_Lean_Parser_Term_if___closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_if___closed__5; @@ -11981,7 +11974,7 @@ lean_object* _init_l_Lean_Parser_Term_if___closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_if___closed__7; @@ -12403,9 +12396,9 @@ lean_object* _init_l_Lean_Parser_Term_fromTerm___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_fromTerm___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_fromTerm___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -12413,7 +12406,7 @@ lean_object* _init_l_Lean_Parser_Term_fromTerm___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_fromTerm___closed__1; @@ -12793,9 +12786,9 @@ lean_object* _init_l_Lean_Parser_Term_haveAssign___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_haveAssign___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_haveAssign___elambda__1___closed__5; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -12803,7 +12796,7 @@ lean_object* _init_l_Lean_Parser_Term_haveAssign___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_haveAssign___closed__1; @@ -13629,7 +13622,7 @@ lean_object* _init_l_Lean_Parser_Term_have___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Tactic_seq___closed__2; @@ -13651,7 +13644,7 @@ lean_object* _init_l_Lean_Parser_Term_have___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_have___closed__4; @@ -14331,7 +14324,7 @@ lean_object* _init_l_Lean_Parser_Term_suffices___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_suffices___closed__2; @@ -14799,7 +14792,7 @@ lean_object* _init_l_Lean_Parser_Term_show___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_fromTerm; @@ -15398,9 +15391,9 @@ lean_object* _init_l_Lean_Parser_Term_structInstArrayRef___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__5; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -15408,9 +15401,9 @@ lean_object* _init_l_Lean_Parser_Term_structInstArrayRef___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -15418,7 +15411,7 @@ lean_object* _init_l_Lean_Parser_Term_structInstArrayRef___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_structInstArrayRef___closed__2; @@ -16033,9 +16026,9 @@ lean_object* _init_l_Lean_Parser_Term_structInstLVal___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_structInstLVal___elambda__1___spec__1___closed__1; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_structInstLVal___elambda__1___spec__1___closed__1; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -18287,7 +18280,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_structInst___elambda__1___closed__5; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -18296,9 +18289,9 @@ lean_object* _init_l_Lean_Parser_Term_structInst___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_structInst___elambda__1___closed__7; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_structInst___elambda__1___closed__7; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -18306,7 +18299,7 @@ lean_object* _init_l_Lean_Parser_Term_structInst___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_structInst___closed__2; @@ -18339,9 +18332,9 @@ lean_object* _init_l_Lean_Parser_Term_structInst___closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_structInst___elambda__1___closed__8; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_structInst___elambda__1___closed__8; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -18358,7 +18351,7 @@ lean_object* _init_l_Lean_Parser_Term_structInst___closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_typeAscription___closed__1; @@ -19633,9 +19626,9 @@ lean_object* _init_l_Lean_Parser_Term_subtype___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_subtype___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_subtype___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -19643,7 +19636,7 @@ lean_object* _init_l_Lean_Parser_Term_subtype___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_explicitUniv___closed__4; @@ -20458,8 +20451,8 @@ lean_object* _init_l_Lean_Parser_Term_listLit___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__5; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_1 = l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__1; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -20467,31 +20460,31 @@ return x_3; lean_object* _init_l_Lean_Parser_Term_listLit___closed__2() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__1; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); -return x_3; +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Term_listLit___closed__1; +x_4 = l_Lean_Parser_sepByInfo(x_2, x_3); +return x_4; } } lean_object* _init_l_Lean_Parser_Term_listLit___closed__3() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_Term_listLit___closed__2; -x_4 = l_Lean_Parser_sepByInfo(x_2, x_3); -return x_4; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_listLit___closed__2; +x_2 = l_Lean_Parser_Term_structInstArrayRef___closed__2; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; } } lean_object* _init_l_Lean_Parser_Term_listLit___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_listLit___closed__3; -x_2 = l_Lean_Parser_Term_structInstArrayRef___closed__2; +x_1 = l_Lean_Parser_Term_structInstArrayRef___closed__1; +x_2 = l_Lean_Parser_Term_listLit___closed__3; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } @@ -20500,35 +20493,25 @@ lean_object* _init_l_Lean_Parser_Term_listLit___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_listLit___closed__1; +x_1 = l_Lean_Parser_Term_listLit___elambda__1___closed__2; x_2 = l_Lean_Parser_Term_listLit___closed__4; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } lean_object* _init_l_Lean_Parser_Term_listLit___closed__6() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_listLit___elambda__1___closed__2; -x_2 = l_Lean_Parser_Term_listLit___closed__5; -x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_listLit___closed__7() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Term_listLit___elambda__1___closed__4; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Term_listLit___closed__6; +x_3 = l_Lean_Parser_Term_listLit___closed__5; x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_Term_listLit___closed__8() { +lean_object* _init_l_Lean_Parser_Term_listLit___closed__7() { _start: { lean_object* x_1; @@ -20536,12 +20519,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_listLit___elambda__1), 2, 0) return x_1; } } -lean_object* _init_l_Lean_Parser_Term_listLit___closed__9() { +lean_object* _init_l_Lean_Parser_Term_listLit___closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_listLit___closed__7; -x_2 = l_Lean_Parser_Term_listLit___closed__8; +x_1 = l_Lean_Parser_Term_listLit___closed__6; +x_2 = l_Lean_Parser_Term_listLit___closed__7; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -20552,7 +20535,7 @@ lean_object* _init_l_Lean_Parser_Term_listLit() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Term_listLit___closed__9; +x_1 = l_Lean_Parser_Term_listLit___closed__8; return x_1; } } @@ -21067,7 +21050,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__5; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -21077,7 +21060,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_arrayLit___closed__1; -x_2 = l_Lean_Parser_Term_listLit___closed__4; +x_2 = l_Lean_Parser_Term_listLit___closed__3; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } @@ -21425,9 +21408,9 @@ lean_object* _init_l_Lean_Parser_Term_explicit___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_namedPattern___elambda__1___closed__6; -x_2 = l_Lean_Parser_Level_paren___closed__1; -x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); +x_1 = l_Lean_Parser_Term_explicit___elambda__1___closed__2; +x_2 = l_Lean_Parser_Term_namedPattern___closed__3; +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } @@ -21435,37 +21418,15 @@ lean_object* _init_l_Lean_Parser_Term_explicit___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Term_namedPattern___closed__2; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_Term_explicit___closed__1; -x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); -return x_4; -} -} -lean_object* _init_l_Lean_Parser_Term_explicit___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_explicit___elambda__1___closed__2; -x_2 = l_Lean_Parser_Term_explicit___closed__2; -x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_explicit___closed__4() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Term_explicit___elambda__1___closed__4; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Term_explicit___closed__3; +x_3 = l_Lean_Parser_Term_explicit___closed__1; x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_Term_explicit___closed__5() { +lean_object* _init_l_Lean_Parser_Term_explicit___closed__3() { _start: { lean_object* x_1; @@ -21473,12 +21434,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_explicit___elambda__1), 2, 0 return x_1; } } -lean_object* _init_l_Lean_Parser_Term_explicit___closed__6() { +lean_object* _init_l_Lean_Parser_Term_explicit___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_explicit___closed__4; -x_2 = l_Lean_Parser_Term_explicit___closed__5; +x_1 = l_Lean_Parser_Term_explicit___closed__2; +x_2 = l_Lean_Parser_Term_explicit___closed__3; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -21489,7 +21450,7 @@ lean_object* _init_l_Lean_Parser_Term_explicit() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Term_explicit___closed__6; +x_1 = l_Lean_Parser_Term_explicit___closed__4; return x_1; } } @@ -21990,7 +21951,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_inaccessible___elambda__1___closed__6; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -22000,7 +21961,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_inaccessible___closed__1; -x_2 = l_Lean_Parser_antiquotNestedExpr___closed__4; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__5; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } @@ -23109,9 +23070,9 @@ lean_object* _init_l_Lean_Parser_Term_binderTactic___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_binderTactic___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_binderTactic___elambda__1___closed__6; +x_2 = l_Lean_Parser_Term_if___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -23708,7 +23669,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_explicitBinder___closed__5; -x_2 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__4; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } @@ -23749,7 +23710,7 @@ x_12 = l_Lean_Parser_Term_explicitBinder___closed__2; x_13 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2); lean_closure_set(x_13, 0, x_12); lean_closure_set(x_13, 1, x_10); -x_14 = l_Lean_Parser_antiquotNestedExpr___closed__1; +x_14 = l_Lean_Parser_antiquotNestedExpr___closed__2; x_15 = l_Lean_Parser_andthenInfo(x_14, x_11); x_16 = l_Lean_Parser_Term_explicitBinder___closed__1; x_17 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2); @@ -23896,16 +23857,6 @@ return x_18; lean_object* _init_l_Lean_Parser_Term_implicitBinder___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_structInst___elambda__1___closed__5; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_implicitBinder___closed__2() { -_start: -{ lean_object* x_1; lean_object* x_2; x_1 = l_Lean_Parser_Term_structInst___elambda__1___closed__5; x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1); @@ -23913,7 +23864,7 @@ lean_closure_set(x_2, 0, x_1); return x_2; } } -lean_object* _init_l_Lean_Parser_Term_implicitBinder___closed__3() { +lean_object* _init_l_Lean_Parser_Term_implicitBinder___closed__2() { _start: { lean_object* x_1; lean_object* x_2; @@ -23938,7 +23889,7 @@ x_7 = l_Lean_Parser_andthenInfo(x_5, x_6); x_8 = lean_ctor_get(x_4, 1); lean_inc(x_8); lean_dec(x_4); -x_9 = l_Lean_Parser_Term_implicitBinder___closed__3; +x_9 = l_Lean_Parser_Term_implicitBinder___closed__2; x_10 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2); lean_closure_set(x_10, 0, x_8); lean_closure_set(x_10, 1, x_9); @@ -23947,9 +23898,9 @@ x_12 = l_Lean_Parser_Term_explicitBinder___closed__2; x_13 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2); lean_closure_set(x_13, 0, x_12); lean_closure_set(x_13, 1, x_10); -x_14 = l_Lean_Parser_Term_implicitBinder___closed__1; +x_14 = l_Lean_Parser_Term_structInst___closed__1; x_15 = l_Lean_Parser_andthenInfo(x_14, x_11); -x_16 = l_Lean_Parser_Term_implicitBinder___closed__2; +x_16 = l_Lean_Parser_Term_implicitBinder___closed__1; x_17 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2); lean_closure_set(x_17, 0, x_16); lean_closure_set(x_17, 1, x_13); @@ -24982,7 +24933,7 @@ lean_object* _init_l_Lean_Parser_Term_depArrow___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_depArrow___closed__1; @@ -26263,7 +26214,7 @@ lean_object* _init_l_Lean_Parser_Term_forall___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_explicitUniv___closed__2; @@ -27041,7 +26992,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj x_1 = l_Lean_Parser_darrow; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_3 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_4 = lean_ctor_get(x_3, 0); lean_inc(x_4); x_5 = l_Lean_Parser_andthenInfo(x_2, x_4); @@ -27154,7 +27105,7 @@ lean_object* _init_l_Lean_Parser_Term_matchAlt___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_explicitUniv___closed__2; @@ -27191,7 +27142,7 @@ lean_object* _init_l_Lean_Parser_Term_matchAlt___closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_darrow; @@ -30086,9 +30037,9 @@ lean_object* _init_l_Lean_Parser_Term_matchAlts___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__2___closed__2; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__2___closed__2; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -31055,9 +31006,9 @@ lean_object* _init_l_Lean_Parser_Term_match___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_match___elambda__1___closed__8; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_match___elambda__1___closed__8; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -31507,7 +31458,7 @@ lean_object* _init_l_Lean_Parser_Term_nomatch___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_nomatch___closed__1; @@ -31917,7 +31868,7 @@ lean_object* _init_l_Lean_Parser_Term_parser_x21___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_parser_x21___closed__1; @@ -32327,7 +32278,7 @@ lean_object* _init_l_Lean_Parser_Term_tparser_x21___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_tparser_x21___closed__1; @@ -32728,7 +32679,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_borrowed___elambda__1___closed__6; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -33513,7 +33464,7 @@ lean_object* _init_l_Lean_Parser_Term_match__syntax___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_match___closed__3; @@ -33801,7 +33752,7 @@ lean_object* _init_l_Lean_Parser_Term_letIdDecl___closed__7() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_letIdDecl___closed__4; @@ -34104,7 +34055,7 @@ lean_object* _init_l_Lean_Parser_Term_letPatDecl___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_letPatDecl___closed__2; @@ -34116,7 +34067,7 @@ lean_object* _init_l_Lean_Parser_Term_letPatDecl___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_letPatDecl___closed__3; @@ -34918,7 +34869,7 @@ lean_object* _init_l_Lean_Parser_Term_let___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Tactic_seq___closed__2; @@ -35994,48 +35945,38 @@ return x_49; lean_object* _init_l_Lean_Parser_Term_doLet___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_let___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); -return x_3; +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Term_letDecl; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Term_let___closed__1; +x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); +return x_4; } } lean_object* _init_l_Lean_Parser_Term_doLet___closed__2() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Term_letDecl; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_Term_doLet___closed__1; -x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); -return x_4; -} -} -lean_object* _init_l_Lean_Parser_Term_doLet___closed__3() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_doLet___elambda__1___closed__2; -x_2 = l_Lean_Parser_Term_doLet___closed__2; +x_2 = l_Lean_Parser_Term_doLet___closed__1; x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_doLet___closed__4() { +lean_object* _init_l_Lean_Parser_Term_doLet___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Term_doLet___elambda__1___closed__4; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Term_doLet___closed__3; +x_3 = l_Lean_Parser_Term_doLet___closed__2; x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_Term_doLet___closed__5() { +lean_object* _init_l_Lean_Parser_Term_doLet___closed__4() { _start: { lean_object* x_1; @@ -36043,12 +35984,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_doLet___elambda__1), 2, 0); return x_1; } } -lean_object* _init_l_Lean_Parser_Term_doLet___closed__6() { +lean_object* _init_l_Lean_Parser_Term_doLet___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_doLet___closed__4; -x_2 = l_Lean_Parser_Term_doLet___closed__5; +x_1 = l_Lean_Parser_Term_doLet___closed__3; +x_2 = l_Lean_Parser_Term_doLet___closed__4; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -36059,7 +36000,7 @@ lean_object* _init_l_Lean_Parser_Term_doLet() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Term_doLet___closed__6; +x_1 = l_Lean_Parser_Term_doLet___closed__5; return x_1; } } @@ -36444,7 +36385,7 @@ lean_object* _init_l_Lean_Parser_Term_doId___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_doId___closed__2; @@ -37258,7 +37199,7 @@ lean_object* _init_l_Lean_Parser_Term_doPat___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_leftArrow; @@ -37272,9 +37213,9 @@ lean_object* _init_l_Lean_Parser_Term_doPat___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_doPat___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_doPat___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -37282,7 +37223,7 @@ lean_object* _init_l_Lean_Parser_Term_doPat___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_doPat___closed__2; @@ -37303,7 +37244,7 @@ lean_object* _init_l_Lean_Parser_Term_doPat___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_doPat___closed__4; @@ -37500,7 +37441,7 @@ lean_object* _init_l_Lean_Parser_Term_doExpr___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_doExpr___elambda__1___closed__2; @@ -38505,7 +38446,7 @@ lean_object* _init_l_Lean_Parser_Term_bracketedDoSeq___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_implicitBinder___closed__1; +x_1 = l_Lean_Parser_Term_structInst___closed__1; x_2 = l_Lean_Parser_Term_bracketedDoSeq___closed__1; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; @@ -38729,7 +38670,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj x_1 = l_Lean_Parser_Term_leftArrow; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_3 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_4 = lean_ctor_get(x_3, 0); lean_inc(x_4); x_5 = l_Lean_Parser_andthenInfo(x_2, x_4); @@ -39654,9 +39595,9 @@ lean_object* _init_l_Lean_Parser_Term_nativeRefl___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_nativeRefl___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_nativeRefl___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -40064,9 +40005,9 @@ lean_object* _init_l_Lean_Parser_Term_nativeDecide___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_nativeDecide___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_nativeDecide___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -40474,9 +40415,9 @@ lean_object* _init_l_Lean_Parser_Term_decide___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_decide___elambda__1___closed__6; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_decide___elambda__1___closed__6; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -40885,7 +40826,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_not___elambda__1___closed__6; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -41305,7 +41246,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_bnot___elambda__1___closed__6; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -42597,7 +42538,7 @@ lean_object* _init_l_Lean_Parser_Term_namedArgument___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__1; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; x_2 = l_Lean_Parser_Term_namedArgument___closed__1; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; @@ -42608,7 +42549,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_namedArgument___closed__2; -x_2 = l_Lean_Parser_antiquotNestedExpr___closed__4; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__5; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } @@ -44040,7 +43981,7 @@ lean_object* _init_l_Lean_Parser_Term_dollar___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_Parser_Term_dollar___closed__1; @@ -44906,9 +44847,9 @@ lean_object* _init_l_Lean_Parser_Term_where___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__2; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Tactic_seq___closed__2; +x_2 = l_Lean_Parser_Term_where___closed__1; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } } @@ -44916,55 +44857,45 @@ lean_object* _init_l_Lean_Parser_Term_where___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Tactic_seq___closed__2; +x_1 = l_Lean_nullKind; x_2 = l_Lean_Parser_Term_where___closed__2; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } lean_object* _init_l_Lean_Parser_Term_where___closed__4() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_nullKind; -x_2 = l_Lean_Parser_Term_where___closed__3; -x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); -return x_3; +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Term_letDecl; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Term_where___closed__3; +x_4 = l_Lean_Parser_sepBy1Info(x_2, x_3); +return x_4; } } lean_object* _init_l_Lean_Parser_Term_where___closed__5() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Term_letDecl; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_Term_where___closed__4; -x_4 = l_Lean_Parser_sepBy1Info(x_2, x_3); -return x_4; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_where___closed__1; +x_2 = l_Lean_Parser_Term_where___closed__4; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; } } lean_object* _init_l_Lean_Parser_Term_where___closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_where___closed__1; -x_2 = l_Lean_Parser_Term_where___closed__5; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_where___closed__7() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_where___elambda__1___closed__2; -x_2 = l_Lean_Parser_Term_where___closed__6; +x_2 = l_Lean_Parser_Term_where___closed__5; x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_where___closed__8() { +lean_object* _init_l_Lean_Parser_Term_where___closed__7() { _start: { lean_object* x_1; @@ -44972,12 +44903,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_where___elambda__1), 2, 0); return x_1; } } -lean_object* _init_l_Lean_Parser_Term_where___closed__9() { +lean_object* _init_l_Lean_Parser_Term_where___closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_where___closed__7; -x_2 = l_Lean_Parser_Term_where___closed__8; +x_1 = l_Lean_Parser_Term_where___closed__6; +x_2 = l_Lean_Parser_Term_where___closed__7; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -44988,7 +44919,7 @@ lean_object* _init_l_Lean_Parser_Term_where() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Term_where___closed__9; +x_1 = l_Lean_Parser_Term_where___closed__8; return x_1; } } @@ -47489,46 +47420,36 @@ return x_3; lean_object* _init_l_Lean_Parser_Term_subst___closed__4() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_subst___elambda__1___spec__2___closed__2; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); -return x_3; +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Term_subst___closed__3; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Term_subst___closed__2; +x_4 = l_Lean_Parser_sepBy1Info(x_2, x_3); +return x_4; } } lean_object* _init_l_Lean_Parser_Term_subst___closed__5() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Term_subst___closed__3; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_Term_subst___closed__4; -x_4 = l_Lean_Parser_sepBy1Info(x_2, x_3); -return x_4; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_subst___closed__2; +x_2 = l_Lean_Parser_Term_subst___closed__4; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; } } lean_object* _init_l_Lean_Parser_Term_subst___closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_subst___closed__2; -x_2 = l_Lean_Parser_Term_subst___closed__5; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_subst___closed__7() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_subst___elambda__1___closed__2; -x_2 = l_Lean_Parser_Term_subst___closed__6; +x_2 = l_Lean_Parser_Term_subst___closed__5; x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_subst___closed__8() { +lean_object* _init_l_Lean_Parser_Term_subst___closed__7() { _start: { lean_object* x_1; @@ -47536,12 +47457,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_subst___elambda__1), 2, 0); return x_1; } } -lean_object* _init_l_Lean_Parser_Term_subst___closed__9() { +lean_object* _init_l_Lean_Parser_Term_subst___closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_subst___closed__7; -x_2 = l_Lean_Parser_Term_subst___closed__8; +x_1 = l_Lean_Parser_Term_subst___closed__6; +x_2 = l_Lean_Parser_Term_subst___closed__7; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -47552,7 +47473,7 @@ lean_object* _init_l_Lean_Parser_Term_subst() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Term_subst___closed__9; +x_1 = l_Lean_Parser_Term_subst___closed__8; return x_1; } } @@ -50149,7 +50070,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_tacticBlock___elambda__1___closed__6; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -50158,9 +50079,9 @@ lean_object* _init_l_Lean_Parser_Term_tacticBlock___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_tacticBlock___elambda__1___closed__8; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +x_1 = l_Lean_Parser_Term_tacticBlock___elambda__1___closed__8; +x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } @@ -50889,7 +50810,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__4; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -50899,7 +50820,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Tactic_nonEmptySeq___closed__1; -x_2 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__4; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } @@ -51200,7 +51121,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_levelStxQuot___elambda__1___closed__2; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -51210,7 +51131,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_levelStxQuot___closed__1; -x_2 = l_Lean_Parser_Level_paren___closed__4; +x_2 = l_Lean_Parser_Level_paren___closed__2; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } @@ -51499,7 +51420,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_funBinderStxQuot___elambda__1___closed__2; -x_2 = l_Lean_Parser_Level_paren___closed__1; +x_2 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } @@ -51511,7 +51432,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Term_funBinder; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_antiquotNestedExpr___closed__3; +x_3 = l_Lean_Parser_antiquotNestedExpr___closed__4; x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); return x_4; } @@ -52783,8 +52704,6 @@ l_Lean_Parser_Term_listLit___closed__7 = _init_l_Lean_Parser_Term_listLit___clos lean_mark_persistent(l_Lean_Parser_Term_listLit___closed__7); l_Lean_Parser_Term_listLit___closed__8 = _init_l_Lean_Parser_Term_listLit___closed__8(); lean_mark_persistent(l_Lean_Parser_Term_listLit___closed__8); -l_Lean_Parser_Term_listLit___closed__9 = _init_l_Lean_Parser_Term_listLit___closed__9(); -lean_mark_persistent(l_Lean_Parser_Term_listLit___closed__9); l_Lean_Parser_Term_listLit = _init_l_Lean_Parser_Term_listLit(); lean_mark_persistent(l_Lean_Parser_Term_listLit); res = l___regBuiltinParser_Lean_Parser_Term_listLit(lean_io_mk_world()); @@ -52839,10 +52758,6 @@ l_Lean_Parser_Term_explicit___closed__3 = _init_l_Lean_Parser_Term_explicit___cl lean_mark_persistent(l_Lean_Parser_Term_explicit___closed__3); l_Lean_Parser_Term_explicit___closed__4 = _init_l_Lean_Parser_Term_explicit___closed__4(); lean_mark_persistent(l_Lean_Parser_Term_explicit___closed__4); -l_Lean_Parser_Term_explicit___closed__5 = _init_l_Lean_Parser_Term_explicit___closed__5(); -lean_mark_persistent(l_Lean_Parser_Term_explicit___closed__5); -l_Lean_Parser_Term_explicit___closed__6 = _init_l_Lean_Parser_Term_explicit___closed__6(); -lean_mark_persistent(l_Lean_Parser_Term_explicit___closed__6); l_Lean_Parser_Term_explicit = _init_l_Lean_Parser_Term_explicit(); lean_mark_persistent(l_Lean_Parser_Term_explicit); res = l___regBuiltinParser_Lean_Parser_Term_explicit(lean_io_mk_world()); @@ -52993,8 +52908,6 @@ l_Lean_Parser_Term_implicitBinder___closed__1 = _init_l_Lean_Parser_Term_implici lean_mark_persistent(l_Lean_Parser_Term_implicitBinder___closed__1); l_Lean_Parser_Term_implicitBinder___closed__2 = _init_l_Lean_Parser_Term_implicitBinder___closed__2(); lean_mark_persistent(l_Lean_Parser_Term_implicitBinder___closed__2); -l_Lean_Parser_Term_implicitBinder___closed__3 = _init_l_Lean_Parser_Term_implicitBinder___closed__3(); -lean_mark_persistent(l_Lean_Parser_Term_implicitBinder___closed__3); l_Lean_Parser_Term_instBinder___elambda__1___closed__1 = _init_l_Lean_Parser_Term_instBinder___elambda__1___closed__1(); lean_mark_persistent(l_Lean_Parser_Term_instBinder___elambda__1___closed__1); l_Lean_Parser_Term_instBinder___elambda__1___closed__2 = _init_l_Lean_Parser_Term_instBinder___elambda__1___closed__2(); @@ -53689,8 +53602,6 @@ l_Lean_Parser_Term_doLet___closed__4 = _init_l_Lean_Parser_Term_doLet___closed__ lean_mark_persistent(l_Lean_Parser_Term_doLet___closed__4); l_Lean_Parser_Term_doLet___closed__5 = _init_l_Lean_Parser_Term_doLet___closed__5(); lean_mark_persistent(l_Lean_Parser_Term_doLet___closed__5); -l_Lean_Parser_Term_doLet___closed__6 = _init_l_Lean_Parser_Term_doLet___closed__6(); -lean_mark_persistent(l_Lean_Parser_Term_doLet___closed__6); l_Lean_Parser_Term_doLet = _init_l_Lean_Parser_Term_doLet(); lean_mark_persistent(l_Lean_Parser_Term_doLet); l_Lean_Parser_Term_doId___elambda__1___closed__1 = _init_l_Lean_Parser_Term_doId___elambda__1___closed__1(); @@ -54298,8 +54209,6 @@ l_Lean_Parser_Term_where___closed__7 = _init_l_Lean_Parser_Term_where___closed__ lean_mark_persistent(l_Lean_Parser_Term_where___closed__7); l_Lean_Parser_Term_where___closed__8 = _init_l_Lean_Parser_Term_where___closed__8(); lean_mark_persistent(l_Lean_Parser_Term_where___closed__8); -l_Lean_Parser_Term_where___closed__9 = _init_l_Lean_Parser_Term_where___closed__9(); -lean_mark_persistent(l_Lean_Parser_Term_where___closed__9); l_Lean_Parser_Term_where = _init_l_Lean_Parser_Term_where(); lean_mark_persistent(l_Lean_Parser_Term_where); res = l___regBuiltinParser_Lean_Parser_Term_where(lean_io_mk_world()); @@ -54702,8 +54611,6 @@ l_Lean_Parser_Term_subst___closed__7 = _init_l_Lean_Parser_Term_subst___closed__ lean_mark_persistent(l_Lean_Parser_Term_subst___closed__7); l_Lean_Parser_Term_subst___closed__8 = _init_l_Lean_Parser_Term_subst___closed__8(); lean_mark_persistent(l_Lean_Parser_Term_subst___closed__8); -l_Lean_Parser_Term_subst___closed__9 = _init_l_Lean_Parser_Term_subst___closed__9(); -lean_mark_persistent(l_Lean_Parser_Term_subst___closed__9); l_Lean_Parser_Term_subst = _init_l_Lean_Parser_Term_subst(); lean_mark_persistent(l_Lean_Parser_Term_subst); res = l___regBuiltinParser_Lean_Parser_Term_subst(lean_io_mk_world()); diff --git a/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c b/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c index 88a8ecfc78..48d01b5e71 100644 --- a/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c +++ b/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c @@ -262,8 +262,8 @@ lean_object* lean_nat_sub(lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Parenthesizer_visit___main___closed__6; lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkWsBefore_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_symbolAux_parenthesizer(lean_object*); +extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__1; extern lean_object* l_Lean_choiceKind___closed__2; -extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__2; lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_fieldIdx_parenthesizer___closed__1; lean_object* l_Lean_Syntax_MonadTraverser_getIdx(lean_object*); lean_object* l_Lean_PrettyPrinter_Parenthesizer_numLitNoAntiquot_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*); @@ -388,6 +388,7 @@ lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_numLitNoAntiquot_pa lean_object* l_Lean_Meta_whnf(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_optional_parenthesizer___closed__1; lean_object* l_Lean_PrettyPrinter_Parenthesizer_visit___main___closed__9; +extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__3; uint8_t l_Lean_Elab_Term_Quotation_isAntiquot(lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_many_parenthesizer___closed__1; lean_object* l_Lean_PrettyPrinter_Parenthesizer_ParenthesizerM_monadTraverser___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -638,7 +639,6 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_termParser_parenthesizer___lambd lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_symbolNoWsAux_parenthesizer___closed__3; lean_object* l_Lean_Syntax_MonadTraverser_getCur___at_Lean_PrettyPrinter_Parenthesizer_visitArgs___spec__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Syntax_MonadTraverser_getCur___rarg___lambda__1___boxed(lean_object*); -extern lean_object* l_Lean_Parser_Level_paren___closed__1; lean_object* l_Lean_PrettyPrinter_Parenthesizer_try_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_string_dec_eq(lean_object*, lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); @@ -4013,7 +4013,7 @@ x_26 = lean_ctor_get(x_21, 2); lean_dec(x_26); x_27 = lean_ctor_get(x_21, 1); lean_dec(x_27); -x_28 = l_Lean_Parser_Level_paren___closed__1; +x_28 = l_Lean_Parser_antiquotNestedExpr___closed__1; lean_ctor_set(x_21, 2, x_28); lean_ctor_set(x_21, 1, x_28); x_29 = lean_box(0); @@ -4028,7 +4028,7 @@ x_31 = lean_ctor_get(x_21, 3); lean_inc(x_31); lean_inc(x_30); lean_dec(x_21); -x_32 = l_Lean_Parser_Level_paren___closed__1; +x_32 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_33 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_33, 0, x_30); lean_ctor_set(x_33, 1, x_32); @@ -4060,7 +4060,7 @@ if (lean_is_exclusive(x_21)) { lean_dec_ref(x_21); x_38 = lean_box(0); } -x_39 = l_Lean_Parser_Level_paren___closed__1; +x_39 = l_Lean_Parser_antiquotNestedExpr___closed__1; if (lean_is_scalar(x_38)) { x_40 = lean_alloc_ctor(0, 4, 0); } else { @@ -4109,7 +4109,7 @@ if (lean_is_exclusive(x_43)) { lean_dec_ref(x_43); x_48 = lean_box(0); } -x_49 = l_Lean_Parser_Level_paren___closed__1; +x_49 = l_Lean_Parser_antiquotNestedExpr___closed__1; if (lean_is_scalar(x_48)) { x_50 = lean_alloc_ctor(0, 4, 0); } else { @@ -4921,7 +4921,7 @@ x_87 = lean_ctor_get(x_82, 2); lean_dec(x_87); x_88 = lean_ctor_get(x_82, 1); lean_dec(x_88); -x_89 = l_Lean_Parser_Level_paren___closed__1; +x_89 = l_Lean_Parser_antiquotNestedExpr___closed__1; lean_ctor_set(x_82, 3, x_43); lean_ctor_set(x_82, 2, x_89); lean_ctor_set(x_82, 1, x_89); @@ -4937,7 +4937,7 @@ lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; x_91 = lean_ctor_get(x_82, 0); lean_inc(x_91); lean_dec(x_82); -x_92 = l_Lean_Parser_Level_paren___closed__1; +x_92 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_93 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_93, 0, x_91); lean_ctor_set(x_93, 1, x_92); @@ -4972,7 +4972,7 @@ if (lean_is_exclusive(x_95)) { lean_dec_ref(x_95); x_98 = lean_box(0); } -x_99 = l_Lean_Parser_Level_paren___closed__1; +x_99 = l_Lean_Parser_antiquotNestedExpr___closed__1; if (lean_is_scalar(x_98)) { x_100 = lean_alloc_ctor(0, 4, 0); } else { @@ -5041,7 +5041,7 @@ x_123 = lean_ctor_get(x_118, 2); lean_dec(x_123); x_124 = lean_ctor_get(x_118, 1); lean_dec(x_124); -x_125 = l_Lean_Parser_Level_paren___closed__1; +x_125 = l_Lean_Parser_antiquotNestedExpr___closed__1; lean_ctor_set(x_118, 3, x_43); lean_ctor_set(x_118, 2, x_125); lean_ctor_set(x_118, 1, x_125); @@ -5057,7 +5057,7 @@ lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; x_127 = lean_ctor_get(x_118, 0); lean_inc(x_127); lean_dec(x_118); -x_128 = l_Lean_Parser_Level_paren___closed__1; +x_128 = l_Lean_Parser_antiquotNestedExpr___closed__1; x_129 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_129, 0, x_127); lean_ctor_set(x_129, 1, x_128); @@ -5092,7 +5092,7 @@ if (lean_is_exclusive(x_131)) { lean_dec_ref(x_131); x_134 = lean_box(0); } -x_135 = l_Lean_Parser_Level_paren___closed__1; +x_135 = l_Lean_Parser_antiquotNestedExpr___closed__1; if (lean_is_scalar(x_134)) { x_136 = lean_alloc_ctor(0, 4, 0); } else { @@ -5198,7 +5198,7 @@ if (lean_is_exclusive(x_157)) { lean_dec_ref(x_157); x_161 = lean_box(0); } -x_162 = l_Lean_Parser_Level_paren___closed__1; +x_162 = l_Lean_Parser_antiquotNestedExpr___closed__1; if (lean_is_scalar(x_161)) { x_163 = lean_alloc_ctor(0, 4, 0); } else { @@ -5275,7 +5275,7 @@ if (lean_is_exclusive(x_180)) { lean_dec_ref(x_180); x_184 = lean_box(0); } -x_185 = l_Lean_Parser_Level_paren___closed__1; +x_185 = l_Lean_Parser_antiquotNestedExpr___closed__1; if (lean_is_scalar(x_184)) { x_186 = lean_alloc_ctor(0, 4, 0); } else { @@ -12600,7 +12600,7 @@ lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___closed__2() _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); x_3 = l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___closed__1;