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-01-30 20:57:42 -08:00
parent 21618361b7
commit 2f74415eaf
25 changed files with 43832 additions and 49230 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Init/Lean/Elab/Quotation.lean
View file

@ -426,7 +426,7 @@ def oldParseExpr (env : Environment) (input : String) (pos : String.Pos) : Excep
let c := Parser.mkParserContext env (Parser.mkInputContext input "<foo>");
let s := Parser.mkParserState c.input;
let s := s.setPos pos;
let s := (Parser.termParser Parser.appPrec : Parser.Parser).fn Parser.appPrec c s;
let s := (Parser.termParser Parser.appPrec : Parser.Parser).fn { rbp := Parser.appPrec, .. c } s;
let stx := s.stxStack.back;
match s.errorMsg with
| some errorMsg =>

4
stage0/src/Init/Lean/Parser/Command.lean
View file

@ -15,7 +15,7 @@ registerBuiltinParserAttribute `builtinCommandParser `command
@[init] def regCommandParserAttribute : IO Unit :=
registerBuiltinDynamicParserAttribute `commandParser `command
@[inline] def commandParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
@[inline] def commandParser (rbp : Nat := 0) : Parser :=
categoryParser `command rbp
/--
@ -28,7 +28,7 @@ categoryParser `command rbp
namespace Command
def commentBody : Parser :=
{ fn := rawFn (fun _ => finishCommentBlock 1) true }
{ fn := rawFn (finishCommentBlock 1) true }
def docComment := parser! "/--" >> commentBody
def attrArg : Parser := ident <|> strLit <|> numLit

2
stage0/src/Init/Lean/Parser/Level.lean
View file

@ -12,7 +12,7 @@ namespace Parser
@[init] def regBuiltinLevelParserAttr : IO Unit :=
registerBuiltinParserAttribute `builtinLevelParser `level
@[inline] def levelParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
@[inline] def levelParser (rbp : Nat := 0) : Parser :=
categoryParser `level rbp
namespace Level

4
stage0/src/Init/Lean/Parser/Module.lean
View file

@ -39,7 +39,7 @@ let ctx := mkParserContext env inputCtx;
let ctx := Module.updateTokens ctx;
let s := mkParserState ctx.input;
let s := whitespace ctx s;
let s := Module.header.fn (0:Nat) ctx s;
let s := Module.header.fn ctx s;
let stx := s.stxStack.back;
match s.errorMsg with
| some errorMsg =>
@ -73,7 +73,7 @@ partial def parseCommand (env : Environment) (inputCtx : InputContext) : ModuleP
let c := mkParserContext env inputCtx;
let s := { ParserState . cache := initCacheForInput c.input, pos := pos };
let s := whitespace c s;
let s := (commandParser : Parser).fn (0:Nat) c s;
let s := (commandParser : Parser).fn c s;
match s.errorMsg with
| none =>
let stx := s.stxStack.back;

621
stage0/src/Init/Lean/Parser/Parser.lean
View file

File diff suppressed because it is too large Load diff

2
stage0/src/Init/Lean/Parser/Syntax.lean
View file

@ -14,7 +14,7 @@ namespace Parser
let leadingIdentAsSymbol := true;
registerBuiltinParserAttribute `builtinSyntaxParser `syntax leadingIdentAsSymbol
@[inline] def syntaxParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
@[inline] def syntaxParser (rbp : Nat := 0) : Parser :=
categoryParser `syntax rbp
def maxPrec := parser! nonReservedSymbol "max" true

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

@ -16,19 +16,19 @@ registerBuiltinParserAttribute `builtinTacticParser `tactic leadingIdentAsSymbol
@[init] def regTacticParserAttribute : IO Unit :=
registerBuiltinDynamicParserAttribute `tacticParser `tactic
@[inline] def tacticParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
@[inline] def tacticParser (rbp : Nat := 0) : Parser :=
categoryParser `tactic rbp
namespace Tactic
def underscoreFn {k : ParserKind} : ParserFn k :=
fun a c s =>
let s := symbolFn "_" a c s;
def underscoreFn : ParserFn :=
fun c s =>
let s := symbolFn "_" c s;
let stx := s.stxStack.back;
let s := s.popSyntax;
s.pushSyntax $ mkIdentFrom stx `_
@[inline] def underscore {k : ParserKind} : Parser k :=
@[inline] def underscore : Parser :=
{ fn := underscoreFn,
info := mkAtomicInfo "ident" }

6
stage0/src/Init/Lean/Parser/Term.lean
View file

