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 2022-07-27 13:41:21 -07:00
parent 1c770ac8d7
commit 00dd9da304
9 changed files with 2278 additions and 1038 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
stage0/src/Init/Notation.lean generated
View file

@ -9,10 +9,34 @@ prelude
import Init.Prelude
import Init.Coe
-- DSL for specifying parser precedences and priorities
/-- Auxiliary type used to represent syntax categories. We mainly use them to attach doc strings to syntax categories. -/
structure Lean.Parser.Category
namespace Lean.Parser.Category
/-- The command syntax category. -/
def command : Category := {}
/-- The term syntax category. -/
def term : Category := {}
/-- The tactic syntax category. -/
def tactic : Category := {}
/-- The syntax category for elements that can appear in the `do` notation. -/
def doElem : Category := {}
/-- The attribute syntax category. Declarations can be annotated with attributes using the `@[...]` notation. -/
def attr : Category := {}
/-- The syntax syntax category. This is the syntax category used to define syntax itself. -/
def stx : Category := {}
/-- The priority syntax category. Priorities are used in many different attributes. -/
def prio : Category := {}
/-- The precedence syntax category. Parsers have precedence in Lean. -/
def prec : Category := {}
end Lean.Parser.Category
namespace Lean.Parser.Syntax
/-! DSL for specifying parser precedences and priorities -/
syntax:65 (name := addPrec) prec " + " prec:66 : prec
syntax:65 (name := subPrec) prec " - " prec:66 : prec

41
stage0/src/Init/Prelude.lean generated
View file

@ -102,6 +102,47 @@ opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
-/
init_quot
/--
Let `α` be any type, and let `r` be an equivalence relation on `α`.
It is mathematically common to form the "quotient" `α / r`, that is, the type of elements of `α` "modulo" `r`.
Set theoretically, one can view `α / r` as the set of equivalence classes of `α` modulo `r`.
If `f : α → β` is any function that respects the equivalence relation in the sense that for every `x y : α`, `r x y` implies `f x = f y`,
then f "lifts" to a function `f' : α / r → β` defined on each equivalence class `⟦x⟧` by `f' ⟦x⟧ = f x`.
Lean extends the Calculus of Constructions with additional constants that perform exactly these constructions,
and installs this last equation as a definitional reduction rule.
Given a type `α` and any binary relation `r` on `α`, `Quot r` is a type. Note that `r` is not required to be
an equilance relation. `Quot` is the basic building block used to construct later the type `Quotient`.
-/
add_decl_doc Quot
/--
Given a type `α` and any binary relation `r` on `α`, `Quot.mk` maps `α` to `Quot r`.
So that if `r : α → α → Prop` and `a : α`, then `Quot.mk r a` is an element of `Quot r`.
See `Quot`.
-/
add_decl_doc Quot.mk
/--
Given a type `α` and any binary relation `r` on `α`,
`Quot.ind` says that every element of `Quot r` is of the form `Quot.mk r a`.
See `Quot` and `Quot.lift`.
-/
add_decl_doc Quot.ind
/--
Given a type `α`, any binary relation `r` on `α`, a function `f : α → β`, and a proof `h`
that `f` respects the relation `r`, then `Quot.lift f h` is the corresponding function on `Quot r`.
The idea is that for each element `a` in `α`, the function `Quot.lift f h` maps `Quot.mk r a`
(the `r`-class containing `a`) to `f a`, wherein `h` shows that this function is well defined.
In fact, the computation principle is declared as a reduction rule.
-/
add_decl_doc Quot.lift
inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
| refl (a : α) : HEq a a

22
stage0/src/Lean/Elab/Syntax.lean generated
View file

