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-12-05 07:40:35 -08:00
parent bcf4ffdd1a
commit 6f6e153a85
6 changed files with 5164 additions and 5049 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
stage0/src/Lean/Parser/Syntax.lean generated
View file

@ -44,28 +44,25 @@ namespace Command
def optPrio := optional ("[" >> numLit >> "]")
def «scoped» := parser! "scoped "
def «local» := parser! "local "
def attrKind := optional («scoped» <|> «local»)
def «prefix» := parser! "prefix"
def «infix» := parser! "infix"
def «infixl» := parser! "infixl"
def «infixr» := parser! "infixr"
def «postfix» := parser! "postfix"
def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «postfix»
@[builtinCommandParser] def «mixfix» := parser! attrKind >> mixfixKind >> optPrecedence >> optPrio >> ppSpace >> strLit >> darrow >> termParser
@[builtinCommandParser] def «mixfix» := parser! Term.attrKind >> mixfixKind >> optPrecedence >> optPrio >> ppSpace >> strLit >> darrow >> termParser
-- NOTE: We use `suppressInsideQuot` in the following parsers because quotations inside them are evaluated in the same stage and
-- thus should be ignored when we use `checkInsideQuot` to prepare the next stage for a builtin syntax change
def identPrec := parser! ident >> optPrecedence
def optKind : Parser := optional ("[" >> ident >> "]")
def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Parser.Command.notationItem) (strLit <|> identPrec)
@[builtinCommandParser] def «notation» := parser! attrKind >> "notation" >> optPrecedence >> optPrio >> many notationItem >> darrow >> termParser
@[builtinCommandParser] def «notation» := parser! Term.attrKind >> "notation" >> optPrecedence >> optPrio >> many notationItem >> darrow >> termParser
@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (parser! "macro_rules" >> optKind >> Term.matchAlts)
def parserKind := parser! ident
def parserPrio := parser! numLit
def parserKindPrio := parser! atomic (ident >> ", ") >> numLit
def optKindPrio : Parser := optional ("[" >> (parserKindPrio <|> parserKind <|> parserPrio) >> "]")
@[builtinCommandParser] def «syntax» := parser! attrKind >> "syntax " >> optPrecedence >> optKindPrio >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def «syntax» := parser! Term.attrKind >> "syntax " >> optPrecedence >> optKindPrio >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def syntaxAbbrev := parser! "syntax " >> ident >> " := " >> many1 syntaxParser
@[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident
def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> syntaxParser maxPrec

5
stage0/src/Lean/Parser/Term.lean generated
View file

@ -152,7 +152,10 @@ def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFoll
@[builtinTermParser] def «let*» := parser!:leadPrec withPosition ("let* " >> letDecl) >> optSemicolon termParser
def attrArg : Parser := ident <|> strLit <|> numLit
-- use `rawIdent` because of attribute names such as `instance`
def attrInstance := ppGroup $ parser! optional "scoped" >> rawIdent >> many (ppSpace >> attrArg)
def «scoped» := parser! "scoped "
def «local» := parser! "local "
def attrKind := optional («scoped» <|> «local»)
def attrInstance := ppGroup $ parser! attrKind >> rawIdent >> many (ppSpace >> attrArg)
def attributes := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
def letRecDecls := sepBy1 (group (optional «attributes» >> letDecl)) ", "

7883
stage0/stdlib/Lean/Elab/Syntax.c generated
View file

File diff suppressed because it is too large Load diff

236
stage0/stdlib/Lean/Parser/Command.c generated
View file

@ -20,7 +20,6 @@ lean_object* l_Lean_Parser_Command_universes_formatter(lean_object*, lean_object
lean_object* l_Lean_Parser_Command_check__failure___closed__5;
lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__3;
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1121____closed__23;
lean_object* l_Lean_Parser_Command_attribute_formatter___closed__11;
lean_object* l_Lean_Parser_Command_builtin__initialize___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_example___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_declModifiers_formatter___closed__22;
@ -647,7 +646,6 @@ lean_object* l___regBuiltin_Lean_Parser_Term_quot_formatter___closed__1;
lean_object* l_Lean_Parser_Command_noncomputable_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_structureTk_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_universe_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__23;
lean_object* l_Lean_Parser_Command_universe___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_declaration_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_ctor___closed__10;
@ -701,6 +699,7 @@ lean_object* l_Lean_Parser_Command_openSimple___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__20;
lean_object* l_Lean_Parser_Command_declaration_formatter___closed__10;
lean_object* l_Lean_Parser_optional_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_local___closed__1;
lean_object* l_Lean_Parser_Command_instance_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_initialize___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_example___elambda__1___closed__1;
@ -708,7 +707,6 @@ lean_object* l_Lean_Parser_Command_ctor_formatter___closed__2;
lean_object* l_Lean_Parser_Command_declValSimple_formatter___closed__3;
lean_object* l_Lean_Parser_Command_universes_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Command_openRenamingItem___closed__4;
lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__21;
lean_object* l_Lean_Parser_Command_declValSimple___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_open___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_extends___closed__5;
@ -834,7 +832,6 @@ lean_object* l_Lean_Parser_Command_structExplicitBinder_formatter___closed__3;
lean_object* l_Lean_Parser_Command_extends___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_structExplicitBinder___closed__4;
lean_object* l_Lean_Parser_Command_init__quot_formatter___closed__2;
lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__20;
lean_object* l_Lean_Parser_Command_openHiding_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_abbrev___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_variables___elambda__1___closed__4;
@ -1259,6 +1256,7 @@ lean_object* l_Lean_Parser_Command_classTk___closed__2;
lean_object* l_Lean_Parser_Command_declValEqns_formatter___closed__2;
lean_object* l_Lean_Parser_Command_noncomputable_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_initialize___elambda__1___closed__14;
extern lean_object* l_Lean_Parser_Term_local_formatter___closed__2;
lean_object* l_Lean_Parser_Command_structSimpleBinder_formatter___closed__2;
lean_object* l_Lean_Parser_Command_declaration___elambda__1___closed__11;
lean_object* l_Lean_Parser_Command_optDeclSig_formatter___closed__2;
@ -1462,7 +1460,6 @@ lean_object* l_Lean_Parser_Term_quot___closed__10;
lean_object* l_Lean_Parser_Command_inductive_parenthesizer___closed__9;
lean_object* l_Lean_Parser_Command_noncomputable_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_declSig___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__22;
lean_object* l_Lean_Parser_Command_structSimpleBinder___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_declModifiers_formatter___closed__8;
lean_object* l_Lean_Parser_Command_structFields___elambda__1___closed__9;
@ -2310,6 +2307,7 @@ lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_openOnly_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_openOnly___closed__7;
lean_object* l_Lean_Parser_Command_attribute_formatter___closed__7;
extern lean_object* l_Lean_Parser_Term_local___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__14;
lean_object* l_Lean_Parser_Command_inductive_formatter___closed__7;
lean_object* l_Lean_Parser_Command_classInductive_formatter___closed__4;
@ -23925,9 +23923,13 @@ return x_4;
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("local ");
return x_1;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_local___closed__1;
x_2 = l_Lean_Parser_Term_local___elambda__1___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);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__6() {
@ -23935,51 +23937,11 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__5;
x_2 = l_String_trim(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__6;
x_2 = l_Lean_Parser_symbolInfo(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__6;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__7;
x_2 = l_Lean_Parser_Command_attribute___elambda__1___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);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__9;
x_2 = l_Lean_Parser_optional(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__11() {
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__7() {
_start:
{
lean_object* x_1;
@ -23987,59 +23949,98 @@ x_1 = lean_mk_string("] ");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__12() {
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__11;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__7;
x_2 = l_String_trim(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__13() {
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__12;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__8;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__14() {
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__7;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
x_3 = l_Lean_Parser_Command_attribute___elambda__1___closed__13;
x_3 = l_Lean_Parser_Command_attribute___elambda__1___closed__9;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_4, 0, x_3);
lean_closure_set(x_4, 1, x_2);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__15() {
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_attributes___elambda__1___closed__3;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
x_3 = l_Lean_Parser_Command_attribute___elambda__1___closed__14;
x_3 = l_Lean_Parser_Command_attribute___elambda__1___closed__10;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_4, 0, x_2);
lean_closure_set(x_4, 1, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__16() {
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_mkAntiquotScope___closed__5;
x_2 = l_Lean_Parser_Command_attribute___elambda__1___closed__15;
x_2 = l_Lean_Parser_Command_attribute___elambda__1___closed__11;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__13() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("attribute ");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__13;
x_2 = l_String_trim(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__14;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__15;
x_2 = l_Lean_Parser_Command_attribute___elambda__1___closed__12;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -24049,74 +24050,35 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__17() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("attribute ");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__17;
x_2 = l_String_trim(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__19() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__18;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__20() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__19;
x_2 = l_Lean_Parser_Command_attribute___elambda__1___closed__16;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__21() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__10;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__6;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
x_3 = l_Lean_Parser_Command_attribute___elambda__1___closed__20;
x_3 = l_Lean_Parser_Command_attribute___elambda__1___closed__16;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_4, 0, x_2);
lean_closure_set(x_4, 1, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__22() {
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__2;
x_2 = l_Lean_Parser_Command_attribute___elambda__1___closed__21;
x_2 = l_Lean_Parser_Command_attribute___elambda__1___closed__17;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__23() {
static lean_object* _init_l_Lean_Parser_Command_attribute___elambda__1___closed__19() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_sepByScopeSuffixes___elambda__1___closed__11;
x_2 = l_Lean_Parser_Command_attribute___elambda__1___closed__22;
x_2 = l_Lean_Parser_Command_attribute___elambda__1___closed__18;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -24130,7 +24092,7 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; lean_object*
x_3 = l_Lean_Parser_Command_attribute___elambda__1___closed__4;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
x_5 = l_Lean_Parser_Command_attribute___elambda__1___closed__23;
x_5 = l_Lean_Parser_Command_attribute___elambda__1___closed__19;
x_6 = 1;
x_7 = l_Lean_Parser_orelseFnCore(x_4, x_5, x_6, x_1, x_2);
return x_7;
@ -24140,7 +24102,7 @@ static lean_object* _init_l_Lean_Parser_Command_attribute___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__12;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__8;
x_2 = l_Lean_Parser_symbolInfo(x_1);
return x_2;
}
@ -24183,7 +24145,7 @@ static lean_object* _init_l_Lean_Parser_Command_attribute___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__18;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__14;
x_2 = l_Lean_Parser_symbolInfo(x_1);
return x_2;
}
@ -24202,7 +24164,7 @@ static lean_object* _init_l_Lean_Parser_Command_attribute___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__10;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__6;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Command_attribute___closed__6;
@ -24302,8 +24264,8 @@ static lean_object* _init_l_Lean_Parser_Command_attribute_formatter___closed__2(
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__5;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_symbol_formatter), 6, 1);
x_1 = l_Lean_Parser_Term_local_formatter___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_optional_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
@ -24312,8 +24274,8 @@ static lean_object* _init_l_Lean_Parser_Command_attribute_formatter___closed__3(
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute_formatter___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_optional_formatter), 6, 1);
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__13;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_symbol_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
@ -24322,7 +24284,7 @@ static lean_object* _init_l_Lean_Parser_Command_attribute_formatter___closed__4(
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__17;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__7;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_symbol_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -24331,19 +24293,21 @@ return x_2;
static lean_object* _init_l_Lean_Parser_Command_attribute_formatter___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__11;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_symbol_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_attribute_formatter___closed__4;
x_2 = l_Lean_Parser_Command_structExplicitBinder_formatter___closed__4;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute_formatter___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_attribute_formatter___closed__5;
x_2 = l_Lean_Parser_Command_structExplicitBinder_formatter___closed__4;
x_1 = l_Lean_Parser_Term_attributes_formatter___closed__4;
x_2 = l_Lean_Parser_Command_attribute_formatter___closed__5;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -24354,7 +24318,7 @@ static lean_object* _init_l_Lean_Parser_Command_attribute_formatter___closed__7(
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_attributes_formatter___closed__4;
x_1 = l_Lean_Parser_mkAntiquotScope_formatter___closed__1;
x_2 = l_Lean_Parser_Command_attribute_formatter___closed__6;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -24366,7 +24330,7 @@ static lean_object* _init_l_Lean_Parser_Command_attribute_formatter___closed__8(
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_mkAntiquotScope_formatter___closed__1;
x_1 = l_Lean_Parser_Command_attribute_formatter___closed__3;
x_2 = l_Lean_Parser_Command_attribute_formatter___closed__7;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -24378,7 +24342,7 @@ static lean_object* _init_l_Lean_Parser_Command_attribute_formatter___closed__9(
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_attribute_formatter___closed__4;
x_1 = l_Lean_Parser_Command_attribute_formatter___closed__2;
x_2 = l_Lean_Parser_Command_attribute_formatter___closed__8;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -24389,22 +24353,10 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Command_attribute_formatter___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_attribute_formatter___closed__3;
x_2 = l_Lean_Parser_Command_attribute_formatter___closed__9;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_attribute_formatter___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_attribute___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Command_attribute_formatter___closed__10;
x_3 = l_Lean_Parser_Command_attribute_formatter___closed__9;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -24417,7 +24369,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Command_attribute_formatter___closed__1;
x_7 = l_Lean_Parser_Command_attribute_formatter___closed__11;
x_7 = l_Lean_Parser_Command_attribute_formatter___closed__10;
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -32681,14 +32633,6 @@ l_Lean_Parser_Command_attribute___elambda__1___closed__18 = _init_l_Lean_Parser_
lean_mark_persistent(l_Lean_Parser_Command_attribute___elambda__1___closed__18);
l_Lean_Parser_Command_attribute___elambda__1___closed__19 = _init_l_Lean_Parser_Command_attribute___elambda__1___closed__19();
lean_mark_persistent(l_Lean_Parser_Command_attribute___elambda__1___closed__19);
l_Lean_Parser_Command_attribute___elambda__1___closed__20 = _init_l_Lean_Parser_Command_attribute___elambda__1___closed__20();
lean_mark_persistent(l_Lean_Parser_Command_attribute___elambda__1___closed__20);
l_Lean_Parser_Command_attribute___elambda__1___closed__21 = _init_l_Lean_Parser_Command_attribute___elambda__1___closed__21();
lean_mark_persistent(l_Lean_Parser_Command_attribute___elambda__1___closed__21);
l_Lean_Parser_Command_attribute___elambda__1___closed__22 = _init_l_Lean_Parser_Command_attribute___elambda__1___closed__22();
lean_mark_persistent(l_Lean_Parser_Command_attribute___elambda__1___closed__22);
l_Lean_Parser_Command_attribute___elambda__1___closed__23 = _init_l_Lean_Parser_Command_attribute___elambda__1___closed__23();
lean_mark_persistent(l_Lean_Parser_Command_attribute___elambda__1___closed__23);
l_Lean_Parser_Command_attribute___closed__1 = _init_l_Lean_Parser_Command_attribute___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_attribute___closed__1);
l_Lean_Parser_Command_attribute___closed__2 = _init_l_Lean_Parser_Command_attribute___closed__2();
@ -32738,8 +32682,6 @@ l_Lean_Parser_Command_attribute_formatter___closed__9 = _init_l_Lean_Parser_Comm
lean_mark_persistent(l_Lean_Parser_Command_attribute_formatter___closed__9);
l_Lean_Parser_Command_attribute_formatter___closed__10 = _init_l_Lean_Parser_Command_attribute_formatter___closed__10();
lean_mark_persistent(l_Lean_Parser_Command_attribute_formatter___closed__10);
l_Lean_Parser_Command_attribute_formatter___closed__11 = _init_l_Lean_Parser_Command_attribute_formatter___closed__11();
lean_mark_persistent(l_Lean_Parser_Command_attribute_formatter___closed__11);
l___regBuiltin_Lean_Parser_Command_attribute_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Command_attribute_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Command_attribute_formatter___closed__1);
res = l___regBuiltin_Lean_Parser_Command_attribute_formatter(lean_io_mk_world());

805
stage0/stdlib/Lean/Parser/Syntax.c generated
View file

File diff suppressed because it is too large Load diff

1275
stage0/stdlib/Lean/Parser/Term.c generated
View file

File diff suppressed because it is too large Load diff