@ -122,9 +122,9 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}"
@[builtinTermParser] def uminus := parser! "-" >> termParser 100
def namedArgument := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
@[builtinTermParser] def app := tparser! many1 ((toTrailing namedArgument) <|> termParser appPrec)
@[builtinTermParser] def app := tparser! many1 (namedArgument <|> termParser appPrec)
def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Term.type || leading.isOfKind `Lean.Parser.Term.sort)
def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type || stx.isOfKind `Lean.Parser.Term.sort)
@[builtinTermParser] def sortApp := tparser! checkIsSort >> levelParser appPrec
@[builtinTermParser] def proj := tparser! symbolNoWs "." (appPrec+1) >> (fieldIdx <|> ident)
@[builtinTermParser] def arrow := tparser! unicodeInfixR " → " " -> " 25
@ -133,7 +133,7 @@ def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Te
@[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 (toTrailing letDecl) (group ("; " >> " where "))
@[builtinTermParser] def «where» := tparser! symbol " where " 1 >> sepBy1 letDecl (group ("; " >> " where "))
@[builtinTermParser] def fcomp := tparser! infixR " ∘ " 90

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

@ -132,57 +132,32 @@ mkNameNum g.namePrefix g.idx
end NameGenerator
inductive ParserKind
| leading | trailing
/-
Small DSL for describing parsers. We implement an interpreter for it
at `Parser.lean` -/
inductive ParserDescrCore : ParserKind → Type
| andthen {k : ParserKind} : ParserDescrCore k → ParserDescrCore k → ParserDescrCore k
| orelse {k : ParserKind} : ParserDescrCore k → ParserDescrCore k → ParserDescrCore k
| optional {k : ParserKind} : ParserDescrCore k → ParserDescrCore k
| lookahead {k : ParserKind} : ParserDescrCore k → ParserDescrCore k
| try {k : ParserKind} : ParserDescrCore k → ParserDescrCore k
| many {k : ParserKind} : ParserDescrCore k → ParserDescrCore k
| many1 {k : ParserKind} : ParserDescrCore k → ParserDescrCore k
| sepBy {k : ParserKind} : ParserDescrCore k → ParserDescrCore k → ParserDescrCore k
| sepBy1 {k : ParserKind} : ParserDescrCore k → ParserDescrCore k → ParserDescrCore k
| node {k : ParserKind} : Name → ParserDescrCore k → ParserDescrCore k
| trailingNode : Name → ParserDescrCore ParserKind.trailing → ParserDescrCore ParserKind.trailing
| symbol {k : ParserKind} : String → Option Nat → ParserDescrCore k
| nonReservedSymbol : String → Bool → ParserDescrCore ParserKind.leading
| numLit {k : ParserKind} : ParserDescrCore k
| strLit {k : ParserKind} : ParserDescrCore k
| charLit {k : ParserKind} : ParserDescrCore k
| nameLit {k : ParserKind} : ParserDescrCore k
| ident {k : ParserKind} : ParserDescrCore k
| parser {k : ParserKind} : Name → Nat → ParserDescrCore k
inductive ParserDescr
| andthen : ParserDescr → ParserDescr → ParserDescr
| orelse : ParserDescr → ParserDescr → ParserDescr
| optional : ParserDescr → ParserDescr
| lookahead : ParserDescr → ParserDescr
| try : ParserDescr → ParserDescr
| many : ParserDescr → ParserDescr
| many1 : ParserDescr → ParserDescr
| sepBy : ParserDescr → ParserDescr → ParserDescr
| sepBy1 : ParserDescr → ParserDescr → ParserDescr
| node : Name → ParserDescr → ParserDescr
| trailingNode : Name → ParserDescr → ParserDescr
| symbol : String → Option Nat → ParserDescr
| nonReservedSymbol : String → Bool → ParserDescr
| numLit : ParserDescr
| strLit : ParserDescr
| charLit : ParserDescr
| nameLit : ParserDescr
| ident : ParserDescr
| parser : Name → Nat → ParserDescr
instance ParserDescrCore.inhabited {k} : Inhabited (ParserDescrCore k) := ⟨ParserDescrCore.symbol "" none⟩
abbrev ParserDescr := ParserDescrCore ParserKind.leading
abbrev TrailingParserDescr := ParserDescrCore ParserKind.trailing
@[matchPattern] abbrev ParserDescr.andthen := @ParserDescrCore.andthen
@[matchPattern] abbrev ParserDescr.orelse := @ParserDescrCore.orelse
@[matchPattern] abbrev ParserDescr.optional := @ParserDescrCore.optional
@[matchPattern] abbrev ParserDescr.lookahead := @ParserDescrCore.lookahead
@[matchPattern] abbrev ParserDescr.try := @ParserDescrCore.try
@[matchPattern] abbrev ParserDescr.many := @ParserDescrCore.many
@[matchPattern] abbrev ParserDescr.many1 := @ParserDescrCore.many1
@[matchPattern] abbrev ParserDescr.sepBy := @ParserDescrCore.sepBy
@[matchPattern] abbrev ParserDescr.sepBy1 := @ParserDescrCore.sepBy1
@[matchPattern] abbrev ParserDescr.node := @ParserDescrCore.node
@[matchPattern] abbrev ParserDescr.trailingNode := @ParserDescrCore.trailingNode
@[matchPattern] abbrev ParserDescr.symbol := @ParserDescrCore.symbol
@[matchPattern] abbrev ParserDescr.numLit := @ParserDescrCore.numLit
@[matchPattern] abbrev ParserDescr.strLit := @ParserDescrCore.strLit
@[matchPattern] abbrev ParserDescr.charLit := @ParserDescrCore.charLit
@[matchPattern] abbrev ParserDescr.nameLit := @ParserDescrCore.nameLit
@[matchPattern] abbrev ParserDescr.ident := @ParserDescrCore.ident
@[matchPattern] abbrev ParserDescr.nonReservedSymbol := @ParserDescrCore.nonReservedSymbol
@[matchPattern] abbrev ParserDescr.parser := @ParserDescrCore.parser
instance ParserDescr.inhabited : Inhabited ParserDescr := ⟨ParserDescr.symbol "" none⟩
abbrev TrailingParserDescr := ParserDescr
/- Syntax -/

6
stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
View file

@ -84,7 +84,6 @@ lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabModN___closed__1;
extern lean_object* l_Lean_Parser_Term_show___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_elabMul___closed__2;
extern lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__2;
extern lean_object* l_Array_empty___closed__1;
lean_object* l_Lean_Elab_Term_elabPow___closed__3;
lean_object* lean_environment_find(lean_object*, lean_object*);
@ -526,6 +525,7 @@ lean_object* l_Lean_Elab_Term_elabProd(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabSub___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__2;
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__24;
extern lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__2;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabDiv(lean_object*);
lean_object* l_Lean_Elab_Term_elabNe___closed__1;
lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__4;
@ -1024,7 +1024,7 @@ lean_object* l_Lean_Elab_Term_expandDollar(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_46; uint8_t x_47;
x_46 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__2;
x_46 = l_Lean_Parser_Term_dollar___elambda__1___closed__2;
lean_inc(x_1);
x_47 = l_Lean_Syntax_isOfKind(x_1, x_46);
if (x_47 == 0)
@ -1166,7 +1166,7 @@ lean_object* l___regBuiltinMacro_Lean_Elab_Term_expandDollar(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__2;
x_2 = l_Lean_Parser_Term_dollar___elambda__1___closed__2;
x_3 = l___regBuiltinMacro_Lean_Elab_Term_expandDollar___closed__1;
x_4 = l_Lean_Elab_addBuiltinMacro(x_2, x_3, x_1);
return x_4;

6
stage0/stdlib/Init/Lean/Elab/Level.c
View file

@ -30,6 +30,7 @@ lean_object* l_Lean_Syntax_getIdAt(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_LevelElabM_MonadLog___lambda__3(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Level_max___elambda__1___closed__1;
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(lean_object*);
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l___private_Init_Data_Array_Basic_4__foldrRangeMAux___main___at_Lean_Elab_Level_elabLevel___main___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_elabLevel(lean_object*, lean_object*, lean_object*);
@ -95,7 +96,6 @@ lean_object* l_Lean_Elab_Level_LevelElabM_MonadLog___lambda__2___boxed(lean_obje
lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Level_elabLevel___main___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_elabLevel___main___closed__4;
lean_object* l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(lean_object*);
lean_object* l_Lean_Elab_getPos___at_Lean_Elab_Level_elabLevel___main___spec__3___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_elabLevel___main___closed__2;
lean_object* l_Lean_Elab_Level_elabLevel___main___closed__8;
@ -1264,7 +1264,7 @@ x_75 = l_Lean_Syntax_getArg(x_1, x_74);
lean_dec(x_1);
x_76 = l_Lean_Syntax_getArgs(x_75);
lean_dec(x_75);
x_77 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_76);
x_77 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_76);
x_78 = l_Lean_Elab_Level_elabLevel___main(x_77, x_2, x_3);
if (lean_obj_tag(x_78) == 0)
{
@ -1330,7 +1330,7 @@ x_93 = l_Lean_Syntax_getArg(x_1, x_92);
lean_dec(x_1);
x_94 = l_Lean_Syntax_getArgs(x_93);
lean_dec(x_93);
x_95 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_94);
x_95 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_94);
x_96 = l_Lean_Elab_Level_elabLevel___main(x_95, x_2, x_3);
if (lean_obj_tag(x_96) == 0)
{

75
stage0/stdlib/Init/Lean/Elab/Quotation.c
View file

@ -40,7 +40,6 @@ extern lean_object* l___private_Init_Lean_Compiler_InitAttr_2__isUnitType___clos
lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__41;
lean_object* l___private_Init_Lean_Elab_Quotation_13__toPreterm(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__13;
lean_object* l_Lean_Parser_mkParserContext(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__8;
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_2__quoteList___main___at___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___spec__2(lean_object*);
@ -139,6 +138,7 @@ extern lean_object* l_Lean_Parser_Term_num___elambda__1___closed__1;
lean_object* l_List_range(lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_8__explodeHeadPat___lambda__1___closed__2;
lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__12;
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l___private_Init_Lean_Elab_Quotation_12__exprPlaceholder;
@ -267,7 +267,6 @@ extern lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__1;
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_Quotation_match__syntax_expand___spec__1___closed__4;
lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__52;
lean_object* l___private_Init_Lean_Elab_Quotation_14__oldRunTermElabM(lean_object*);
extern lean_object* l_Lean_Parser_darrow___elambda__1___rarg___closed__3;
lean_object* l_List_filterAux___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__6(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Unhygienic_run___rarg(lean_object*);
@ -316,6 +315,7 @@ extern lean_object* l_Lean_Parser_termParser___closed__2;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_choiceKind;
lean_object* l___private_Init_Lean_Elab_Quotation_13__toPreterm___main___closed__2;
extern lean_object* l_Lean_Parser_darrow___elambda__1___closed__3;
lean_object* l_Lean_Elab_Term_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__28;
extern lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__2;
@ -361,6 +361,7 @@ extern lean_object* l_Lean_Parser_Term_let___elambda__1___closed__2;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_Quotation_elabMatchSyntax(lean_object*);
lean_object* l_List_redLength___main___rarg(lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_11__letBindRhss___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_getTokenTable(lean_object*);
lean_object* l_Lean_List_hasQuote(lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -381,7 +382,6 @@ extern lean_object* l_Lean_Elab_Term_elabListLit___closed__5;
extern lean_object* l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__1;
lean_object* l_Lean_Option_hasQuote(lean_object*);
uint8_t l_Lean_Syntax_isAtom(lean_object*);
lean_object* l_Lean_Parser_categoryParserFn(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_nullKind___closed__2;
extern lean_object* l_Lean_Parser_Term_if___elambda__1___closed__1;
lean_object* l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__3___boxed(lean_object*, lean_object*);
@ -458,6 +458,7 @@ lean_object* l_Lean_Elab_Term_Quotation_oldParseExpr___closed__1;
lean_object* l_Lean_LocalContext_mkLambda(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__25;
extern lean_object* l_Lean_mkHole___closed__1;
lean_object* l_Lean_Parser_categoryParser___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__40;
lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_adaptExpander(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -595,7 +596,6 @@ lean_object* l_Lean_Elab_Term_Quotation_getAntiquotTerm___boxed(lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__3___closed__1;
extern lean_object* l_Lean_mkAppStx___closed__1;
uint8_t l_Lean_Elab_Term_Quotation_HeadInfo_generalizes(lean_object*, lean_object*);
lean_object* l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand(lean_object*, lean_object*, lean_object*);
lean_object* l_List_zipWith___main___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__8;
@ -11575,7 +11575,7 @@ lean_object* _init_l___private_Init_Lean_Elab_Quotation_11__letBindRhss___main__
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_darrow___elambda__1___rarg___closed__3;
x_1 = l_Lean_Parser_darrow___elambda__1___closed__3;
x_2 = l_Lean_mkAtom(x_1);
return x_2;
}
@ -25019,47 +25019,52 @@ return x_1;
lean_object* lean_parse_expr(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_4 = l_Lean_Elab_Term_Quotation_oldParseExpr___closed__1;
lean_inc(x_2);
x_5 = l_Lean_Parser_mkInputContext(x_2, x_4);
x_6 = l_Lean_Parser_mkParserContext(x_1, x_5);
x_7 = l_Lean_Parser_mkParserState(x_2);
x_6 = l_Lean_Parser_mkParserState(x_2);
lean_dec(x_2);
x_8 = l_Lean_Parser_ParserState_setPos(x_7, x_3);
x_9 = l_Lean_Parser_termParser___closed__2;
x_10 = l_Lean_Parser_appPrec;
x_11 = l_Lean_Parser_categoryParserFn(x_9, x_10, x_6, x_8);
x_12 = lean_ctor_get(x_11, 3);
lean_inc(x_12);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_13 = lean_ctor_get(x_11, 0);
x_7 = l_Lean_Parser_ParserState_setPos(x_6, x_3);
x_8 = l_Lean_Parser_getTokenTable(x_1);
x_9 = l_Lean_Parser_appPrec;
x_10 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_10, 0, x_5);
lean_ctor_set(x_10, 1, x_9);
lean_ctor_set(x_10, 2, x_1);
lean_ctor_set(x_10, 3, x_8);
x_11 = l_Lean_Parser_termParser___closed__2;
x_12 = l_Lean_Parser_categoryParser___elambda__1(x_11, x_9, x_10, x_7);
x_13 = lean_ctor_get(x_12, 3);
lean_inc(x_13);
x_14 = lean_ctor_get(x_11, 1);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_14 = lean_ctor_get(x_12, 0);
lean_inc(x_14);
lean_dec(x_11);
x_15 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_13);
lean_dec(x_13);
x_16 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_16, 0, x_15);
lean_ctor_set(x_16, 1, x_14);
x_17 = lean_alloc_ctor(1, 1, 0);
x_15 = lean_ctor_get(x_12, 1);
lean_inc(x_15);
lean_dec(x_12);
x_16 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_14);
lean_dec(x_14);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
return x_17;
lean_ctor_set(x_17, 1, x_15);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_17);
return x_18;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_dec(x_11);
x_18 = lean_ctor_get(x_12, 0);
lean_inc(x_18);
lean_object* x_19; lean_object* x_20; lean_object* x_21;
lean_dec(x_12);
x_19 = l_Lean_Parser_Error_toString(x_18);
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_19);
return x_20;
x_19 = lean_ctor_get(x_13, 0);
lean_inc(x_19);
lean_dec(x_13);
x_20 = l_Lean_Parser_Error_toString(x_19);
x_21 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_21, 0, x_20);
return x_21;
}
}
}

48
stage0/stdlib/Init/Lean/Elab/Syntax.c
View file

@ -17,6 +17,7 @@ lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__45;
lean_object* l_Lean_Elab_Command_elabSyntax___closed__11;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__34;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__95;
extern lean_object* l_Lean_Parser_Syntax_many___elambda__1___closed__1;
lean_object* l_Lean_Elab_Term_getEnv___rarg(lean_object*);
extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__mkParserSeq___spec__1___closed__2;
@ -35,6 +36,7 @@ lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__12;
lean_object* l_Lean_Name_eraseMacroScopes(lean_object*);
lean_object* l_Lean_Syntax_isNatLitAux(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_expandNotation___closed__2;
extern lean_object* l_Lean_Parser_Syntax_many___elambda__1___closed__2;
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Command_expandNotation___spec__4(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_getOptions(lean_object*, lean_object*);
extern lean_object* l_Lean_Macro_throwUnsupported___closed__1;
@ -47,6 +49,7 @@ lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__75;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__15;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabReserve(lean_object*);
extern lean_object* l_Lean_Parser_Syntax_try___elambda__1___closed__1;
extern lean_object* l_Lean_Parser_Syntax_many1___elambda__1___closed__1;
lean_object* l___private_Init_Lean_Elab_Syntax_1__expandOptPrecedence(lean_object*);
extern lean_object* l_Lean_Elab_Term_elabArrayLit___closed__13;
lean_object* l_Lean_Elab_Command_elabSyntax___closed__36;
@ -72,16 +75,15 @@ extern lean_object* l___private_Init_Lean_Elab_TermBinders_10__expandFunBindersA
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__5;
extern lean_object* l_Lean_Elab_registerBuiltinMacroAttr___lambda__1___closed__5;
uint8_t lean_name_eq(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Syntax_many1___elambda__1___closed__2;
lean_object* l_Lean_Elab_Command_Macro_mkFreshKind(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__104;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabReserve___closed__1;
lean_object* l_Lean_Syntax_getIdAt(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
extern lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__3;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__33;
lean_object* lean_array_fswap(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_identKind___closed__2;
extern lean_object* l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__1;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__13;
extern lean_object* l_Lean_Elab_Command_runTermElabM___rarg___closed__1;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__23;
@ -89,8 +91,10 @@ lean_object* l_Lean_Elab_Command_elabSyntax___closed__7;
lean_object* l_Lean_Elab_Command_expandMacroArgIntoPattern(lean_object*, lean_object*);
extern lean_object* l_PersistentHashMap_mkCollisionNode___rarg___closed__1;
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_Syntax_7__antiquote___main___spec__5(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Syntax_orelse___elambda__1___closed__1;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__101;
extern lean_object* l_Array_empty___closed__1;
extern lean_object* l_Lean_Parser_unquotedSymbolFn___closed__1;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__46;
lean_object* l_Array_mapSepElemsM___at_Lean_Elab_Command_elabMacroRulesAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabReserve___closed__2;
@ -125,7 +129,6 @@ lean_object* l___private_Init_Lean_Elab_Syntax_8__regTraceClasses(lean_object*);
lean_object* l_Lean_Elab_Command_elabSyntax___closed__20;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__9;
extern lean_object* l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
lean_object* l_Lean_Elab_Term_toParserDescrAux(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__81;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__6;
@ -242,6 +245,7 @@ extern lean_object* l_Lean_strLitKind___closed__1;
extern lean_object* l___private_Init_Lean_Elab_TermBinders_10__expandFunBindersAux___main___closed__6;
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__32;
extern lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__1;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__10;
extern lean_object* l_Lean_Elab_Term_mkConst___closed__4;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__1;
@ -250,7 +254,6 @@ extern lean_object* l_Lean_Unhygienic_MonadQuotation___closed__4;
lean_object* l___private_Init_LeanInit_14__filterSepElemsMAux___main___at_Lean_Elab_Command_elabNoKindMacroRulesAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinMacro_Lean_Elab_Command_expandNotation___closed__1;
lean_object* l_Lean_Elab_Command_elabSyntax___closed__29;
extern lean_object* l_Lean_Parser_unquotedSymbolFn___rarg___closed__1;
lean_object* l_Array_filterAux___main___at_Lean_Elab_Command_expandNotation___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__20;
extern lean_object* l_Lean_Parser_mkParserOfConstantUnsafe___closed__4;
@ -259,7 +262,6 @@ lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__56;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__66;
lean_object* l_Nat_repr(lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Quotation_11__letBindRhss___main___closed__11;
extern lean_object* l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
extern lean_object* l_Lean_Parser_Command_attrInstance___elambda__1___closed__2;
extern lean_object* l_Lean_Elab_Term_expandCDot_x3f___closed__3;
lean_object* l_Lean_Elab_Command_elabMacroRules(lean_object*, lean_object*, lean_object*);
@ -268,7 +270,6 @@ lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__37;
lean_object* l_Lean_Elab_Command_elabNoKindMacroRulesAux___closed__4;
lean_object* l___private_Init_Lean_Elab_Command_1__ioErrorToMessage(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getId(lean_object*);
extern lean_object* l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__1;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__7;
lean_object* l_Lean_Elab_Command_adaptExpander(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabSyntax___closed__33;
@ -406,12 +407,11 @@ lean_object* l_Lean_Elab_Command_getMainModule(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Syntax_3__markAsTrailingParser___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__31;
extern lean_object* l_Lean_Elab_Term_elabArrayLit___closed__12;
extern lean_object* l_Lean_Parser_mkAntiquotAux___closed__1;
extern lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__2;
lean_object* l_Lean_Elab_Command_elabSyntax___closed__8;
lean_object* l_Lean_Elab_Command_elabNoKindMacroRulesAux___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__7;
extern lean_object* l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
lean_object* l_Lean_Syntax_getArgs(lean_object*);
lean_object* l_Lean_Elab_Term_checkLeftRec___closed__3;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabReserve___closed__3;
@ -550,7 +550,6 @@ extern lean_object* l_Lean_mkAppStx___closed__2;
extern lean_object* l_Lean_Parser_mkParserOfConstantUnsafe___closed__3;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__23;
extern lean_object* l_Lean_Elab_mkMacroAttribute___closed__1;
extern lean_object* l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__1;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__2;
lean_object* l___private_Init_Lean_Elab_Syntax_4__withNotFirst___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Quotation_3__quoteOption___rarg___closed__6;
@ -583,6 +582,7 @@ lean_object* l_Lean_Elab_Command_expandNotationItemIntoSyntaxItem___boxed(lean_o
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__59;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__82;
extern lean_object* l_Lean_Parser_Command_declId___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_mkAntiquot___closed__1;
lean_object* l_Lean_Elab_Command_logTrace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Syntax_1__expandOptPrecedence(lean_object* x_1) {
_start:
@ -1594,7 +1594,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__mkParserSeq___spec__1___closed__4;
x_2 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__1;
x_2 = l_Lean_Parser_Syntax_optional___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -1604,7 +1604,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__mkParserSeq___spec__1___closed__6;
x_2 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__1;
x_2 = l_Lean_Parser_Syntax_optional___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -1669,7 +1669,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__mkParserSeq___spec__1___closed__4;
x_2 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__1;
x_2 = l_Lean_Parser_Syntax_many1___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -1679,7 +1679,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__mkParserSeq___spec__1___closed__6;
x_2 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__1;
x_2 = l_Lean_Parser_Syntax_many1___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -1744,7 +1744,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__mkParserSeq___spec__1___closed__4;
x_2 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__1;
x_2 = l_Lean_Parser_Syntax_many___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -1754,7 +1754,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__mkParserSeq___spec__1___closed__6;
x_2 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__1;
x_2 = l_Lean_Parser_Syntax_many___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -2419,7 +2419,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__mkParserSeq___spec__1___closed__4;
x_2 = l_Lean_Parser_unquotedSymbolFn___rarg___closed__1;
x_2 = l_Lean_Parser_unquotedSymbolFn___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -2429,7 +2429,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__mkParserSeq___spec__1___closed__6;
x_2 = l_Lean_Parser_unquotedSymbolFn___rarg___closed__1;
x_2 = l_Lean_Parser_unquotedSymbolFn___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -2810,22 +2810,22 @@ x_32 = lean_name_eq(x_6, x_31);
if (x_32 == 0)
{
lean_object* x_33; uint8_t x_34;
x_33 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
x_33 = l_Lean_Parser_Syntax_many___elambda__1___closed__2;
x_34 = lean_name_eq(x_6, x_33);
if (x_34 == 0)
{
lean_object* x_35; uint8_t x_36;
x_35 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
x_35 = l_Lean_Parser_Syntax_many1___elambda__1___closed__2;
x_36 = lean_name_eq(x_6, x_35);
if (x_36 == 0)
{
lean_object* x_37; uint8_t x_38;
x_37 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
x_37 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
x_38 = lean_name_eq(x_6, x_37);
if (x_38 == 0)
{
lean_object* x_39; uint8_t x_40;
x_39 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
x_39 = l_Lean_Parser_Syntax_orelse___elambda__1___closed__1;
x_40 = lean_name_eq(x_6, x_39);
if (x_40 == 0)
{
@ -12763,7 +12763,7 @@ x_36 = lean_array_push(x_35, x_34);
x_37 = l_Lean_mkOptionalNode___closed__1;
x_38 = lean_array_push(x_36, x_37);
x_39 = lean_array_push(x_38, x_37);
x_40 = l_Lean_Parser_mkAntiquotAux___closed__1;
x_40 = l_Lean_Parser_mkAntiquot___closed__1;
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_40);
lean_ctor_set(x_41, 1, x_39);
@ -13101,7 +13101,7 @@ x_21 = lean_array_push(x_20, x_19);
x_22 = l_Lean_mkOptionalNode___closed__1;
x_23 = lean_array_push(x_21, x_22);
x_24 = lean_array_push(x_23, x_22);
x_25 = l_Lean_Parser_mkAntiquotAux___closed__1;
x_25 = l_Lean_Parser_mkAntiquot___closed__1;
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_24);
@ -14065,7 +14065,7 @@ x_14 = lean_array_push(x_13, x_12);
x_15 = l_Lean_mkOptionalNode___closed__1;
x_16 = lean_array_push(x_14, x_15);
x_17 = lean_array_push(x_16, x_15);
x_18 = l_Lean_Parser_mkAntiquotAux___closed__1;
x_18 = l_Lean_Parser_mkAntiquot___closed__1;
x_19 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set(x_19, 1, x_17);

6
stage0/stdlib/Init/Lean/Elab/Tactic/Basic.c
View file

@ -217,7 +217,6 @@ lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalTraceState___closed__3;
lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalCase___closed__3;
extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__7;
extern lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Tactic_evalTactic___main___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_monadLog___closed__8;
extern lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__2;
@ -328,6 +327,7 @@ uint8_t l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_isValidSyntaxN
lean_object* l_Lean_Elab_Tactic_addBuiltinTactic(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_modifyMCtx(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_tagUntaggedGoals(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
lean_object* l_Lean_Elab_Tactic_getOptions___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_declareBuiltinTactic___closed__2;
lean_object* l_Lean_Elab_Tactic_withMVarContext___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -14896,7 +14896,7 @@ lean_object* l_Lean_Elab_Tactic_evalOrelse(lean_object* x_1, lean_object* x_2, l
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
x_4 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
lean_inc(x_1);
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
@ -15021,7 +15021,7 @@ lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalOrelse(lean_object* x_1)
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
x_2 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
x_3 = l___regBuiltinTactic_Lean_Elab_Tactic_evalOrelse___closed__2;
x_4 = l___regBuiltinTactic_Lean_Elab_Tactic_evalOrelse___closed__3;
x_5 = l_Lean_Elab_Tactic_addBuiltinTactic(x_2, x_3, x_4, x_1);

8
stage0/stdlib/Init/Lean/Elab/Term.c
View file

@ -169,6 +169,7 @@ lean_object* l_Lean_Elab_Term_elabBadCDot___boxed(lean_object*, lean_object*, le
extern lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__2;
lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
lean_object* l_PersistentArray_push___rarg(lean_object*, lean_object*);
lean_object* l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabTypeStx___closed__2;
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l_Lean_Elab_Term_logTrace___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -331,7 +332,6 @@ lean_object* l___private_Init_Lean_Elab_Term_6__exceptionToSorry___closed__1;
lean_object* l_Lean_Elab_Term_TermElabM_inhabited(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkInstMVar(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__6;
extern lean_object* l_Lean_Parser_darrow___elambda__1___rarg___closed__3;
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_levelMVarToParam___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Term_8__elabTermUsing(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
@ -384,6 +384,7 @@ lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getLevel___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_List_repr___rarg___closed__2;
lean_object* l_Lean_Elab_Term_trySynthInstance___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_darrow___elambda__1___closed__3;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabRawCharLit(lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabTypeStx(lean_object*);
lean_object* l_Lean_Elab_Term_isClass___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -797,7 +798,6 @@ lean_object* l_Lean_Elab_Term_getMCtx___rarg(lean_object*);
extern lean_object* l_Lean_mkAppStx___closed__1;
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Term_3__fromMetaState___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentArray_foldlM___at___private_Init_Lean_Elab_Term_3__fromMetaState___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(lean_object*);
lean_object* l_Lean_Elab_Term_Lean_Elab_MonadMacroAdapter___closed__4;
lean_object* l_Lean_Elab_Term_monadLog___closed__4;
lean_object* l_Lean_Meta_isType(lean_object*, lean_object*, lean_object*);
@ -10646,7 +10646,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_darrow___elambda__1___rarg___closed__3;
x_2 = l_Lean_Parser_darrow___elambda__1___closed__3;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -18733,7 +18733,7 @@ x_4 = lean_array_get_size(x_1);
x_5 = lean_unsigned_to_nat(1u);
x_6 = lean_nat_sub(x_4, x_5);
lean_dec(x_4);
x_7 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_1);
x_7 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_1);
x_8 = l___private_Init_Lean_Elab_Term_10__mkPairsAux___main(x_1, x_6, x_7, x_2, x_3);
return x_8;
}

10
stage0/stdlib/Init/Lean/Elab/TermApp.c
View file

@ -234,10 +234,10 @@ lean_object* l___private_Init_Lean_Elab_TermApp_14__resolveLValAux___closed__7;
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_TermApp_26__elabAppAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_formatEntry___closed__1;
extern lean_object* l_Lean_Elab_Term_TermElabResult_inhabited;
extern lean_object* l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l_Lean_Elab_Term_TermElabM_inhabited___boxed(lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabExplicit___closed__1;
extern lean_object* l_Lean_Parser_Term_arrayRef___elambda__1___closed__2;
lean_object* l_Lean_Name_replacePrefix___main(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_TermApp_26__elabAppAux___closed__3;
lean_object* l___private_Init_Lean_Elab_TermApp_23__getSuccess(lean_object*);
@ -369,6 +369,7 @@ lean_object* l_Array_insertAt___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_pure___at___private_Init_Lean_Elab_TermApp_27__expandApp___spec__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_findField_x3f___main(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_TermApp_18__addLValArg___main___closed__6;
extern lean_object* l_Lean_Parser_Term_sortApp___elambda__1___closed__2;
lean_object* l_Lean_Name_components(lean_object*);
lean_object* l_Array_forMAux___main___at___private_Init_Lean_Elab_TermApp_15__resolveLValLoop___main___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Elab_Term_elabExplicitUniv___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -382,7 +383,6 @@ lean_object* l___private_Init_Lean_Elab_TermApp_14__resolveLValAux___closed__16;
lean_object* l___private_Init_Lean_Elab_TermApp_14__resolveLValAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_TermApp_18__addLValArg___main___closed__4;
lean_object* l___private_Init_Lean_Elab_TermApp_7__getForallBody(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_sortApp___elambda__1___rarg___closed__2;
lean_object* l_Lean_Elab_Term_Arg_inhabited;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_Elab_getPosition___at___private_Init_Lean_Elab_TermApp_24__toMessageData___spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -9380,7 +9380,7 @@ x_186 = l_coeDecidableEq(x_185);
if (x_186 == 0)
{
lean_object* x_187; uint8_t x_188;
x_187 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
x_187 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__2;
lean_inc(x_2);
x_188 = l_Lean_Syntax_isOfKind(x_2, x_187);
if (x_188 == 0)
@ -12639,7 +12639,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabArrayRef(lean_object* x_1
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
x_2 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__2;
x_3 = l___regBuiltinTermElab_Lean_Elab_Term_elabArrayRef___closed__2;
x_4 = l___regBuiltinTermElab_Lean_Elab_Term_elabArrayRef___closed__3;
x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1);
@ -12828,7 +12828,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSortApp(lean_object* x_1)
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Parser_Term_sortApp___elambda__1___rarg___closed__2;
x_2 = l_Lean_Parser_Term_sortApp___elambda__1___closed__2;
x_3 = l___regBuiltinTermElab_Lean_Elab_Term_elabSortApp___closed__2;
x_4 = l___regBuiltinTermElab_Lean_Elab_Term_elabSortApp___closed__3;
x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1);

23864
stage0/stdlib/Init/Lean/Parser/Command.c
View file

File diff suppressed because it is too large Load diff

1874
stage0/stdlib/Init/Lean/Parser/Level.c
View file

File diff suppressed because it is too large Load diff

1321
stage0/stdlib/Init/Lean/Parser/Module.c
View file

File diff suppressed because it is too large Load diff

15030
stage0/stdlib/Init/Lean/Parser/Parser.c
View file

File diff suppressed because it is too large Load diff

11534
stage0/stdlib/Init/Lean/Parser/Syntax.c
View file

File diff suppressed because it is too large Load diff

4350
stage0/stdlib/Init/Lean/Parser/Tactic.c
View file

File diff suppressed because it is too large Load diff

33766
stage0/stdlib/Init/Lean/Parser/Term.c
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Init/Lean/Parser/Transform.c
View file

@ -21,6 +21,7 @@ lean_object* lean_array_get_size(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_setTailInfo(lean_object*, lean_object*);
lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(lean_object*);
lean_object* lean_string_utf8_byte_size(lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___closed__2;
@ -41,7 +42,6 @@ lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_manyToSepBy___spec__1__
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
extern lean_object* l_Lean_mkOptionalNode___closed__2;
lean_object* l_Lean_Syntax_getTailInfo___main(lean_object*);
lean_object* l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(lean_object*);
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_manyToSepBy___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
@ -61,7 +61,7 @@ else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_8 = lean_array_fget(x_3, x_4);
x_9 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_5);
x_9 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_5);
x_10 = l_Lean_Syntax_getTailInfo___main(x_9);
x_11 = lean_unsigned_to_nat(1u);
x_12 = lean_nat_add(x_4, x_11);

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

@ -47,7 +47,6 @@ lean_object* l_Lean_Macro_throwUnsupported___boxed(lean_object*, lean_object*);
lean_object* l_Lean_identKind___closed__1;
lean_object* l_Lean_fieldIdxKind___closed__2;
lean_object* l_Lean_Syntax_getOptional_x3f(lean_object*);
lean_object* l_Lean_ParserDescr_orelse(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__2(lean_object*);
lean_object* l___private_Init_LeanInit_8__decodeHexDigit___boxed(lean_object*, lean_object*);
uint32_t l_Lean_idBeginEscape;
@ -57,7 +56,6 @@ lean_object* l___private_Init_LeanInit_4__extractMainModule(lean_object*, lean_o
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Array_filterSepElemsM___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isAtom___boxed(lean_object*);
lean_object* l_Lean_ParserDescr_optional(uint8_t, lean_object*);
lean_object* l_Array_mapSepElemsM___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_toNat___boxed(lean_object*);
lean_object* l_Lean_identKind___closed__2;
@ -65,7 +63,6 @@ lean_object* l___private_Init_LeanInit_8__decodeHexDigit(lean_object*, lean_obje
lean_object* l___private_Init_LeanInit_1__eraseMacroScopesAux___main(lean_object*);
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux(lean_object*);
lean_object* l_Lean_ParserDescr_lookahead(uint8_t, lean_object*);
lean_object* l_Array_findSomeMAux___main___at_Lean_Syntax_findAux___main___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_5__extractMacroScopesAux(lean_object*, lean_object*);
extern lean_object* l_Array_empty___closed__1;
@ -76,21 +73,17 @@ lean_object* l_Lean_fieldIdxKind___closed__1;
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main(lean_object*);
uint8_t l_Char_isDigit(uint32_t);
lean_object* l_Lean_charLitKind___closed__2;
lean_object* l_Lean_ParserDescr_many(uint8_t, lean_object*);
lean_object* l_Lean_isGreek___boxed(lean_object*);
uint32_t l_Lean_idEndEscape;
lean_object* l___private_Init_LeanInit_7__decodeOctalLitAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isIdRest___boxed(lean_object*);
lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
uint8_t l_Lean_isIdBeginEscape(uint32_t);
lean_object* l_Lean_ParserDescr_ident(uint8_t);
lean_object* l___private_Init_LeanInit_9__decodeHexLitAux___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_strLit(uint8_t);
lean_object* l_Lean_Name_HasToString___closed__1;
lean_object* l_Lean_mkNameSimple(lean_object*);
lean_object* l_Lean_isIdFirst___boxed(lean_object*);
lean_object* l_Lean_mkHole___boxed(lean_object*);
lean_object* l_Lean_ParserDescr_andthen___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_14__filterSepElemsMAux___main___at_Array_filterSepElems___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* l_Array_findSomeMAux___main___at_Lean_Syntax_findAux___main___spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -102,7 +95,6 @@ lean_object* l_Lean_Syntax_termIdToAntiquot___closed__3;
lean_object* l___private_Init_LeanInit_12__decodeQuotedChar___boxed__const__4;
lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_inhabited;
lean_object* l_Lean_ParserDescr_charLit(uint8_t);
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l_Lean_Syntax_identToStrLit(lean_object*);
lean_object* l___private_Init_LeanInit_6__decodeBinLitAux___main(lean_object*, lean_object*, lean_object*);
@ -119,7 +111,6 @@ lean_object* l_Lean_mkIdentFrom___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_decodeStrLitAux___main___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NameGenerator_Inhabited;
lean_object* l_Lean_mkTermIdFromIdent___closed__1;
lean_object* l_Lean_ParserDescr_try(uint8_t, lean_object*);
lean_object* l_Lean_nameLitKind;
lean_object* l_Lean_Syntax_termIdToAntiquot___closed__2;
lean_object* l_Lean_mkAppStx___closed__8;
@ -143,14 +134,12 @@ lean_object* l_Lean_Syntax_strLitToAtom(lean_object*);
lean_object* l_Lean_Syntax_isLit_x3f___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_hasArgs___boxed(lean_object*);
lean_object* l_Lean_mkStxNumLit(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescrCore_inhabited(uint8_t);
lean_object* l_Lean_Name_HasAppend___closed__1;
lean_object* l_Array_mapSepElems___boxed(lean_object*, lean_object*);
uint8_t l_Lean_Name_hasMacroScopes(lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__3(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isLit_x3f(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_termIdToAntiquot___closed__4;
lean_object* l_Lean_ParserDescr_many1(uint8_t, lean_object*);
lean_object* l___private_Init_LeanInit_15__mapSepElemsMAux___main___at_Array_mapSepElems___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isCharLit_x3f(lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
@ -160,7 +149,6 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_findAux___main(lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_6__decodeBinLitAux___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_numLitKind;
lean_object* l_Lean_ParserDescr_many___boxed(lean_object*, lean_object*);
lean_object* l_Lean_choiceKind___closed__1;
lean_object* l___private_Init_LeanInit_7__decodeOctalLitAux___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapSepElemsM(lean_object*);
@ -174,10 +162,8 @@ lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isSimpleTermId_x3f___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getId___boxed(lean_object*);
lean_object* l___private_Init_LeanInit_13__decodeNameLitAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_numLit___boxed(lean_object*);
lean_object* l_Lean_Syntax_isFieldIdx_x3f(lean_object*);
lean_object* l_Substring_takeWhileAux___main___at___private_Init_LeanInit_13__decodeNameLitAux___main___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_many1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Macro_addMacroScope(lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_14__filterSepElemsMAux___main___at_Array_filterSepElems___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkTermIdFrom___boxed(lean_object*, lean_object*);
@ -204,47 +190,35 @@ lean_object* l_Lean_mkNullNode(lean_object*);
lean_object* l_Lean_strLitKind___closed__2;
lean_object* l_Lean_NameGenerator_Inhabited___closed__1;
size_t l_Lean_Name_hash(lean_object*);
lean_object* l_Lean_ParserDescr_parser(uint8_t, lean_object*, lean_object*);
lean_object* l_Nat_repr(lean_object*);
lean_object* l_Array_mapSepElemsM___at_Array_mapSepElems___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_HasToString;
lean_object* l___private_Init_LeanInit_13__decodeNameLitAux___main___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_lookahead___boxed(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_sepBy(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_choiceKind;
lean_object* l_Lean_charLitKind;
lean_object* l_Substring_takeWhileAux___main___at___private_Init_LeanInit_13__decodeNameLitAux___main___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_andthen(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_charLit___boxed(lean_object*);
lean_object* l___private_Init_LeanInit_6__decodeBinLitAux___main___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_symbol___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_findSomeMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_9__decodeHexLitAux___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_numLitKind___closed__2;
lean_object* l_Lean_ParserDescr_node(uint8_t, lean_object*, lean_object*);
uint32_t lean_string_utf8_get(lean_object*, lean_object*);
lean_object* l_Lean_mkAppStx___closed__6;
lean_object* l_Lean_ParserDescr_try___boxed(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_ident___boxed(lean_object*);
lean_object* l_Lean_mkOptionalNode(lean_object*);
lean_object* l_Nat_pred(lean_object*);
uint8_t l_Array_isEmpty___rarg(lean_object*);
lean_object* l_Lean_Name_toStringWithSep___boxed(lean_object*, lean_object*);
lean_object* l_Array_filterSepElemsM(lean_object*);
lean_object* l_Lean_firstFrontendMacroScope;
lean_object* l_Lean_ParserDescr_node___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_nameLit___boxed(lean_object*);
lean_object* l_Lean_ParserDescr_inhabited___closed__1;
lean_object* l_Lean_NameGenerator_mkChild(lean_object*);
lean_object* l_Lean_ParserDescr_parser___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isCharLit_x3f___boxed(lean_object*);
lean_object* l___private_Init_LeanInit_2__assembleParts(lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_nullKind___closed__1;
lean_object* l_Lean_Syntax_decodeStrLit___boxed(lean_object*);
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_nonReservedSymbol___boxed(lean_object*, lean_object*);
uint8_t l_Lean_isIdEndEscape(uint32_t);
lean_object* l_Lean_Syntax_decodeCharLit(lean_object*);
lean_object* l_Lean_MacroScopesView_inhabited___closed__1;
@ -262,12 +236,8 @@ lean_object* l_Lean_Syntax_getHeadInfo___main(lean_object*);
lean_object* l_Lean_mkAppStx___closed__3;
lean_object* l_Lean_isLetterLike___boxed(lean_object*);
lean_object* l_Lean_Syntax_isIdOrAtom_x3f(lean_object*);
lean_object* l_Lean_ParserDescrCore_inhabited___boxed(lean_object*);
uint8_t l_Lean_Name_hasMacroScopes___main(lean_object*);
lean_object* l_Lean_ParserDescr_strLit___boxed(lean_object*);
lean_object* l_Lean_identKind;
lean_object* l_Lean_ParserDescr_trailingNode(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_sepBy1(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_mkCTermId(lean_object*);
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
lean_object* l_Lean_Syntax_inhabited;
@ -305,7 +275,6 @@ lean_object* l___private_Init_LeanInit_12__decodeQuotedChar___boxed__const__2;
lean_object* l_Lean_mkHole___closed__1;
lean_object* l_Lean_Name_hasMacroScopes___boxed(lean_object*);
lean_object* l_Lean_isIdBeginEscape___boxed(lean_object*);
lean_object* l_Lean_ParserDescr_numLit(uint8_t);
lean_object* l_Lean_mkStxStrLit(lean_object*, lean_object*);
lean_object* lean_nat_mul(lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_13__decodeNameLitAux___boxed(lean_object*, lean_object*, lean_object*);
@ -320,7 +289,6 @@ lean_object* l_Lean_mkTermIdFrom(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_decodeNameLit(lean_object*);
lean_object* l_Lean_mkOptionalNode___closed__1;
lean_object* l_Lean_Syntax_isNameLit_x3f(lean_object*);
lean_object* l_Lean_ParserDescr_orelse___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isIdEndEscape___boxed(lean_object*);
lean_object* l_Lean_Syntax_getOptionalIdent_x3f___boxed(lean_object*);
lean_object* l___private_Init_LeanInit_10__decodeDecimalLitAux___main___boxed(lean_object*, lean_object*, lean_object*);
@ -333,13 +301,13 @@ lean_object* l_Lean_Syntax_isNone___boxed(lean_object*);
lean_object* l_Lean_mkCIdentFrom___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkHole___closed__2;
lean_object* l_Lean_mkCIdentFrom___closed__1;
lean_object* l_Lean_ParserDescr_inhabited;
lean_object* l_Lean_Syntax_decodeNameLit___boxed(lean_object*);
lean_object* lean_string_length(lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___closed__1;
lean_object* l_Lean_nameLitKind___closed__2;
uint8_t l_Lean_isSubScriptAlnum(uint32_t);
lean_object* l_List_foldl___main___at_Lean_MacroScopesView_review___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_sepBy___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Macro_throwUnsupported(lean_object*, lean_object*);
lean_object* lean_mk_syntax_ident(lean_object*);
lean_object* l_Lean_mkStxLit(lean_object*, lean_object*, lean_object*);
@ -362,15 +330,12 @@ lean_object* l_Lean_mkAtomFrom___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_14__filterSepElemsMAux___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Array_filterSepElemsM___at_Array_filterSepElems___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_symbol(uint8_t, lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_9__decodeHexLitAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__1(lean_object*);
lean_object* l___private_Init_LeanInit_14__filterSepElemsMAux___boxed(lean_object*);
uint8_t l_UInt32_decLe(uint32_t, uint32_t);
lean_object* l_Lean_ParserDescr_optional___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkAppStx___closed__2;
lean_object* l___private_Init_LeanInit_14__filterSepElemsMAux___main___boxed(lean_object*);
lean_object* l_Lean_ParserDescr_nonReservedSymbol(lean_object*, uint8_t);
lean_object* l_Lean_Name_hasMacroScopes___main___boxed(lean_object*);
lean_object* l_Lean_Name_hasMacroScopes___main___closed__1;
lean_object* l_Lean_Syntax_findAux(lean_object*, lean_object*);
@ -386,7 +351,6 @@ lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_Lean_mkAppStx___closed__1;
lean_object* l___private_Init_LeanInit_3__extractImported___main(lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_string_hash(lean_object*);
lean_object* l_Lean_ParserDescr_sepBy1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_1__eraseMacroScopesAux___main___boxed(lean_object*);
lean_object* l_Lean_Name_append___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_14__filterSepElemsMAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -401,7 +365,6 @@ uint32_t l_Char_ofNat(lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_12__decodeQuotedChar___boxed__const__3;
uint8_t l_Lean_Syntax_isIdent(lean_object*);
lean_object* l_Lean_ParserDescr_nameLit(uint8_t);
uint8_t l_Lean_isGreek(uint32_t x_1) {
_start:
{
@ -1530,399 +1493,24 @@ return x_17;
}
}
}
lean_object* l_Lean_ParserDescrCore_inhabited(uint8_t x_1) {
lean_object* _init_l_Lean_ParserDescr_inhabited___closed__1() {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = lean_box(0);
x_3 = l_String_splitAux___main___closed__1;
x_4 = lean_alloc_ctor(11, 2, 1);
lean_ctor_set(x_4, 0, x_3);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
return x_4;
}
}
lean_object* l_Lean_ParserDescrCore_inhabited___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_ParserDescrCore_inhabited(x_2);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_andthen(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_andthen___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_1);
lean_dec(x_1);
x_5 = l_Lean_ParserDescr_andthen(x_4, x_2, x_3);
return x_5;
}
}
lean_object* l_Lean_ParserDescr_orelse(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_ctor(1, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_orelse___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_1);
lean_dec(x_1);
x_5 = l_Lean_ParserDescr_orelse(x_4, x_2, x_3);
return x_5;
}
}
lean_object* l_Lean_ParserDescr_optional(uint8_t x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_ctor(2, 1, 1);
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_3 = lean_alloc_ctor(11, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_1);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_optional___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* _init_l_Lean_ParserDescr_inhabited() {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = l_Lean_ParserDescr_optional(x_3, x_2);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_lookahead(uint8_t x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_ctor(3, 1, 1);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_1);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_lookahead___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = l_Lean_ParserDescr_lookahead(x_3, x_2);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_try(uint8_t x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_ctor(4, 1, 1);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_1);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_try___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = l_Lean_ParserDescr_try(x_3, x_2);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_many(uint8_t x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_1);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_many___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = l_Lean_ParserDescr_many(x_3, x_2);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_many1(uint8_t x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_ctor(6, 1, 1);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_1);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_many1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = l_Lean_ParserDescr_many1(x_3, x_2);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_sepBy(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_ctor(7, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_sepBy___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_1);
lean_dec(x_1);
x_5 = l_Lean_ParserDescr_sepBy(x_4, x_2, x_3);
return x_5;
}
}
lean_object* l_Lean_ParserDescr_sepBy1(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_ctor(8, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_sepBy1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_1);
lean_dec(x_1);
x_5 = l_Lean_ParserDescr_sepBy1(x_4, x_2, x_3);
return x_5;
}
}
lean_object* l_Lean_ParserDescr_node(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_ctor(9, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_node___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_1);
lean_dec(x_1);
x_5 = l_Lean_ParserDescr_node(x_4, x_2, x_3);
return x_5;
}
}
lean_object* l_Lean_ParserDescr_trailingNode(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_symbol(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_ctor(11, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_symbol___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_1);
lean_dec(x_1);
x_5 = l_Lean_ParserDescr_symbol(x_4, x_2, x_3);
return x_5;
}
}
lean_object* l_Lean_ParserDescr_numLit(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(13, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_ParserDescr_numLit___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_ParserDescr_numLit(x_2);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_strLit(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(14, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_ParserDescr_strLit___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_ParserDescr_strLit(x_2);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_charLit(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(15, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_ParserDescr_charLit___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_ParserDescr_charLit(x_2);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_nameLit(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(16, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_ParserDescr_nameLit___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_ParserDescr_nameLit(x_2);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_ident(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(17, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_ParserDescr_ident___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_ParserDescr_ident(x_2);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_nonReservedSymbol(lean_object* x_1, uint8_t x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_ctor(12, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_nonReservedSymbol___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_unbox(x_2);
lean_dec(x_2);
x_4 = l_Lean_ParserDescr_nonReservedSymbol(x_1, x_3);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_parser(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_ctor(18, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_parser___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_1);
lean_dec(x_1);
x_5 = l_Lean_ParserDescr_parser(x_4, x_2, x_3);
return x_5;
lean_object* x_1;
x_1 = l_Lean_ParserDescr_inhabited___closed__1;
return x_1;
}
}
lean_object* _init_l_Lean_Syntax_inhabited() {
@ -6957,6 +6545,10 @@ l_Lean_NameGenerator_Inhabited___closed__3 = _init_l_Lean_NameGenerator_Inhabite
lean_mark_persistent(l_Lean_NameGenerator_Inhabited___closed__3);
l_Lean_NameGenerator_Inhabited = _init_l_Lean_NameGenerator_Inhabited();
lean_mark_persistent(l_Lean_NameGenerator_Inhabited);
l_Lean_ParserDescr_inhabited___closed__1 = _init_l_Lean_ParserDescr_inhabited___closed__1();
lean_mark_persistent(l_Lean_ParserDescr_inhabited___closed__1);
l_Lean_ParserDescr_inhabited = _init_l_Lean_ParserDescr_inhabited();
lean_mark_persistent(l_Lean_ParserDescr_inhabited);
l_Lean_Syntax_inhabited = _init_l_Lean_Syntax_inhabited();
lean_mark_persistent(l_Lean_Syntax_inhabited);
l_Lean_choiceKind___closed__1 = _init_l_Lean_choiceKind___closed__1();