@ -87,6 +87,12 @@ def resolveParserName [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv
| _ => none
catch _ => return []
/-- (Try to) a term info for the category `catName` at `ref`. -/
def addCategoryInfo (ref : Syntax) (catName : Name) : TermElabM Unit := do
let declName := ``Lean.Parser.Category ++ catName
if (← getEnv).contains declName then
addTermInfo' ref (Lean.mkConst declName)
open TSyntax.Compat in
/--
Given a `stx` of category `syntax`, return a `(newStx, lhsPrec?)`,
@ -148,6 +154,7 @@ where
throwErrorAt stx "invalid atomic left recursive syntax"
let prec? ← liftMacroM <| expandOptPrecedence stx[1]
let prec := prec?.getD 0
addCategoryInfo stx catName
return (← `(ParserDescr.cat $(quote catName) $(quote prec)), 1)
processAlias (id : Syntax) (args : Array Syntax) := do
@ -254,19 +261,21 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d
elabCommand cmd
@[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab := fun stx => do
let catName := stx[1].getId
let docString? := stx[0].getOptional?.map fun stx => ⟨stx⟩
let catName := stx[2].getId
let catBehavior :=
if stx[2].isNone then
if stx[3].isNone then
Parser.LeadingIdentBehavior.default
else if stx[2][3].getKind == ``Parser.Command.catBehaviorBoth then
else if stx[3][3].getKind == ``Parser.Command.catBehaviorBoth then
Parser.LeadingIdentBehavior.both
else
Parser.LeadingIdentBehavior.symbol
let attrName := catName.appendAfter "Parser"
let env ← getEnv
let env ← Parser.registerParserCategory env attrName catName catBehavior
setEnv env
setEnv (← Parser.registerParserCategory (← getEnv) attrName catName catBehavior)
let catDeclName := `_root_ ++ ``Lean.Parser.Category ++ catName
let cmd ← `($[$docString?]? def $(mkIdentFrom stx[2] catDeclName) : Lean.Parser.Category := {})
declareSyntaxCatQuotParser catName
elabCommand cmd
/--
Auxiliary function for creating declaration names from parser descriptions.
@ -330,6 +339,7 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
let cat := catStx.getId.eraseMacroScopes
unless (Parser.isParserCategory (← getEnv) cat) do
throwErrorAt catStx "unknown category '{cat}'"
liftTermElabM none <| Term.addCategoryInfo catStx cat
let syntaxParser := mkNullNode ps
-- If the user did not provide an explicit precedence, we assign `maxPrec` to atom-like syntax and `leadPrec` otherwise.
let precDefault := if isAtomLikeSyntax syntaxParser then Parser.maxPrec else Parser.leadPrec

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

@ -74,7 +74,7 @@ def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Par
def catBehaviorBoth := leading_parser nonReservedSymbol "both"
def catBehaviorSymbol := leading_parser nonReservedSymbol "symbol"
def catBehavior := optional ("(" >> nonReservedSymbol "behavior" >> " := " >> (catBehaviorBoth <|> catBehaviorSymbol) >> ")")
@[builtinCommandParser] def syntaxCat := leading_parser "declare_syntax_cat " >> ident >> catBehavior
@[builtinCommandParser] def syntaxCat := leading_parser optional docComment >> "declare_syntax_cat " >> ident >> catBehavior
def macroArg := leading_parser optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> syntaxParser argPrec
def macroRhs (quotP : Parser) : Parser := leading_parser "`(" >> incQuotDepth quotP >> ")" <|> withPosition termParser
def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >> macroRhs Tactic.seq1

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

@ -197,10 +197,39 @@ def letPatDecl := leading_parser (withAnonymousAntiquot := false) atomic (termP
def letEqnsDecl := leading_parser (withAnonymousAntiquot := false) letIdLhs >> (" := " <|> matchAlts)
-- Remark: we disable anonymous antiquotations here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl`
def letDecl := leading_parser (withAnonymousAntiquot := false) notFollowedBy (nonReservedSymbol "rec") "rec" >> (letIdDecl <|> letPatDecl <|> letEqnsDecl)
/--
`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example, assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
-/
@[builtinTermParser] def «let» := leading_parser:leadPrec withPosition ("let " >> letDecl) >> optSemicolon termParser
/--
`let_fun x := v; b` is syntax sugar for `(fun x => b) v`. It is very similar to `let x := v; b`, but they are not equivalent.
In `let_fun`, the value `v` has been abstracted away and cannot be accessed in `b`.
-/
@[builtinTermParser] def «let_fun» := leading_parser:leadPrec withPosition ((symbol "let_fun " <|> "let_λ") >> letDecl) >> optSemicolon termParser
/--
`let_delayed x := v; b` is similar to `let x := v; b`, but `b` is elaborated before `v`.
-/
@[builtinTermParser] def «let_delayed» := leading_parser:leadPrec withPosition ("let_delayed " >> letDecl) >> optSemicolon termParser
-- `let`-declaration that is only included in the elaborated term if variable is still there
/--
`let`-declaration that is only included in the elaborated term if variable is still there.
It is often used when building macros.
-/
@[builtinTermParser] def «let_tmp» := leading_parser:leadPrec withPosition ("let_tmp " >> letDecl) >> optSemicolon termParser
instance : Coe (TSyntax ``letIdBinder) (TSyntax ``funBinder) where

88
stage0/stdlib/Init/Notation.c generated
View file

@ -91,6 +91,7 @@ static lean_object* l_Lean_deprecated___closed__2;
static lean_object* l_Lean_termThis___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term___x3e____1___closed__1;
static lean_object* l___aux__Init__Notation______macroRules__term___x2a____1___closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_Category_term;
static lean_object* l___aux__Init__Notation______macroRules__term___x3d_x3d____1___closed__1;
LEAN_EXPORT lean_object* l_Lean___aux__Init__Notation______macroRules__Lean__termThis__1(lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules__term___u2218____1___closed__11;
@ -118,6 +119,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x3d____2
static lean_object* l_Lean_Parser_Syntax_addPrec___closed__1;
static lean_object* l_term_x7b___x3a___x2f_x2f___x7d___closed__9;
static lean_object* l_term___x7c_x7c_____closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_Category_doElem;
static lean_object* l_Lean_Parser_Syntax_addPrio___closed__4;
static lean_object* l_term___x2d_____closed__2;
static lean_object* l_term___x5e_x5e_x5e_____closed__5;
@ -219,6 +221,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x2b____1___c
static lean_object* l___aux__Init__Notation______macroRules__term___x3d_x3d____1___closed__8;
static lean_object* l___aux__Init__Notation______macroRules__termDepIfThenElse__1___closed__6;
static lean_object* l_termMax__prec___closed__4;
LEAN_EXPORT lean_object* l_Lean_Parser_Category_prio;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__Prod__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules__stx___x2b__1___closed__1;
static lean_object* l_boolIfThenElse___closed__6;
@ -300,6 +303,7 @@ static lean_object* l_term___u2208_____closed__6;
static lean_object* l_Lean_rawStx_quot___closed__7;
static lean_object* l_termDepIfThenElse___closed__7;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___u2218____1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_Category_attr;
static lean_object* l_Lean_termThis___closed__5;
static lean_object* l_Lean___aux__Init__Notation______macroRules__term_x5b___x5d__1___closed__7;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__prioLow__1(lean_object*, lean_object*, lean_object*);
@ -776,6 +780,7 @@ static lean_object* l_term___x26_x26_x26_____closed__2;
static lean_object* l___aux__Init__Notation______macroRules__termIfThenElse__1___closed__2;
static lean_object* l_term___x3c_____closed__4;
static lean_object* l_termDepIfThenElse___closed__30;
LEAN_EXPORT lean_object* l_Lean_Parser_Category_stx;
static lean_object* l___aux__Init__Notation______macroRules__term___x26_x26____1___closed__6;
static lean_object* l___aux__Init__Notation______macroRules__term___x25____1___closed__4;
static lean_object* l_Lean_Parser_Syntax_addPrec___closed__10;
@ -805,6 +810,7 @@ LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___u2227__
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x24_x3e____1___closed__4;
LEAN_EXPORT lean_object* l_term___x2f_x5c__;
static lean_object* l_term___x2b_x2b_____closed__2;
LEAN_EXPORT lean_object* l_Lean_Parser_Category_prec;
static lean_object* l_term___x3e_____closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term_x7b___x3a___x2f_x2f___x7d__1___closed__1;
static lean_object* l_term___x25_____closed__4;
@ -872,6 +878,7 @@ static lean_object* l_termDepIfThenElse___closed__33;
static lean_object* l_term___x2a_____closed__6;
static lean_object* l_term___x3c_x2a_x3e_____closed__6;
static lean_object* l_term_x2d_____closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_Category_command;
static lean_object* l_precMin___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__boolIfThenElse__1___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term___x26_x26_x26____1___closed__4;
@ -916,6 +923,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x3c____1___c
static lean_object* l_boolIfThenElse___closed__12;
static lean_object* l___aux__Init__Notation______macroRules__term___x3d_x3d____2___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a____1___closed__5;
LEAN_EXPORT lean_object* l_Lean_Parser_Category_tactic;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__stx___x3c_x7c_x3e____1(lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules__term___x3d_x3d____1___closed__9;
static lean_object* l_stx___x2c_x2b___closed__2;
@ -1387,6 +1395,70 @@ static lean_object* l_Lean_withAnnotateTerm___closed__5;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__SeqRight__seqRight__1(lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules__term___x2a____1___closed__7;
LEAN_EXPORT lean_object* l_termWithout__expected__type__;
static lean_object* _init_l_Lean_Parser_Category_command() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Category_term() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Category_tactic() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Category_doElem() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Category_attr() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Category_stx() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Category_prio() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Category_prec() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Syntax_addPrec___closed__1() {
_start:
{
@ -37053,6 +37125,22 @@ lean_dec_ref(res);
res = initialize_Init_Coe(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Category_command = _init_l_Lean_Parser_Category_command();
lean_mark_persistent(l_Lean_Parser_Category_command);
l_Lean_Parser_Category_term = _init_l_Lean_Parser_Category_term();
lean_mark_persistent(l_Lean_Parser_Category_term);
l_Lean_Parser_Category_tactic = _init_l_Lean_Parser_Category_tactic();
lean_mark_persistent(l_Lean_Parser_Category_tactic);
l_Lean_Parser_Category_doElem = _init_l_Lean_Parser_Category_doElem();
lean_mark_persistent(l_Lean_Parser_Category_doElem);
l_Lean_Parser_Category_attr = _init_l_Lean_Parser_Category_attr();
lean_mark_persistent(l_Lean_Parser_Category_attr);
l_Lean_Parser_Category_stx = _init_l_Lean_Parser_Category_stx();
lean_mark_persistent(l_Lean_Parser_Category_stx);
l_Lean_Parser_Category_prio = _init_l_Lean_Parser_Category_prio();
lean_mark_persistent(l_Lean_Parser_Category_prio);
l_Lean_Parser_Category_prec = _init_l_Lean_Parser_Category_prec();
lean_mark_persistent(l_Lean_Parser_Category_prec);
l_Lean_Parser_Syntax_addPrec___closed__1 = _init_l_Lean_Parser_Syntax_addPrec___closed__1();
lean_mark_persistent(l_Lean_Parser_Syntax_addPrec___closed__1);
l_Lean_Parser_Syntax_addPrec___closed__2 = _init_l_Lean_Parser_Syntax_addPrec___closed__2();

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

File diff suppressed because it is too large Load diff

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

@ -38,6 +38,7 @@ static lean_object* l_Lean_Parser_Command_notationItem_parenthesizer___closed__1
static lean_object* l_Lean_Parser_Term_prec_quot___elambda__1___closed__13;
static lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__8;
static lean_object* l_Lean_Parser_Command_macroArg___elambda__1___closed__10;
static lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__14;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Parser_Command_elab__rules_formatter(lean_object*);
static lean_object* l_Lean_Parser_Command_elab__rules___elambda__1___closed__10;
static lean_object* l_Lean_Parser_Command_notationItem___closed__4;
@ -78,6 +79,7 @@ static lean_object* l_Lean_Parser_Term_prec_quot___elambda__1___closed__10;
static lean_object* l_Lean_Parser_Command_mixfixKind___closed__2;
static lean_object* l_Lean_Parser_Syntax_atom___closed__6;
static lean_object* l_Lean_Parser_Command_infixr___elambda__1___closed__3;
static lean_object* l_Lean_Parser_Command_syntaxCat_formatter___closed__7;
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Command_macro__rules_parenthesizer___closed__10;
static lean_object* l___regBuiltin_Lean_Parser_Command_mixfix_declRange___closed__7;
@ -576,6 +578,7 @@ static lean_object* l_Lean_Parser_Command_macroTailTactic_parenthesizer___closed
static lean_object* l_Lean_Parser_Command_optKind___closed__16;
static lean_object* l_Lean_Parser_Command_syntax___closed__5;
static lean_object* l_Lean_Parser_Term_prio_quot___elambda__1___closed__13;
static lean_object* l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__7;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Parser_Syntax_sepBy_parenthesizer(lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Parser_Command_syntaxAbbrev_formatter(lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Syntax___hyg_5____closed__2;
@ -1071,6 +1074,7 @@ lean_object* l_Lean_addBuiltinDeclarationRanges(lean_object*, lean_object*, lean
static lean_object* l_Lean_Parser_Command_mixfix_parenthesizer___closed__13;
LEAN_EXPORT lean_object* l_Lean_Parser_Command_optNamedName_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Term_prec_quot_parenthesizer___closed__2;
static lean_object* l_Lean_Parser_Command_syntaxCat___closed__10;
static lean_object* l_Lean_Parser_Command_mixfixKind___closed__1;
static lean_object* l_Lean_Parser_Command_macroArg___elambda__1___closed__9;
static lean_object* l___regBuiltin_Lean_Parser_Syntax_cat_declRange___closed__7;
@ -23265,22 +23269,24 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
x_2 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__8;
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;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_macro__rules___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
x_3 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__8;
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_syntaxCat___elambda__1___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9;
x_2 = l_Lean_Parser_precedence___elambda__1___closed__12;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
x_2 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9;
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;
@ -23290,8 +23296,8 @@ static lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_precedence___elambda__1___closed__11;
x_2 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__10;
x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__10;
x_2 = l_Lean_Parser_precedence___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);
@ -23302,9 +23308,11 @@ static lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_precedence___elambda__1___lambda__1___closed__1;
x_2 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__5;
x_3 = lean_string_append(x_1, x_2);
x_1 = l_Lean_Parser_precedence___elambda__1___closed__11;
x_2 = l_Lean_Parser_Command_syntaxCat___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;
}
}
@ -23312,7 +23320,17 @@ static lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__12;
x_1 = l_Lean_Parser_precedence___elambda__1___lambda__1___closed__1;
x_2 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__5;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__13;
x_2 = l_Lean_Parser_precedence___elambda__1___lambda__1___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
@ -23321,172 +23339,193 @@ return x_3;
LEAN_EXPORT lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint32_t x_10; uint32_t x_11; uint8_t x_12;
lean_object* x_3; 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; uint32_t x_12; uint32_t x_13; uint8_t x_14;
x_3 = l_Lean_Parser_Command_catBehavior;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
x_5 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__3;
x_5 = l_Lean_Parser_Command_macro__rules___elambda__1___closed__4;
x_6 = lean_ctor_get(x_5, 1);
lean_inc(x_6);
x_7 = lean_ctor_get(x_1, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_7, 0);
x_7 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__3;
x_8 = lean_ctor_get(x_7, 1);
lean_inc(x_8);
lean_dec(x_7);
x_9 = lean_ctor_get(x_2, 2);
x_9 = lean_ctor_get(x_1, 0);
lean_inc(x_9);
x_10 = lean_string_utf8_get(x_8, x_9);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
lean_dec(x_9);
x_11 = 36;
x_12 = lean_uint32_dec_eq(x_10, x_11);
if (x_12 == 0)
x_11 = lean_ctor_get(x_2, 2);
lean_inc(x_11);
x_12 = lean_string_utf8_get(x_10, x_11);
lean_dec(x_11);
x_13 = 36;
x_14 = lean_uint32_dec_eq(x_12, x_13);
if (x_14 == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17;
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19;
lean_dec(x_8);
x_15 = lean_unsigned_to_nat(1024u);
x_16 = l_Lean_Parser_checkPrecFn(x_15, x_1, x_2);
x_17 = lean_ctor_get(x_16, 4);
lean_inc(x_17);
x_18 = lean_box(0);
x_19 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(x_17, x_18);
lean_dec(x_17);
if (x_19 == 0)
{
lean_dec(x_10);
lean_dec(x_6);
x_13 = lean_unsigned_to_nat(1024u);
x_14 = l_Lean_Parser_checkPrecFn(x_13, x_1, x_2);
x_15 = lean_ctor_get(x_14, 4);
lean_inc(x_15);
x_16 = lean_box(0);
x_17 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(x_15, x_16);
lean_dec(x_15);
if (x_17 == 0)
{
lean_dec(x_8);
lean_dec(x_4);
lean_dec(x_1);
return x_14;
return x_16;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint32_t x_24; uint32_t x_25; uint8_t x_26; lean_object* x_27;
x_18 = lean_ctor_get(x_14, 0);
lean_inc(x_18);
x_19 = lean_array_get_size(x_18);
lean_dec(x_18);
x_20 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__5;
x_21 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__13;
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24; lean_object* x_25;
x_20 = lean_ctor_get(x_16, 0);
lean_inc(x_20);
x_21 = lean_array_get_size(x_20);
lean_dec(x_20);
lean_inc(x_1);
x_22 = l_Lean_Parser_symbolFnAux(x_20, x_21, x_1, x_14);
x_23 = lean_ctor_get(x_22, 2);
x_22 = lean_apply_2(x_6, x_1, x_16);
x_23 = lean_ctor_get(x_22, 4);
lean_inc(x_23);
x_24 = lean_string_utf8_get(x_8, x_23);
x_24 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(x_23, x_18);
lean_dec(x_23);
lean_dec(x_8);
x_25 = 37;
x_26 = lean_uint32_dec_eq(x_24, x_25);
if (x_26 == 0)
if (x_24 == 0)
{
x_27 = x_22;
goto block_49;
}
else
{
lean_object* x_50;
lean_inc(x_1);
x_50 = l_Lean_Parser_tokenAntiquotFn(x_1, x_22);
x_27 = x_50;
goto block_49;
}
block_49:
{
lean_object* x_28; uint8_t x_29;
x_28 = lean_ctor_get(x_27, 4);
lean_inc(x_28);
x_29 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(x_28, x_16);
lean_dec(x_28);
if (x_29 == 0)
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33;
lean_dec(x_10);
lean_dec(x_4);
x_30 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
x_31 = l_Lean_Parser_ParserState_mkNode(x_27, x_30, x_19);
x_32 = lean_ctor_get(x_31, 4);
lean_inc(x_32);
x_33 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(x_32, x_16);
lean_dec(x_32);
if (x_33 == 0)
{
lean_dec(x_1);
return x_31;
x_25 = x_22;
goto block_31;
}
else
{
lean_object* x_34;
x_34 = l_Lean_Parser_setLhsPrecFn(x_13, x_1, x_31);
lean_dec(x_1);
return x_34;
}
}
else
{
lean_object* x_35; lean_object* x_36; uint8_t x_37;
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; uint32_t x_36; uint32_t x_37; uint8_t x_38;
x_32 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__5;
x_33 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__14;
lean_inc(x_1);
x_35 = l_Lean_Parser_ident___elambda__1(x_1, x_27);
x_36 = lean_ctor_get(x_35, 4);
lean_inc(x_36);
x_37 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(x_36, x_16);
lean_dec(x_36);
if (x_37 == 0)
x_34 = l_Lean_Parser_symbolFnAux(x_32, x_33, x_1, x_22);
x_35 = lean_ctor_get(x_34, 2);
lean_inc(x_35);
x_36 = lean_string_utf8_get(x_10, x_35);
lean_dec(x_35);
lean_dec(x_10);
x_37 = 37;
x_38 = lean_uint32_dec_eq(x_36, x_37);
if (x_38 == 0)
{
lean_object* x_39; uint8_t x_40;
x_39 = lean_ctor_get(x_34, 4);
lean_inc(x_39);
x_40 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(x_39, x_18);
lean_dec(x_39);
if (x_40 == 0)
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; uint8_t x_41;
lean_dec(x_4);
x_38 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
x_39 = l_Lean_Parser_ParserState_mkNode(x_35, x_38, x_19);
x_40 = lean_ctor_get(x_39, 4);
lean_inc(x_40);
x_41 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(x_40, x_16);
lean_dec(x_40);
if (x_41 == 0)
{
lean_dec(x_1);
return x_39;
x_25 = x_34;
goto block_31;
}
else
{
lean_object* x_42;
x_42 = l_Lean_Parser_setLhsPrecFn(x_13, x_1, x_39);
lean_dec(x_1);
return x_42;
}
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; uint8_t x_47;
lean_object* x_41; lean_object* x_42; uint8_t x_43;
lean_inc(x_1);
x_43 = lean_apply_2(x_4, x_1, x_35);
x_44 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
x_45 = l_Lean_Parser_ParserState_mkNode(x_43, x_44, x_19);
x_41 = l_Lean_Parser_ident___elambda__1(x_1, x_34);
x_42 = lean_ctor_get(x_41, 4);
lean_inc(x_42);
x_43 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(x_42, x_18);
lean_dec(x_42);
if (x_43 == 0)
{
lean_dec(x_4);
x_25 = x_41;
goto block_31;
}
else
{
lean_object* x_44;
lean_inc(x_1);
x_44 = lean_apply_2(x_4, x_1, x_41);
x_25 = x_44;
goto block_31;
}
}
}
else
{
lean_object* x_45; lean_object* x_46; uint8_t x_47;
lean_inc(x_1);
x_45 = l_Lean_Parser_tokenAntiquotFn(x_1, x_34);
x_46 = lean_ctor_get(x_45, 4);
lean_inc(x_46);
x_47 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(x_46, x_16);
x_47 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(x_46, x_18);
lean_dec(x_46);
if (x_47 == 0)
{
lean_dec(x_1);
return x_45;
}
else
{
lean_object* x_48;
x_48 = l_Lean_Parser_setLhsPrecFn(x_13, x_1, x_45);
lean_dec(x_1);
return x_48;
}
}
}
}
}
}
else
{
lean_object* x_51; uint8_t x_52; lean_object* x_53;
lean_dec(x_8);
lean_dec(x_4);
x_51 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__11;
x_52 = 1;
x_53 = l_Lean_Parser_orelseFnCore(x_6, x_51, x_52, x_1, x_2);
return x_53;
x_25 = x_45;
goto block_31;
}
else
{
lean_object* x_48; lean_object* x_49; uint8_t x_50;
lean_inc(x_1);
x_48 = l_Lean_Parser_ident___elambda__1(x_1, x_45);
x_49 = lean_ctor_get(x_48, 4);
lean_inc(x_49);
x_50 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(x_49, x_18);
lean_dec(x_49);
if (x_50 == 0)
{
lean_dec(x_4);
x_25 = x_48;
goto block_31;
}
else
{
lean_object* x_51;
lean_inc(x_1);
x_51 = lean_apply_2(x_4, x_1, x_48);
x_25 = x_51;
goto block_31;
}
}
}
}
block_31:
{
lean_object* x_26; lean_object* x_27; lean_object* x_28; uint8_t x_29;
x_26 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
x_27 = l_Lean_Parser_ParserState_mkNode(x_25, x_26, x_21);
x_28 = lean_ctor_get(x_27, 4);
lean_inc(x_28);
x_29 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_828____at_Lean_Parser_ParserState_hasError___spec__1(x_28, x_18);
lean_dec(x_28);
if (x_29 == 0)
{
lean_dec(x_1);
return x_27;
}
else
{
lean_object* x_30;
x_30 = l_Lean_Parser_setLhsPrecFn(x_15, x_1, x_27);
lean_dec(x_1);
return x_30;
}
}
}
}
else
{
lean_object* x_52; uint8_t x_53; lean_object* x_54;
lean_dec(x_10);
lean_dec(x_6);
lean_dec(x_4);
x_52 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__12;
x_53 = 1;
x_54 = l_Lean_Parser_orelseFnCore(x_8, x_52, x_53, x_1, x_2);
return x_54;
}
}
}
@ -23526,20 +23565,22 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
x_2 = l_Lean_Parser_Command_syntaxCat___closed__3;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_macro__rules___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Command_syntaxCat___closed__3;
x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_syntaxCat___closed__4;
x_2 = l_Lean_Parser_epsilonInfo;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
x_2 = l_Lean_Parser_Command_syntaxCat___closed__4;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
@ -23547,8 +23588,8 @@ static lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Command_syntaxCat___closed__5;
x_1 = l_Lean_Parser_Command_syntaxCat___closed__5;
x_2 = l_Lean_Parser_epsilonInfo;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
@ -23556,16 +23597,26 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Command_syntaxCat___closed__6;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__3;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Command_syntaxCat___closed__6;
x_3 = l_Lean_Parser_Command_syntaxCat___closed__7;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__8() {
static lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__9() {
_start:
{
lean_object* x_1;
@ -23573,12 +23624,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_syntaxCat___elambda__1),
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__9() {
static lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_syntaxCat___closed__7;
x_2 = l_Lean_Parser_Command_syntaxCat___closed__8;
x_1 = l_Lean_Parser_Command_syntaxCat___closed__8;
x_2 = l_Lean_Parser_Command_syntaxCat___closed__9;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -23589,7 +23640,7 @@ static lean_object* _init_l_Lean_Parser_Command_syntaxCat() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Command_syntaxCat___closed__9;
x_1 = l_Lean_Parser_Command_syntaxCat___closed__10;
return x_1;
}
}
@ -23623,7 +23674,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(77u);
x_2 = lean_unsigned_to_nat(101u);
x_2 = lean_unsigned_to_nat(124u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -23637,7 +23688,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Parser_Command_syntaxCat_declRange___closed__1;
x_2 = lean_unsigned_to_nat(24u);
x_3 = l___regBuiltin_Lean_Parser_Command_syntaxCat_declRange___closed__2;
x_4 = lean_unsigned_to_nat(101u);
x_4 = lean_unsigned_to_nat(124u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -24023,10 +24074,22 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Command_syntaxCat_formatter___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_macro__rules_formatter___closed__3;
x_2 = l_Lean_Parser_Command_syntaxCat_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);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Command_syntaxCat_formatter___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_syntaxCat___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Command_syntaxCat_formatter___closed__5;
x_3 = l_Lean_Parser_Command_syntaxCat_formatter___closed__6;
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);
@ -24039,7 +24102,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Command_syntaxCat_formatter___closed__1;
x_7 = l_Lean_Parser_Command_syntaxCat_formatter___closed__6;
x_7 = l_Lean_Parser_Command_syntaxCat_formatter___closed__7;
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;
}
@ -24389,10 +24452,22 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_macro__rules_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__5;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 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_syntaxCat_parenthesizer___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_syntaxCat___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__5;
x_3 = l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__6;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -24405,7 +24480,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__1;
x_7 = l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__6;
x_7 = l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__7;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_withAntiquot_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -33364,6 +33439,8 @@ l_Lean_Parser_Command_syntaxCat___elambda__1___closed__12 = _init_l_Lean_Parser_
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___elambda__1___closed__12);
l_Lean_Parser_Command_syntaxCat___elambda__1___closed__13 = _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__13();
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___elambda__1___closed__13);
l_Lean_Parser_Command_syntaxCat___elambda__1___closed__14 = _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__14();
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___elambda__1___closed__14);
l_Lean_Parser_Command_syntaxCat___closed__1 = _init_l_Lean_Parser_Command_syntaxCat___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___closed__1);
l_Lean_Parser_Command_syntaxCat___closed__2 = _init_l_Lean_Parser_Command_syntaxCat___closed__2();
@ -33382,6 +33459,8 @@ l_Lean_Parser_Command_syntaxCat___closed__8 = _init_l_Lean_Parser_Command_syntax
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___closed__8);
l_Lean_Parser_Command_syntaxCat___closed__9 = _init_l_Lean_Parser_Command_syntaxCat___closed__9();
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___closed__9);
l_Lean_Parser_Command_syntaxCat___closed__10 = _init_l_Lean_Parser_Command_syntaxCat___closed__10();
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___closed__10);
l_Lean_Parser_Command_syntaxCat = _init_l_Lean_Parser_Command_syntaxCat();
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat);
res = l___regBuiltin_Lean_Parser_Command_syntaxCat(lean_io_mk_world());
@ -33454,6 +33533,8 @@ l_Lean_Parser_Command_syntaxCat_formatter___closed__5 = _init_l_Lean_Parser_Comm
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat_formatter___closed__5);
l_Lean_Parser_Command_syntaxCat_formatter___closed__6 = _init_l_Lean_Parser_Command_syntaxCat_formatter___closed__6();
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat_formatter___closed__6);
l_Lean_Parser_Command_syntaxCat_formatter___closed__7 = _init_l_Lean_Parser_Command_syntaxCat_formatter___closed__7();
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat_formatter___closed__7);
l___regBuiltin_Lean_Parser_Command_syntaxCat_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Command_syntaxCat_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Command_syntaxCat_formatter___closed__1);
l___regBuiltin_Lean_Parser_Command_syntaxCat_formatter___closed__2 = _init_l___regBuiltin_Lean_Parser_Command_syntaxCat_formatter___closed__2();
@ -33511,6 +33592,8 @@ l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__5 = _init_l_Lean_Parser_
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__5);
l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__6 = _init_l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__6();
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__6);
l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__7 = _init_l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__7();
lean_mark_persistent(l_Lean_Parser_Command_syntaxCat_parenthesizer___closed__7);
l___regBuiltin_Lean_Parser_Command_syntaxCat_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Command_syntaxCat_parenthesizer___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Command_syntaxCat_parenthesizer___closed__1);
l___regBuiltin_Lean_Parser_Command_syntaxCat_parenthesizer___closed__2 = _init_l___regBuiltin_Lean_Parser_Command_syntaxCat_parenthesizer___closed__2();

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

File diff suppressed because it is too large Load diff