max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-05-27 16:15:19 -07:00
parent dbe4aa447e
commit bbdf1f39ed
17 changed files with 793 additions and 876 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
stage0/src/Init/LeanInit.lean
View file

@ -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 -/

1
stage0/src/Lean/Elab/Syntax.lean
View file

@ -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

16
stage0/src/Lean/Parser/Command.lean
View file

@ -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)

8
stage0/src/Lean/Parser/Parser.lean
View file

@ -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

12
stage0/src/Lean/Parser/Syntax.lean
View file

@ -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

10
stage0/src/Lean/Parser/Tactic.lean
View file

@ -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

22
stage0/src/Lean/Parser/Term.lean
View file

@ -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

8
stage0/stdlib/Init/LeanInit.c
View file

@ -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;
}
}

4
stage0/stdlib/Lean/Elab/Syntax.c
View file

@ -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

316
stage0/stdlib/Lean/Parser/Command.c
View file

@ -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();

62
stage0/stdlib/Lean/Parser/Level.c
View file

@ -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());

19
stage0/stdlib/Lean/Parser/Module.c
View file

@ -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;
}
}

210
stage0/stdlib/Lean/Parser/Parser.c
View file

@ -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();

181
stage0/stdlib/Lean/Parser/Syntax.c
View file

@ -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();

191
stage0/stdlib/Lean/Parser/Tactic.c
View file

@ -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());

575
stage0/stdlib/Lean/Parser/Term.c
View file

File diff suppressed because it is too large Load diff

30
stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c
View file

@ -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;