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-13 16:09:34 -08:00
parent e98507023e
commit a3f5db0900
11 changed files with 4067 additions and 1306 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -86,7 +86,7 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
@[builtinCommandParser] def exit := parser! "#exit"
@[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
@[builtinCommandParser] def «init_quot» := parser! "init_quot"
@[builtinCommandParser] def «set_option» := parser! "set_option " >> ident >> (symbolOrIdent "true" <|> symbolOrIdent "false" <|> strLit <|> numLit)
@[builtinCommandParser] def «set_option» := parser! "set_option " >> ident >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit)
@[builtinCommandParser] def «attribute» := parser! optional "local " >> "attribute " >> "[" >> sepBy1 attrInstance ", " >> "]" >> many1 ident
@[builtinCommandParser] def «export» := parser! "export " >> ident >> "(" >> many1 ident >> ")"
def openHiding := parser! try (ident >> "hiding") >> many1 ident
@ -98,7 +98,7 @@ def openSimple := parser! many1 ident
@[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident
/- Lean3 command declaration commands -/
def maxPrec := parser! symbolOrIdent "max"
def maxPrec := parser! nonReservedSymbol "max"
def precedenceLit : Parser := numLit <|> maxPrec
def «precedence» := parser! " : " >> precedenceLit
def quotedSymbolPrec := parser! quotedSymbol >> optional «precedence»

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

@ -21,8 +21,8 @@ categoryParser `level rbp
namespace Level
@[builtinLevelParser] def paren := parser! symbol "(" appPrec >> levelParser >> ")"
@[builtinLevelParser] def max := parser! symbolOrIdent "max" >> many1 (levelParser appPrec)
@[builtinLevelParser] def imax := parser! symbolOrIdent "imax" >> many1 (levelParser appPrec)
@[builtinLevelParser] def max := parser! nonReservedSymbol "max " >> many1 (levelParser appPrec)
@[builtinLevelParser] def imax := parser! "imax" >> many1 (levelParser appPrec)
@[builtinLevelParser] def hole := parser! "_"
@[builtinLevelParser] def num := parser! numLit
@[builtinLevelParser] def ident := parser! ident

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

@ -897,7 +897,7 @@ symbolAux sym lbp
For example, the universe `max` Function is parsed using this combinator so that
it can still be used as an identifier outside of universes (but registering it
as a token in a Term Syntax would not break the universe Parser). -/
def symbolOrIdentFnAux (sym : String) (errorMsg : String) : BasicParserFn :=
def nonReservedSymbolFnAux (sym : String) (errorMsg : String) : BasicParserFn :=
fun c s =>
let startPos := s.pos;
let s := tokenFn c s;
@ -914,16 +914,16 @@ fun c s =>
s.mkErrorAt errorMsg startPos
| _ => s.mkErrorAt errorMsg startPos
@[inline] def symbolOrIdentFn (sym : String) : BasicParserFn :=
symbolOrIdentFnAux sym ("'" ++ sym ++ "'")
@[inline] def nonReservedSymbolFn (sym : String) : BasicParserFn :=
nonReservedSymbolFnAux sym ("'" ++ sym ++ "'")
def symbolOrIdentInfo (sym : String) : ParserInfo :=
def nonReservedSymbolInfo (sym : String) : ParserInfo :=
{ firstTokens := FirstTokens.tokens [ { val := sym }, { val := "ident" } ] }
@[inline] def symbolOrIdent {k : ParserKind} (sym : String) : Parser k :=
@[inline] def nonReservedSymbol {k : ParserKind} (sym : String) : Parser k :=
let sym := sym.trim;
{ info := symbolOrIdentInfo sym,
fn := fun _ => symbolOrIdentFn sym }
{ info := nonReservedSymbolInfo sym,
fn := fun _ => nonReservedSymbolFn sym }
partial def strAux (sym : String) (errorMsg : String) : Nat → BasicParserFn
| j, c, s =>
@ -1247,26 +1247,32 @@ match stx with
| some (Syntax.node k _) => if k == numLitKind || k == charLitKind || k == strLitKind || k == fieldIdxKind then (s, appPrec) else (s, 0)
| _ => (s, 0)
def indexed {α : Type} (map : TokenMap α) (c : ParserContext) (s : ParserState) : ParserState × List α :=
def indexed {α : Type} (map : TokenMap α) (c : ParserContext) (s : ParserState) (leadingIdentAsSymbol : Bool) : ParserState × List α :=
let (s, stx) := peekToken c s;
let find (n : Name) : ParserState × List α :=
match map.find n with
| some as => (s, as)
| _ => (s, []);
match stx with
| some (Syntax.atom _ sym) => find (mkNameSimple sym)
| some (Syntax.ident _ _ _ _) => find `ident
| some (Syntax.node k _) => find k
| _ => (s, [])
| some (Syntax.atom _ sym) => find (mkNameSimple sym)
| some (Syntax.ident _ _ val _) =>
if leadingIdentAsSymbol then
match map.find val with
| some as => (s, as)
| none => find `ident
else
find `ident
| some (Syntax.node k _) => find k
| _ => (s, [])
private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=
if s.stackSize == iniSz + 1 then s
else s.mkNode nullKind iniSz -- throw error instead?
def leadingParser (kind : Name) (tables : ParsingTables) : ParserFn leading :=
def leadingParser (kind : Name) (tables : ParsingTables) (leadingIdentAsSymbol : Bool) : ParserFn leading :=
fun a c s =>
let iniSz := s.stackSize;
let (s, ps) := indexed tables.leadingTable c s;
let (s, ps) := indexed tables.leadingTable c s leadingIdentAsSymbol;
if ps.isEmpty then
s.mkError (toString kind)
else
@ -1282,8 +1288,9 @@ partial def trailingLoop (tables : ParsingTables) (rbp : Nat) (c : ParserContext
let (s, lbp) := currLbp left c s;
if rbp ≥ lbp then s.pushSyntax left
else
let iniSz := s.stackSize;
let (s, ps) := indexed tables.trailingTable c s;
let iniSz := s.stackSize;
let identAsSymbol := false;
let (s, ps) := indexed tables.trailingTable c s identAsSymbol;
if ps.isEmpty && tables.trailingParsers.isEmpty then
s.pushSyntax left -- no available trailing parser
else
@ -1295,9 +1302,9 @@ partial def trailingLoop (tables : ParsingTables) (rbp : Nat) (c : ParserContext
let s := s.popSyntax;
trailingLoop left s
def prattParser (kind : Name) (tables : ParsingTables) : ParserFn leading :=
def prattParser (kind : Name) (tables : ParsingTables) (leadingIdentAsSymbol : Bool) : ParserFn leading :=
fun rbp c s =>
let s := leadingParser kind tables rbp c s;
let s := leadingParser kind tables leadingIdentAsSymbol rbp c s;
if s.hasError then s
else
let left := s.stxStack.back;
@ -1331,7 +1338,11 @@ def mkBuiltinTokenTable : IO (IO.Ref TokenTable) := IO.mkRef {}
def mkBuiltinSyntaxNodeKindSetRef : IO (IO.Ref SyntaxNodeKindSet) := IO.mkRef {}
@[init mkBuiltinSyntaxNodeKindSetRef] constant builtinSyntaxNodeKindSetRef : IO.Ref SyntaxNodeKindSet := arbitrary _
abbrev ParserCategories := PersistentHashMap Name ParsingTables
structure ParserCategory :=
(tables : ParsingTables)
(leadingIdentAsSymbol : Bool := false)
abbrev ParserCategories := PersistentHashMap Name ParserCategory
def mkBuiltinParserCategories : IO (IO.Ref ParserCategories) := IO.mkRef {}
@[init mkBuiltinParserCategories] constant builtinParserCategoriesRef : IO.Ref ParserCategories := arbitrary _
@ -1339,27 +1350,27 @@ def mkBuiltinParserCategories : IO (IO.Ref ParserCategories) := IO.mkRef {}
private def throwParserCategoryAlreadyDefined {α} (catName : Name) : ExceptT String Id α :=
throw ("parser category '" ++ toString catName ++ "' has already been defined")
private def addParserCategoryCore (categories : ParserCategories) (catName : Name) : Except String ParserCategories :=
private def addParserCategoryCore (categories : ParserCategories) (catName : Name) (leadingIdentAsSymbol : Bool) : Except String ParserCategories :=
if categories.contains catName then
throwParserCategoryAlreadyDefined catName
else
pure $ categories.insert catName {}
pure $ categories.insert catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol }
private def addBuiltinParserCategory (catName : Name) : IO Unit := do
private def addBuiltinParserCategory (catName : Name) (leadingIdentAsSymbol : Bool) : IO Unit := do
categories ← builtinParserCategoriesRef.get;
categories ← IO.ofExcept $ addParserCategoryCore categories catName;
categories ← IO.ofExcept $ addParserCategoryCore categories catName leadingIdentAsSymbol;
builtinParserCategoriesRef.set categories
inductive ParserExtensionOleanEntry
| token (val : TokenConfig) : ParserExtensionOleanEntry
| kind (val : SyntaxNodeKind) : ParserExtensionOleanEntry
| category (catName : Name)
| category (catName : Name) (leadingIdentAsSymbol : Bool)
| parser (catName : Name) (declName : Name) : ParserExtensionOleanEntry
inductive ParserExtensionEntry
| token (val : TokenConfig) : ParserExtensionEntry
| kind (val : SyntaxNodeKind) : ParserExtensionEntry
| category (catName : Name)
| category (catName : Name) (leadingIdentAsSymbol : Bool)
| parser (catName : Name) (declName : Name) (k : ParserKind) (p : Parser k) : ParserExtensionEntry
structure ParserExtensionState :=
@ -1401,11 +1412,11 @@ throw ("unknown parser category '" ++ toString catName ++ "'")
def addLeadingParser (categories : ParserCategories) (catName : Name) (parserName : Name) (p : Parser) : Except String ParserCategories :=
let addTokens (tks : List TokenConfig) : Except String ParserCategories :=
match categories.find? catName with
| none => throwUnknownParserCategory catName
| some tables =>
| none => throwUnknownParserCategory catName
| some cat =>
let tks := tks.map $ fun tk => mkNameSimple tk.val;
let tables := tks.eraseDups.foldl (fun (tables : ParsingTables) tk => { leadingTable := tables.leadingTable.insert tk p, .. tables }) tables;
pure (categories.insert catName tables);
let tables := tks.eraseDups.foldl (fun (tables : ParsingTables) tk => { leadingTable := tables.leadingTable.insert tk p, .. tables }) cat.tables;
pure $ categories.insert catName { tables := tables, .. cat };
match p.info.firstTokens with
| FirstTokens.tokens tks => addTokens tks
| FirstTokens.optTokens tks => addTokens tks
@ -1422,8 +1433,8 @@ match p.info.firstTokens with
def addTrailingParser (categories : ParserCategories) (catName : Name) (p : TrailingParser) : Except String ParserCategories :=
match categories.find? catName with
| none => throwUnknownParserCategory catName
| some tables => pure $ categories.insert catName (addTrailingParserAux tables p)
| none => throwUnknownParserCategory catName
| some cat => pure $ categories.insert catName { tables := addTrailingParserAux cat.tables p, .. cat }
def addParser {k} (categories : ParserCategories) (catName : Name) (declName : Name) (p : Parser k) : Except String ParserCategories :=
match k, p with
@ -1461,9 +1472,10 @@ match e with
| _ => unreachable!
| ParserExtensionEntry.kind k =>
{ kinds := s.kinds.insert k, newEntries := ParserExtensionOleanEntry.kind k :: s.newEntries, .. s }
| ParserExtensionEntry.category catName =>
| ParserExtensionEntry.category catName leadingIdentAsSymbol =>
if s.categories.contains catName then s
else { categories := s.categories.insert catName {}, newEntries := ParserExtensionOleanEntry.category catName :: s.newEntries, .. s }
else { categories := s.categories.insert catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol },
newEntries := ParserExtensionOleanEntry.category catName leadingIdentAsSymbol :: s.newEntries, .. s }
| ParserExtensionEntry.parser catName declName _ parser =>
match addParser s.categories catName declName parser with
| Except.ok categories => { categories := categories, newEntries := ParserExtensionOleanEntry.parser catName declName :: s.newEntries, .. s }
@ -1526,8 +1538,8 @@ es.foldlM
pure { tokens := tokens, .. s }
| ParserExtensionOleanEntry.kind k =>
pure { kinds := s.kinds.insert k, .. s }
| ParserExtensionOleanEntry.category catName => do
categories ← IO.ofExcept (addParserCategoryCore s.categories catName);
| ParserExtensionOleanEntry.category catName leadingIdentAsSymbol => do
categories ← IO.ofExcept (addParserCategoryCore s.categories catName leadingIdentAsSymbol);
pure { categories := categories, .. s }
| ParserExtensionOleanEntry.parser catName declName =>
match mkParserOfConstant env s.categories declName with
@ -1555,18 +1567,18 @@ constant parserExtension : ParserExtension := arbitrary _
def isParserCategory (env : Environment) (catName : Name) : Bool :=
(parserExtension.getState env).categories.contains catName
def addParserCategory (env : Environment) (catName : Name) : Except String Environment := do
def addParserCategory (env : Environment) (catName : Name) (leadingIdentAsSymbol : Bool) : Except String Environment := do
if isParserCategory env catName then
throwParserCategoryAlreadyDefined catName
else
pure $ parserExtension.addEntry env $ ParserExtensionEntry.category catName
pure $ parserExtension.addEntry env $ ParserExtensionEntry.category catName leadingIdentAsSymbol
def categoryParserFnImpl (catName : Name) : ParserFn leading :=
fun rbp ctx s =>
let categories := (parserExtension.getState ctx.env).categories;
match categories.find? catName with
| some tables => prattParser catName tables rbp ctx s
| none => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'")
| some cat => prattParser catName cat.tables cat.leadingIdentAsSymbol rbp ctx s
| none => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'")
@[init] def setCategoryParserFnRef : IO Unit :=
categoryParserFnRef.set categoryParserFnImpl
@ -1607,11 +1619,11 @@ def mkParserState (input : String) : ParserState :=
def runParserCategory (env : Environment) (catName : Name) (input : String) (fileName := "<input>") : Except String Syntax :=
let categories := (parserExtension.getState env).categories;
match categories.find? catName with
| some tables =>
| some cat =>
let c := mkParserContext env (mkInputContext input fileName);
let s := mkParserState input;
let s := whitespace c s;
let s := prattParser catName tables (0 : Nat) c s;
let s := prattParser catName cat.tables cat.leadingIdentAsSymbol (0 : Nat) c s;
if s.hasError then
Except.error (s.toErrorMsg c)
else
@ -1652,8 +1664,8 @@ match env.find? declName with
/-
The parsing tables for builtin parsers are "stored" in the extracted source code.
-/
def registerBuiltinParserAttribute (attrName : Name) (catName : Name) : IO Unit := do
addBuiltinParserCategory catName;
def registerBuiltinParserAttribute (attrName : Name) (catName : Name) (leadingIdentAsSymbol := false) : IO Unit := do
addBuiltinParserCategory catName leadingIdentAsSymbol;
registerBuiltinAttribute {
name := attrName,
descr := "Builtin parser",
@ -1699,8 +1711,8 @@ registerAttributeImplBuilder `parserAttr $ fun args =>
| [DataValue.ofName attrName, DataValue.ofName catName] => pure $ mkParserAttributeImpl attrName catName
| _ => throw ("invalid parser attribute implementation builder arguments")
def registerParserCategory (env : Environment) (attrName : Name) (catName : Name) : IO Environment := do
env ← IO.ofExcept $ addParserCategory env catName;
def registerParserCategory (env : Environment) (attrName : Name) (catName : Name) (leadingIdentAsSymbol := false) : IO Environment := do
env ← IO.ofExcept $ addParserCategory env catName leadingIdentAsSymbol;
registerAttributeOfBuilder env `parserAttr [DataValue.ofName attrName, DataValue.ofName catName]
-- declare `termParser` here since it is used everywhere via antiquotations

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

@ -18,14 +18,32 @@ registerBuiltinDynamicParserAttribute `tacticParser `tactic
@[inline] def tacticParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
categoryParser `tactic rbp
def tacticSeq {k : ParserKind} : Parser k :=
sepBy1 tacticParser "; " true
namespace Tactic
def tacticSymbolInfo (sym : String) : ParserInfo :=
{ firstTokens := FirstTokens.tokens [ { val := sym } ] }
@[inline] def tacticSymbol {k : ParserKind} (sym : String) : Parser k :=
let sym := sym.trim;
{ info := tacticSymbolInfo sym,
fn := fun _ => nonReservedSymbolFn sym }
@[builtinTacticParser] def «intro» := parser! tacticSymbol "intro " >> optional ident
@[builtinTacticParser] def «intros» := parser! tacticSymbol "intros " >> many ident
@[builtinTacticParser] def «assumption» := parser! tacticSymbol "assumption"
@[builtinTacticParser] def «apply» := parser! tacticSymbol "apply " >> termParser
@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> tacticSeq >> "end"
@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> tacticSeq >> "}"
@[builtinTacticParser] def orelse := tparser! infixR " <|> " 2
end Tactic
namespace Term
@[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> tacticParser >> "end"
@[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> tacticSeq >> "end"
end Term

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

@ -9,7 +9,6 @@ import Init.Lean.Parser.Level
namespace Lean
namespace Parser
namespace Term
/- Helper functions for defining simple parsers -/
def unicodeInfixR (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
@ -24,6 +23,8 @@ pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser lbp
def infixL (sym : String) (lbp : Nat) : TrailingParser :=
pushLeading >> symbol sym lbp >> termParser lbp
namespace Term
/- Built-in parsers -/
-- NOTE: `checkNoWsBefore` should be used *before* `parser!` so that it is also applied to the generated
-- antiquotation.

87
stage0/stdlib/Init/Lean/Elab/Command.c
View file

@ -399,7 +399,7 @@ lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSynth___closed__1;
lean_object* l___private_Init_Lean_Elab_Command_2__getState(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Command_universe___elambda__1___closed__2;
lean_object* l_Lean_Elab_Command_elabCommandAux___closed__2;
lean_object* l_Lean_Parser_registerParserCategory(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_registerParserCategory(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabOpen___closed__2;
extern lean_object* l_Bool_HasRepr___closed__1;
lean_object* l_Lean_Meta_synthInstance(lean_object*, lean_object*, lean_object*);
@ -18689,79 +18689,80 @@ lean_inc(x_2);
x_8 = l_Lean_Elab_Command_getEnv(x_2, x_3);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_8, 1);
lean_inc(x_10);
lean_dec(x_8);
x_11 = l_Lean_Parser_registerParserCategory(x_9, x_7, x_5, x_10);
if (lean_obj_tag(x_11) == 0)
x_11 = 0;
x_12 = l_Lean_Parser_registerParserCategory(x_9, x_7, x_5, x_11, x_10);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l_Lean_Elab_Command_setEnv(x_12, x_2, x_13);
return x_14;
x_14 = lean_ctor_get(x_12, 1);
lean_inc(x_14);
lean_dec(x_12);
x_15 = l_Lean_Elab_Command_setEnv(x_13, x_2, x_14);
return x_15;
}
else
{
uint8_t x_15;
x_15 = !lean_is_exclusive(x_11);
if (x_15 == 0)
uint8_t x_16;
x_16 = !lean_is_exclusive(x_12);
if (x_16 == 0)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_16 = lean_ctor_get(x_11, 0);
x_17 = l___private_Init_Lean_Elab_Command_1__ioErrorToMessage(x_2, x_1, x_16);
x_18 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_11, 0, x_18);
return x_11;
lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_17 = lean_ctor_get(x_12, 0);
x_18 = l___private_Init_Lean_Elab_Command_1__ioErrorToMessage(x_2, x_1, x_17);
x_19 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set(x_12, 0, x_19);
return x_12;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_19 = lean_ctor_get(x_11, 0);
x_20 = lean_ctor_get(x_11, 1);
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_20 = lean_ctor_get(x_12, 0);
x_21 = lean_ctor_get(x_12, 1);
lean_inc(x_21);
lean_inc(x_20);
lean_inc(x_19);
lean_dec(x_11);
x_21 = l___private_Init_Lean_Elab_Command_1__ioErrorToMessage(x_2, x_1, x_19);
x_22 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_22, 0, x_21);
x_23 = lean_alloc_ctor(1, 2, 0);
lean_dec(x_12);
x_22 = l___private_Init_Lean_Elab_Command_1__ioErrorToMessage(x_2, x_1, x_20);
x_23 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_20);
return x_23;
x_24 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_21);
return x_24;
}
}
}
else
{
uint8_t x_24;
uint8_t x_25;
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_2);
x_24 = !lean_is_exclusive(x_8);
if (x_24 == 0)
x_25 = !lean_is_exclusive(x_8);
if (x_25 == 0)
{
return x_8;
}
else
{
lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_25 = lean_ctor_get(x_8, 0);
x_26 = lean_ctor_get(x_8, 1);
lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_26 = lean_ctor_get(x_8, 0);
x_27 = lean_ctor_get(x_8, 1);
lean_inc(x_27);
lean_inc(x_26);
lean_inc(x_25);
lean_dec(x_8);
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_25);
lean_ctor_set(x_27, 1, x_26);
return x_27;
x_28 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_28, 0, x_26);
lean_ctor_set(x_28, 1, x_27);
return x_28;
}
}
}

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

@ -114,7 +114,6 @@ lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_stxQuot___elambd
extern lean_object* l_Lean_Parser_Term_haveAssign___closed__2;
lean_object* l_Lean_Parser_Command_structExplicitBinder___closed__11;
lean_object* l_Lean_Parser_Command_declId___elambda__1___closed__3;
extern lean_object* l_Lean_Parser_Level_max___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_openRenaming;
lean_object* l_Lean_Parser_Command_variables___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__3;
@ -151,6 +150,7 @@ lean_object* l_Lean_Parser_Command_infixr___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_unsafe___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_declaration___closed__7;
lean_object* l_Lean_Parser_Command_maxPrec___closed__5;
lean_object* l___regBuiltinParser_Lean_Parser_Command_attribute(lean_object*);
lean_object* l_Lean_Parser_Command_attributes___closed__7;
lean_object* l_Lean_Parser_Command_section___closed__5;
@ -255,7 +255,6 @@ lean_object* l_Lean_Parser_Command_classInductive___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_abbrev___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_notation___closed__10;
lean_object* l_Lean_Parser_Command_openRenaming___closed__4;
lean_object* l_Lean_Parser_symbolOrIdentInfo(lean_object*);
lean_object* l_Lean_Parser_Command_example___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_attribute___closed__10;
lean_object* l_Lean_Parser_addBuiltinParser(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
@ -415,7 +414,6 @@ lean_object* l_Lean_Parser_Command_prefix___closed__4;
lean_object* l_Lean_Parser_Command_private___closed__3;
lean_object* l_Lean_Parser_Command_extends___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_structExplicitBinder___closed__4;
extern lean_object* l_Lean_Parser_Level_max___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_abbrev___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_variables___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_infixl___closed__3;
@ -463,6 +461,7 @@ lean_object* l_Lean_Parser_Command_attribute;
lean_object* l_Lean_Parser_Command_docComment___closed__4;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_structure___closed__10;
lean_object* l_Lean_Parser_nonReservedSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_quotedSymbolPrec___elambda__1(lean_object*, lean_object*, lean_object*);
@ -492,6 +491,7 @@ lean_object* l_Lean_Parser_Command_declModifiers___closed__5;
lean_object* l_Lean_Parser_Command_structureTk___closed__1;
lean_object* l_Lean_Parser_Command_init__quot___closed__1;
lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_maxPrec___elambda__1___closed__5;
extern lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_universes___closed__1;
lean_object* lean_nat_sub(lean_object*, lean_object*);
@ -509,9 +509,9 @@ lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_prefix___closed__1;
lean_object* l_Lean_Parser_Command_infixl___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__2;
lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*);
lean_object* l_Lean_Parser_Command_example___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_declId___closed__1;
lean_object* l_Lean_Parser_symbolOrIdentFnAux(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_declModifiers___closed__15;
lean_object* l_Lean_Parser_Command_attributes___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_export___elambda__1(lean_object*, lean_object*, lean_object*);
@ -712,7 +712,7 @@ lean_object* l_Lean_Parser_Command_attributes___closed__1;
lean_object* l_Lean_Parser_Command_extends___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_universe___closed__2;
lean_object* l_Lean_Parser_Command_inductive___closed__6;
lean_object* l_Lean_Parser_registerBuiltinParserAttribute(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_registerBuiltinParserAttribute(lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l_Lean_Parser_Command_structCtor___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_commentBody___elambda__1(lean_object*, lean_object*, lean_object*);
@ -1043,6 +1043,7 @@ lean_object* l_Lean_Parser_Command_postfix___closed__2;
lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_noncomputable___closed__4;
lean_object* l_Lean_Parser_Command_structInstBinder___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_maxPrec___elambda__1___closed__7;
lean_object* l___regBuiltinParser_Lean_Parser_Term_stxQuot(lean_object*);
lean_object* l_Lean_Parser_Command_notation___closed__4;
lean_object* l_Lean_Parser_Command_openOnly___closed__6;
@ -1100,6 +1101,7 @@ lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_
lean_object* l_Lean_Parser_Command_mixfixKind___closed__6;
lean_object* l_Lean_Parser_Command_maxPrec___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_classInductive___elambda__1___closed__9;
extern lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__3;
lean_object* l_Lean_Parser_Command_openRenaming___closed__2;
lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_declaration___closed__8;
@ -1357,7 +1359,6 @@ lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_quotedSymbolPrec___closed__3;
lean_object* l_Lean_Parser_Command_structCtor___elambda__1___closed__6;
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Command_declId___elambda__1___spec__1(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Level_max___closed__1;
lean_object* l_Lean_Parser_Command_infixr___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_universe___closed__3;
lean_object* l_Lean_Parser_Command_structure___closed__12;
@ -1389,6 +1390,7 @@ lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_section___closed__6;
lean_object* l_Lean_Parser_Command_variables___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_declModifiers___closed__4;
lean_object* l_Lean_Parser_Command_maxPrec___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_set__option___closed__11;
lean_object* l_Lean_Parser_Command_open___elambda__1___closed__9;
@ -1435,11 +1437,12 @@ return x_3;
lean_object* l_Lean_Parser_regBuiltinCommandParserAttr(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
x_2 = l_Lean_Parser_regBuiltinCommandParserAttr___closed__2;
x_3 = l_Lean_Parser_regBuiltinCommandParserAttr___closed__4;
x_4 = l_Lean_Parser_registerBuiltinParserAttribute(x_2, x_3, x_1);
return x_4;
x_4 = 0;
x_5 = l_Lean_Parser_registerBuiltinParserAttribute(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_regCommandParserAttribute___closed__1() {
@ -21472,7 +21475,7 @@ lean_inc(x_25);
x_26 = l_Lean_Parser_Command_set__option___elambda__1___closed__7;
x_27 = l_Lean_Parser_Command_set__option___elambda__1___closed__10;
lean_inc(x_2);
x_28 = l_Lean_Parser_symbolOrIdentFnAux(x_26, x_27, x_2, x_21);
x_28 = l_Lean_Parser_nonReservedSymbolFnAux(x_26, x_27, x_2, x_21);
x_29 = lean_ctor_get(x_28, 3);
lean_inc(x_29);
if (lean_obj_tag(x_29) == 0)
@ -21523,7 +21526,7 @@ lean_dec(x_40);
x_42 = l_Lean_Parser_Command_set__option___elambda__1___closed__8;
x_43 = l_Lean_Parser_Command_set__option___elambda__1___closed__12;
lean_inc(x_2);
x_44 = l_Lean_Parser_symbolOrIdentFnAux(x_42, x_43, x_2, x_39);
x_44 = l_Lean_Parser_nonReservedSymbolFnAux(x_42, x_43, x_2, x_39);
x_45 = lean_ctor_get(x_44, 3);
lean_inc(x_45);
if (lean_obj_tag(x_45) == 0)
@ -21684,7 +21687,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_set__option___elambda__1___closed__7;
x_2 = l_Lean_Parser_symbolOrIdentInfo(x_1);
x_2 = l_Lean_Parser_nonReservedSymbolInfo(x_1);
return x_2;
}
}
@ -21693,7 +21696,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_set__option___elambda__1___closed__8;
x_2 = l_Lean_Parser_symbolOrIdentInfo(x_1);
x_2 = l_Lean_Parser_nonReservedSymbolInfo(x_1);
return x_2;
}
}
@ -26106,6 +26109,35 @@ x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Command_maxPrec___elambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Level_LevelToFormat_Result_format___main___closed__3;
x_2 = l_String_trim(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Command_maxPrec___elambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Command_maxPrec___elambda__1___closed__5;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_maxPrec___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_maxPrec___elambda__1___closed__6;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_Command_maxPrec___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -26158,9 +26190,9 @@ x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_array_get_size(x_15);
lean_dec(x_15);
x_17 = l_Lean_Parser_Level_max___elambda__1___closed__4;
x_18 = l_Lean_Parser_Level_max___elambda__1___closed__6;
x_19 = l_Lean_Parser_symbolOrIdentFnAux(x_17, x_18, x_2, x_14);
x_17 = l_Lean_Parser_Command_maxPrec___elambda__1___closed__5;
x_18 = l_Lean_Parser_Command_maxPrec___elambda__1___closed__7;
x_19 = l_Lean_Parser_nonReservedSymbolFnAux(x_17, x_18, x_2, x_14);
x_20 = l_Lean_Parser_Command_maxPrec___elambda__1___closed__2;
x_21 = l_Lean_Parser_ParserState_mkNode(x_19, x_20, x_16);
x_22 = l_Lean_Parser_mergeOrElseErrors(x_21, x_11, x_8);
@ -26173,26 +26205,35 @@ return x_22;
lean_object* _init_l_Lean_Parser_Command_maxPrec___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_maxPrec___elambda__1___closed__5;
x_2 = l_Lean_Parser_nonReservedSymbolInfo(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Command_maxPrec___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_maxPrec___elambda__1___closed__2;
x_2 = l_Lean_Parser_Level_max___closed__1;
x_2 = l_Lean_Parser_Command_maxPrec___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_maxPrec___closed__2() {
lean_object* _init_l_Lean_Parser_Command_maxPrec___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_maxPrec___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Command_maxPrec___closed__1;
x_3 = l_Lean_Parser_Command_maxPrec___closed__2;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Command_maxPrec___closed__3() {
lean_object* _init_l_Lean_Parser_Command_maxPrec___closed__4() {
_start:
{
lean_object* x_1;
@ -26200,12 +26241,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_maxPrec___elambda__1), 3,
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Command_maxPrec___closed__4() {
lean_object* _init_l_Lean_Parser_Command_maxPrec___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_maxPrec___closed__2;
x_2 = l_Lean_Parser_Command_maxPrec___closed__3;
x_1 = l_Lean_Parser_Command_maxPrec___closed__3;
x_2 = l_Lean_Parser_Command_maxPrec___closed__4;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -26216,7 +26257,7 @@ lean_object* _init_l_Lean_Parser_Command_maxPrec() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Command_maxPrec___closed__4;
x_1 = l_Lean_Parser_Command_maxPrec___closed__5;
return x_1;
}
}
@ -32242,6 +32283,12 @@ l_Lean_Parser_Command_maxPrec___elambda__1___closed__3 = _init_l_Lean_Parser_Com
lean_mark_persistent(l_Lean_Parser_Command_maxPrec___elambda__1___closed__3);
l_Lean_Parser_Command_maxPrec___elambda__1___closed__4 = _init_l_Lean_Parser_Command_maxPrec___elambda__1___closed__4();
lean_mark_persistent(l_Lean_Parser_Command_maxPrec___elambda__1___closed__4);
l_Lean_Parser_Command_maxPrec___elambda__1___closed__5 = _init_l_Lean_Parser_Command_maxPrec___elambda__1___closed__5();
lean_mark_persistent(l_Lean_Parser_Command_maxPrec___elambda__1___closed__5);
l_Lean_Parser_Command_maxPrec___elambda__1___closed__6 = _init_l_Lean_Parser_Command_maxPrec___elambda__1___closed__6();
lean_mark_persistent(l_Lean_Parser_Command_maxPrec___elambda__1___closed__6);
l_Lean_Parser_Command_maxPrec___elambda__1___closed__7 = _init_l_Lean_Parser_Command_maxPrec___elambda__1___closed__7();
lean_mark_persistent(l_Lean_Parser_Command_maxPrec___elambda__1___closed__7);
l_Lean_Parser_Command_maxPrec___closed__1 = _init_l_Lean_Parser_Command_maxPrec___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_maxPrec___closed__1);
l_Lean_Parser_Command_maxPrec___closed__2 = _init_l_Lean_Parser_Command_maxPrec___closed__2();
@ -32250,6 +32297,8 @@ l_Lean_Parser_Command_maxPrec___closed__3 = _init_l_Lean_Parser_Command_maxPrec_
lean_mark_persistent(l_Lean_Parser_Command_maxPrec___closed__3);
l_Lean_Parser_Command_maxPrec___closed__4 = _init_l_Lean_Parser_Command_maxPrec___closed__4();
lean_mark_persistent(l_Lean_Parser_Command_maxPrec___closed__4);
l_Lean_Parser_Command_maxPrec___closed__5 = _init_l_Lean_Parser_Command_maxPrec___closed__5();
lean_mark_persistent(l_Lean_Parser_Command_maxPrec___closed__5);
l_Lean_Parser_Command_maxPrec = _init_l_Lean_Parser_Command_maxPrec();
lean_mark_persistent(l_Lean_Parser_Command_maxPrec);
l_Lean_Parser_Command_precedenceLit___closed__1 = _init_l_Lean_Parser_Command_precedenceLit___closed__1();

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

@ -49,7 +49,6 @@ lean_object* l_Lean_Parser_registerBuiltinDynamicParserAttribute(lean_object*, l
lean_object* l_Lean_Parser_Level_paren___closed__7;
lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__5;
lean_object* l_Lean_Parser_Level_hole___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_symbolOrIdentInfo(lean_object*);
lean_object* l_Lean_Parser_addBuiltinParser(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_Parser_Level_ident___elambda__1___closed__3;
@ -75,12 +74,13 @@ lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__1;
lean_object* l_Lean_Parser_Level_ident___closed__3;
lean_object* l___regBuiltinParser_Lean_Parser_Level_paren(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Parser_nonReservedSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Name_appendIndexAfter___closed__1;
lean_object* l_Lean_Parser_nodeInfo(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_addLit___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__2;
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__7;
lean_object* l_Lean_Parser_symbolOrIdentFnAux(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*);
lean_object* l_Lean_Parser_Level_paren;
lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__2;
lean_object* l_Lean_Parser_Level_paren___closed__10;
@ -104,7 +104,7 @@ lean_object* l_Lean_Parser_regLevelParserAttribute(lean_object*);
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__11;
lean_object* l_Lean_Parser_Level_imax___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_ident___closed__1;
lean_object* l_Lean_Parser_registerBuiltinParserAttribute(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_registerBuiltinParserAttribute(lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l_Lean_Parser_Level_addLit___closed__5;
lean_object* l_Lean_Parser_Level_addLit___closed__3;
lean_object* l_Lean_Parser_Level_imax___closed__2;
@ -158,6 +158,7 @@ extern lean_object* l_Lean_Syntax_getKind___closed__3;
lean_object* l_Lean_Parser_mkAntiquot(uint8_t, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__13;
lean_object* l_Lean_Parser_Level_max___elambda__1___closed__5;
lean_object* l_Lean_Parser_Level_max___elambda__1___closed__7;
lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__5;
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__14;
lean_object* l_Lean_Parser_Level_max___elambda__1___closed__3;
@ -169,6 +170,7 @@ lean_object* l_Lean_Parser_Level_paren___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Level_imax(lean_object*);
lean_object* l_Lean_Parser_Level_imax___closed__4;
lean_object* l_Lean_Parser_numLitFn___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__7;
lean_object* l_Lean_Parser_Level_paren___closed__8;
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__4;
lean_object* l_Lean_Parser_Level_hole___closed__4;
@ -218,11 +220,12 @@ return x_3;
lean_object* l_Lean_Parser_regBuiltinLevelParserAttr(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
x_2 = l_Lean_Parser_regBuiltinLevelParserAttr___closed__2;
x_3 = l_Lean_Parser_regBuiltinLevelParserAttr___closed__4;
x_4 = l_Lean_Parser_registerBuiltinParserAttribute(x_2, x_3, x_1);
return x_4;
x_4 = 0;
x_5 = l_Lean_Parser_registerBuiltinParserAttribute(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_regLevelParserAttribute___closed__1() {
@ -858,27 +861,35 @@ return x_5;
lean_object* _init_l_Lean_Parser_Level_max___elambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Level_LevelToFormat_Result_format___main___closed__3;
x_2 = l_String_trim(x_1);
return x_2;
lean_object* x_1;
x_1 = lean_mk_string("max ");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Level_max___elambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Level_max___elambda__1___closed__4;
x_3 = lean_string_append(x_1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Level_max___elambda__1___closed__4;
x_2 = l_String_trim(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Level_max___elambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_max___elambda__1___closed__5;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Level_max___elambda__1___closed__5;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Level_max___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_max___elambda__1___closed__6;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
@ -939,10 +950,10 @@ x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_array_get_size(x_15);
lean_dec(x_15);
x_17 = l_Lean_Parser_Level_max___elambda__1___closed__4;
x_18 = l_Lean_Parser_Level_max___elambda__1___closed__6;
x_17 = l_Lean_Parser_Level_max___elambda__1___closed__5;
x_18 = l_Lean_Parser_Level_max___elambda__1___closed__7;
lean_inc(x_2);
x_19 = l_Lean_Parser_symbolOrIdentFnAux(x_17, x_18, x_2, x_14);
x_19 = l_Lean_Parser_nonReservedSymbolFnAux(x_17, x_18, x_2, x_14);
x_20 = lean_ctor_get(x_19, 3);
lean_inc(x_20);
if (lean_obj_tag(x_20) == 0)
@ -1007,8 +1018,8 @@ lean_object* _init_l_Lean_Parser_Level_max___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Level_max___elambda__1___closed__4;
x_2 = l_Lean_Parser_symbolOrIdentInfo(x_1);
x_1 = l_Lean_Parser_Level_max___elambda__1___closed__5;
x_2 = l_Lean_Parser_nonReservedSymbolInfo(x_1);
return x_2;
}
}
@ -1169,6 +1180,18 @@ x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Level_imax___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Level_imax___elambda__1___closed__6;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_Parser_Level_imax___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -1216,7 +1239,7 @@ return x_9;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_41; lean_object* x_42;
lean_inc(x_8);
x_14 = l_Lean_Parser_ParserState_restore(x_9, x_7, x_8);
lean_dec(x_7);
@ -1224,65 +1247,121 @@ x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_array_get_size(x_15);
lean_dec(x_15);
x_17 = l_Lean_Parser_Level_imax___elambda__1___closed__4;
x_18 = l_Lean_Parser_Level_imax___elambda__1___closed__6;
lean_inc(x_2);
x_19 = l_Lean_Parser_symbolOrIdentFnAux(x_17, x_18, x_2, x_14);
x_20 = lean_ctor_get(x_19, 3);
lean_inc(x_20);
if (lean_obj_tag(x_20) == 0)
x_41 = l_Lean_Parser_tokenFn(x_2, x_14);
x_42 = lean_ctor_get(x_41, 3);
lean_inc(x_42);
if (lean_obj_tag(x_42) == 0)
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_21 = lean_ctor_get(x_19, 0);
lean_inc(x_21);
x_22 = lean_array_get_size(x_21);
lean_dec(x_21);
x_23 = l_Lean_Parser_regBuiltinLevelParserAttr___closed__4;
x_24 = l_Lean_Parser_appPrec;
lean_inc(x_2);
x_25 = l_Lean_Parser_categoryParserFn(x_23, x_24, x_2, x_19);
x_26 = lean_ctor_get(x_25, 3);
lean_inc(x_26);
if (lean_obj_tag(x_26) == 0)
lean_object* x_43; lean_object* x_44;
x_43 = lean_ctor_get(x_41, 0);
lean_inc(x_43);
x_44 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_43);
lean_dec(x_43);
if (lean_obj_tag(x_44) == 2)
{
uint8_t x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
x_27 = 0;
x_28 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Level_max___elambda__1___spec__1(x_27, x_1, x_2, x_25);
lean_dec(x_1);
x_29 = l_Lean_nullKind;
x_30 = l_Lean_Parser_ParserState_mkNode(x_28, x_29, x_22);
x_31 = l_Lean_Parser_Level_imax___elambda__1___closed__1;
x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_16);
x_33 = l_Lean_Parser_mergeOrElseErrors(x_32, x_11, x_8);
lean_dec(x_8);
return x_33;
lean_object* x_45; lean_object* x_46; uint8_t x_47;
x_45 = lean_ctor_get(x_44, 1);
lean_inc(x_45);
lean_dec(x_44);
x_46 = l_Lean_Parser_Level_imax___elambda__1___closed__4;
x_47 = lean_string_dec_eq(x_45, x_46);
lean_dec(x_45);
if (x_47 == 0)
{
lean_object* x_48; lean_object* x_49;
x_48 = l_Lean_Parser_Level_imax___elambda__1___closed__7;
lean_inc(x_8);
x_49 = l_Lean_Parser_ParserState_mkErrorsAt(x_41, x_48, x_8);
x_17 = x_49;
goto block_40;
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38;
lean_dec(x_26);
lean_dec(x_2);
lean_dec(x_1);
x_34 = l_Lean_nullKind;
x_35 = l_Lean_Parser_ParserState_mkNode(x_25, x_34, x_22);
x_36 = l_Lean_Parser_Level_imax___elambda__1___closed__1;
x_37 = l_Lean_Parser_ParserState_mkNode(x_35, x_36, x_16);
x_38 = l_Lean_Parser_mergeOrElseErrors(x_37, x_11, x_8);
lean_dec(x_8);
return x_38;
x_17 = x_41;
goto block_40;
}
}
else
{
lean_object* x_39; lean_object* x_40; lean_object* x_41;
lean_dec(x_20);
lean_object* x_50; lean_object* x_51;
lean_dec(x_44);
x_50 = l_Lean_Parser_Level_imax___elambda__1___closed__7;
lean_inc(x_8);
x_51 = l_Lean_Parser_ParserState_mkErrorsAt(x_41, x_50, x_8);
x_17 = x_51;
goto block_40;
}
}
else
{
lean_object* x_52; lean_object* x_53;
lean_dec(x_42);
x_52 = l_Lean_Parser_Level_imax___elambda__1___closed__7;
lean_inc(x_8);
x_53 = l_Lean_Parser_ParserState_mkErrorsAt(x_41, x_52, x_8);
x_17 = x_53;
goto block_40;
}
block_40:
{
lean_object* x_18;
x_18 = lean_ctor_get(x_17, 3);
lean_inc(x_18);
if (lean_obj_tag(x_18) == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_19 = lean_ctor_get(x_17, 0);
lean_inc(x_19);
x_20 = lean_array_get_size(x_19);
lean_dec(x_19);
x_21 = l_Lean_Parser_regBuiltinLevelParserAttr___closed__4;
x_22 = l_Lean_Parser_appPrec;
lean_inc(x_2);
x_23 = l_Lean_Parser_categoryParserFn(x_21, x_22, x_2, x_17);
x_24 = lean_ctor_get(x_23, 3);
lean_inc(x_24);
if (lean_obj_tag(x_24) == 0)
{
uint8_t x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_25 = 0;
x_26 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Level_max___elambda__1___spec__1(x_25, x_1, x_2, x_23);
lean_dec(x_1);
x_27 = l_Lean_nullKind;
x_28 = l_Lean_Parser_ParserState_mkNode(x_26, x_27, x_20);
x_29 = l_Lean_Parser_Level_imax___elambda__1___closed__1;
x_30 = l_Lean_Parser_ParserState_mkNode(x_28, x_29, x_16);
x_31 = l_Lean_Parser_mergeOrElseErrors(x_30, x_11, x_8);
lean_dec(x_8);
return x_31;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
lean_dec(x_24);
lean_dec(x_2);
lean_dec(x_1);
x_39 = l_Lean_Parser_Level_imax___elambda__1___closed__1;
x_40 = l_Lean_Parser_ParserState_mkNode(x_19, x_39, x_16);
x_41 = l_Lean_Parser_mergeOrElseErrors(x_40, x_11, x_8);
x_32 = l_Lean_nullKind;
x_33 = l_Lean_Parser_ParserState_mkNode(x_23, x_32, x_20);
x_34 = l_Lean_Parser_Level_imax___elambda__1___closed__1;
x_35 = l_Lean_Parser_ParserState_mkNode(x_33, x_34, x_16);
x_36 = l_Lean_Parser_mergeOrElseErrors(x_35, x_11, x_8);
lean_dec(x_8);
return x_41;
return x_36;
}
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
lean_dec(x_18);
lean_dec(x_2);
lean_dec(x_1);
x_37 = l_Lean_Parser_Level_imax___elambda__1___closed__1;
x_38 = l_Lean_Parser_ParserState_mkNode(x_17, x_37, x_16);
x_39 = l_Lean_Parser_mergeOrElseErrors(x_38, x_11, x_8);
lean_dec(x_8);
return x_39;
}
}
}
}
@ -1291,10 +1370,11 @@ return x_41;
lean_object* _init_l_Lean_Parser_Level_imax___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Level_imax___elambda__1___closed__4;
x_2 = l_Lean_Parser_symbolOrIdentInfo(x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Level_imax___elambda__1___closed__4;
x_3 = l_Lean_Parser_symbolInfo(x_2, x_1);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Level_imax___closed__2() {
@ -2322,6 +2402,8 @@ l_Lean_Parser_Level_max___elambda__1___closed__5 = _init_l_Lean_Parser_Level_max
lean_mark_persistent(l_Lean_Parser_Level_max___elambda__1___closed__5);
l_Lean_Parser_Level_max___elambda__1___closed__6 = _init_l_Lean_Parser_Level_max___elambda__1___closed__6();
lean_mark_persistent(l_Lean_Parser_Level_max___elambda__1___closed__6);
l_Lean_Parser_Level_max___elambda__1___closed__7 = _init_l_Lean_Parser_Level_max___elambda__1___closed__7();
lean_mark_persistent(l_Lean_Parser_Level_max___elambda__1___closed__7);
l_Lean_Parser_Level_max___closed__1 = _init_l_Lean_Parser_Level_max___closed__1();
lean_mark_persistent(l_Lean_Parser_Level_max___closed__1);
l_Lean_Parser_Level_max___closed__2 = _init_l_Lean_Parser_Level_max___closed__2();
@ -2353,6 +2435,8 @@ l_Lean_Parser_Level_imax___elambda__1___closed__5 = _init_l_Lean_Parser_Level_im
lean_mark_persistent(l_Lean_Parser_Level_imax___elambda__1___closed__5);
l_Lean_Parser_Level_imax___elambda__1___closed__6 = _init_l_Lean_Parser_Level_imax___elambda__1___closed__6();
lean_mark_persistent(l_Lean_Parser_Level_imax___elambda__1___closed__6);
l_Lean_Parser_Level_imax___elambda__1___closed__7 = _init_l_Lean_Parser_Level_imax___elambda__1___closed__7();
lean_mark_persistent(l_Lean_Parser_Level_imax___elambda__1___closed__7);
l_Lean_Parser_Level_imax___closed__1 = _init_l_Lean_Parser_Level_imax___closed__1();
lean_mark_persistent(l_Lean_Parser_Level_imax___closed__1);
l_Lean_Parser_Level_imax___closed__2 = _init_l_Lean_Parser_Level_imax___closed__2();

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

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

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

@ -35,7 +35,6 @@ lean_object* l_Lean_Parser_Term_letIdDecl;
lean_object* l_Lean_Parser_Term_heq___elambda__1___closed__4;
extern lean_object* l_Lean_Parser_charLit___closed__1;
lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_infixL___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Term_iff(lean_object*);
lean_object* l_Lean_mkAppStx(lean_object*, lean_object*);
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___elambda__1___spec__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
@ -46,6 +45,7 @@ lean_object* l_Lean_Parser_Term_if___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_subst;
lean_object* l_Lean_Parser_Term_quotedName___closed__4;
lean_object* l_Lean_Parser_Term_andthen___elambda__1___closed__2;
lean_object* l_Lean_Parser_unicodeInfixL___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_doSeq___elambda__1___spec__2(uint8_t, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__3;
lean_object* l_Lean_Parser_Term_app___elambda__1___closed__1;
@ -130,6 +130,7 @@ lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___closed__6;
extern lean_object* l_Lean_Parser_Level_paren___closed__2;
lean_object* l_Lean_Parser_Term_inaccessible___closed__1;
lean_object* l_Lean_Parser_Term_not___closed__6;
lean_object* l_Lean_Parser_unicodeInfixR(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__12;
lean_object* l_Lean_Parser_Term_lt___elambda__1___closed__4;
@ -160,6 +161,7 @@ lean_object* l_Lean_Parser_Term_char___closed__3;
lean_object* l_Lean_Parser_Term_listLit___closed__3;
lean_object* l_Lean_Parser_Term_match___closed__7;
lean_object* l___regBuiltinParser_Lean_Parser_Term_pow(lean_object*);
lean_object* l_Lean_Parser_unicodeInfixR___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_eq___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__16;
@ -341,6 +343,7 @@ lean_object* l_Lean_Parser_Term_doLet___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_doPat___closed__4;
lean_object* l_Lean_Parser_Term_doId___closed__2;
lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__4;
lean_object* l_Lean_Parser_infixR___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_match___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__5;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_match__syntax___elambda__1___spec__1___closed__1;
@ -520,7 +523,6 @@ lean_object* l_Lean_Parser_Term_where___closed__4;
lean_object* l_Lean_Parser_Term_prod___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_paren___closed__5;
lean_object* l_Lean_Parser_Term_letPatDecl___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_infixR___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_div___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_sort___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_arrayLit___closed__6;
@ -582,6 +584,7 @@ lean_object* l_Lean_Parser_Term_tupleTail___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_hole___closed__4;
lean_object* l_Lean_Parser_Term_cons___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_fun___closed__6;
lean_object* l_Lean_Parser_infixR___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_num___closed__2;
lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_binderDefault;
@ -689,6 +692,7 @@ lean_object* l_Lean_Parser_Term_structInst___closed__4;
lean_object* l_Lean_Parser_Term_num___closed__4;
lean_object* l_Lean_Parser_dollarSymbol(uint8_t);
lean_object* l_Lean_Parser_Term_suffices___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_infixR(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_fromTerm___closed__2;
lean_object* l_Lean_Parser_Term_id___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_type___elambda__1___closed__5;
@ -795,6 +799,7 @@ lean_object* l_Lean_Parser_Term_orM___closed__1;
lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_letIdDecl___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_equiv___elambda__1___closed__1;
lean_object* l_Lean_Parser_infixL___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_not___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_doElem___closed__4;
lean_object* l_Lean_Parser_Term_seqLeft___elambda__1(lean_object*, lean_object*, lean_object*);
@ -1096,7 +1101,6 @@ lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_
lean_object* l_Lean_Parser_Term_id___closed__3;
lean_object* l_Lean_Parser_Term_let___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_sortApp___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_unicodeInfixL(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_hole___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_structInstSource___closed__6;
lean_object* l_Lean_Parser_Term_namedArgument___closed__2;
@ -1244,7 +1248,6 @@ lean_object* l_Lean_Parser_Term_match__syntax___closed__1;
lean_object* l_Lean_Parser_Term_instBinder___closed__2;
extern lean_object* l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
lean_object* l_Lean_Parser_Term_letDecl___closed__1;
lean_object* l_Lean_Parser_Term_unicodeInfixL___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doSeq___closed__5;
lean_object* l_Lean_Parser_Term_emptyC___closed__4;
lean_object* l_Lean_Parser_Term_band___closed__3;
@ -1282,7 +1285,6 @@ lean_object* l_Lean_Parser_Term_le___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_eq___closed__2;
lean_object* l_Lean_Parser_Term_binderIdent;
lean_object* l_Lean_Parser_Term_simpleBinder___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_infixR(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_seqLeft___closed__3;
lean_object* l_Lean_Parser_Term_implicitBinder___elambda__1___closed__2;
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__4;
@ -1300,7 +1302,6 @@ lean_object* l_Lean_Parser_Term_have___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_namedPattern___closed__4;
lean_object* l_Lean_Parser_Term_seq___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_infixL___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_binderTactic___closed__2;
lean_object* l_Lean_Parser_Term_if___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_div___closed__1;
@ -1402,7 +1403,6 @@ lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__12;
lean_object* l_Lean_Syntax_isTermId_x3f(lean_object*);
lean_object* l_Lean_Parser_Term_let___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_type___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_infixL(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_anonymousCtor;
lean_object* l_Lean_Parser_Term_dollarProj___closed__4;
lean_object* l_Lean_Parser_Term_iff___closed__3;
@ -1423,6 +1423,7 @@ lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_binderType___closed__2;
lean_object* l_Lean_Parser_Term_borrowed___closed__5;
lean_object* l_Lean_Parser_Term_explicitUniv___closed__8;
lean_object* l_Lean_Parser_unicodeInfixR___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_equiv___closed__1;
lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_not___closed__7;
@ -1440,6 +1441,7 @@ lean_object* l_Lean_Parser_Term_structInstSource___closed__1;
lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_depArrow___closed__6;
lean_object* l_Lean_Parser_Term_mapConst___elambda__1___closed__3;
lean_object* l_Lean_Parser_unicodeInfixL(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_namedPattern___closed__1;
lean_object* l_Lean_Parser_Term_doId___closed__7;
lean_object* l_Lean_Parser_Term_explicitBinder___closed__2;
@ -1649,7 +1651,6 @@ lean_object* l_Lean_Parser_Term_fcomp___closed__3;
lean_object* l_Lean_Parser_Term_doLet___closed__2;
lean_object* l_Lean_Parser_Term_type___closed__5;
lean_object* l_Lean_Parser_Term_match___elambda__1___closed__10;
lean_object* l_Lean_Parser_Term_unicodeInfixR___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_andthen___closed__1;
lean_object* l_Lean_Parser_Term_and___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___closed__6;
@ -1720,7 +1721,6 @@ lean_object* l_Lean_Parser_Term_dollarProj;
lean_object* l_Lean_Parser_Term_dollarProj___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_proj___closed__6;
lean_object* l_Lean_Parser_Term_type___closed__4;
lean_object* l_Lean_Parser_Term_infixR___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_beq___closed__2;
lean_object* l_Lean_Parser_Term_arrayLit___closed__2;
lean_object* l_Lean_Parser_Term_ne___elambda__1___closed__4;
@ -1739,6 +1739,7 @@ lean_object* l_Lean_Parser_Term_if___elambda__1___closed__12;
lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_structInst___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_fcomp___closed__2;
lean_object* l_Lean_Parser_Term_where___closed__3;
lean_object* l_Lean_Parser_unicodeInfixL___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_map___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_sort___elambda__1___closed__9;
lean_object* l___regBuiltinParser_Lean_Parser_Term_gt(lean_object*);
@ -1838,6 +1839,7 @@ lean_object* l_Lean_Parser_Term_bindOp___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_do___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_letDecl___closed__3;
lean_object* l_Lean_Parser_Term_subtype___elambda__1___closed__3;
lean_object* l_Lean_Parser_infixL(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_if___closed__7;
lean_object* l_Lean_Parser_Term_match___closed__10;
lean_object* l_Lean_Parser_Term_modN___elambda__1___closed__2;
@ -1868,10 +1870,8 @@ lean_object* l_Lean_Parser_Term_doExpr___closed__3;
lean_object* l_Lean_Parser_Term_binderTactic___closed__3;
lean_object* l_Lean_Parser_Term_doId___closed__6;
lean_object* l_Lean_Parser_Term_leftArrow___elambda__1(lean_object*);
lean_object* l_Lean_Parser_Term_unicodeInfixR___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_unicodeInfixL___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_subtype___closed__11;
lean_object* l_Lean_Parser_unicodeSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_where___closed__10;
@ -1890,7 +1890,6 @@ lean_object* l_Lean_Parser_Term_bnot___elambda__1(lean_object*, lean_object*, le
lean_object* l_Lean_Parser_Term_let;
lean_object* l_Lean_Parser_Term_depArrow___closed__3;
lean_object* l_Lean_Parser_Term_map;
lean_object* l_Lean_Parser_Term_unicodeInfixR(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_forall___closed__6;
lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__2;
@ -1916,6 +1915,7 @@ lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_forall___elambda
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_suffices___closed__3;
lean_object* l_Lean_Parser_Term_arrayRef___elambda__1___closed__3;
lean_object* l_Lean_Parser_infixL___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__8;
@ -1928,7 +1928,7 @@ lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_letIdDecl___closed__6;
lean_object* l_Lean_Parser_Term_app___closed__4;
extern lean_object* l_Lean_Parser_mkAntiquot___closed__1;
lean_object* l_Lean_Parser_Term_unicodeInfixR___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Parser_unicodeInfixR___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
@ -1954,7 +1954,7 @@ return x_5;
}
}
}
lean_object* l_Lean_Parser_Term_unicodeInfixR(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Parser_unicodeInfixR(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; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
@ -1988,7 +1988,7 @@ lean_closure_set(x_17, 0, x_8);
lean_closure_set(x_17, 1, x_16);
x_18 = l_Lean_Parser_epsilonInfo;
x_19 = l_Lean_Parser_andthenInfo(x_18, x_15);
x_20 = lean_alloc_closure((void*)(l_Lean_Parser_Term_unicodeInfixR___elambda__1), 4, 1);
x_20 = lean_alloc_closure((void*)(l_Lean_Parser_unicodeInfixR___elambda__1), 4, 1);
lean_closure_set(x_20, 0, x_17);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_19);
@ -1996,17 +1996,17 @@ lean_ctor_set(x_21, 1, x_20);
return x_21;
}
}
lean_object* l_Lean_Parser_Term_unicodeInfixR___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Parser_unicodeInfixR___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Parser_Term_unicodeInfixR(x_1, x_2, x_3);
x_4 = l_Lean_Parser_unicodeInfixR(x_1, x_2, x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
lean_object* l_Lean_Parser_Term_infixR___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Parser_infixR___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
@ -2032,7 +2032,7 @@ return x_5;
}
}
}
lean_object* l_Lean_Parser_Term_infixR(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Parser_infixR(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; uint8_t x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
@ -2063,7 +2063,7 @@ lean_closure_set(x_15, 0, x_6);
lean_closure_set(x_15, 1, x_14);
x_16 = l_Lean_Parser_epsilonInfo;
x_17 = l_Lean_Parser_andthenInfo(x_16, x_13);
x_18 = lean_alloc_closure((void*)(l_Lean_Parser_Term_infixR___elambda__1), 4, 1);
x_18 = lean_alloc_closure((void*)(l_Lean_Parser_infixR___elambda__1), 4, 1);
lean_closure_set(x_18, 0, x_15);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_17);
@ -2071,16 +2071,16 @@ lean_ctor_set(x_19, 1, x_18);
return x_19;
}
}
lean_object* l_Lean_Parser_Term_infixR___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Parser_infixR___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_Parser_Term_unicodeInfixL___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Parser_unicodeInfixL___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
@ -2106,7 +2106,7 @@ return x_5;
}
}
}
lean_object* l_Lean_Parser_Term_unicodeInfixL(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Parser_unicodeInfixL(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; uint8_t x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
@ -2137,7 +2137,7 @@ lean_closure_set(x_15, 0, x_8);
lean_closure_set(x_15, 1, x_14);
x_16 = l_Lean_Parser_epsilonInfo;
x_17 = l_Lean_Parser_andthenInfo(x_16, x_13);
x_18 = lean_alloc_closure((void*)(l_Lean_Parser_Term_unicodeInfixL___elambda__1), 4, 1);
x_18 = lean_alloc_closure((void*)(l_Lean_Parser_unicodeInfixL___elambda__1), 4, 1);
lean_closure_set(x_18, 0, x_15);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_17);
@ -2145,17 +2145,17 @@ lean_ctor_set(x_19, 1, x_18);
return x_19;
}
}
lean_object* l_Lean_Parser_Term_unicodeInfixL___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Parser_unicodeInfixL___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Parser_Term_unicodeInfixL(x_1, x_2, x_3);
x_4 = l_Lean_Parser_unicodeInfixL(x_1, x_2, x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
lean_object* l_Lean_Parser_Term_infixL___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Parser_infixL___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
@ -2181,7 +2181,7 @@ return x_5;
}
}
}
lean_object* l_Lean_Parser_Term_infixL(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Parser_infixL(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; uint8_t 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; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
@ -2209,7 +2209,7 @@ lean_closure_set(x_13, 0, x_6);
lean_closure_set(x_13, 1, x_12);
x_14 = l_Lean_Parser_epsilonInfo;
x_15 = l_Lean_Parser_andthenInfo(x_14, x_11);
x_16 = lean_alloc_closure((void*)(l_Lean_Parser_Term_infixL___elambda__1), 4, 1);
x_16 = lean_alloc_closure((void*)(l_Lean_Parser_infixL___elambda__1), 4, 1);
lean_closure_set(x_16, 0, x_13);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_15);
@ -2217,11 +2217,11 @@ lean_ctor_set(x_17, 1, x_16);
return x_17;
}
}
lean_object* l_Lean_Parser_Term_infixL___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Parser_infixL___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
lean_dec(x_1);
return x_3;
}
@ -30689,7 +30689,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_depArrow___elambda__1___closed__6;
x_2 = l_Lean_Parser_Term_depArrow___elambda__1___closed__8;
x_3 = lean_unsigned_to_nat(25u);
x_4 = l_Lean_Parser_Term_unicodeInfixR(x_1, x_2, x_3);
x_4 = l_Lean_Parser_unicodeInfixR(x_1, x_2, x_3);
return x_4;
}
}
@ -32259,7 +32259,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_fcomp___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(90u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -32364,7 +32364,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_prod___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(35u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -32469,7 +32469,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_add___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(65u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -32574,7 +32574,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_sub___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(65u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -32679,7 +32679,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_mul___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(70u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -32784,7 +32784,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_div___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(70u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -32889,7 +32889,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_mod___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(70u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -32994,7 +32994,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_modN___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(70u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -33099,7 +33099,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_pow___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(80u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -33213,7 +33213,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_le___elambda__1___closed__3;
x_2 = l_Lean_Parser_Term_le___elambda__1___closed__4;
x_3 = lean_unsigned_to_nat(50u);
x_4 = l_Lean_Parser_Term_unicodeInfixL(x_1, x_2, x_3);
x_4 = l_Lean_Parser_unicodeInfixL(x_1, x_2, x_3);
return x_4;
}
}
@ -33327,7 +33327,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_ge___elambda__1___closed__3;
x_2 = l_Lean_Parser_Term_ge___elambda__1___closed__4;
x_3 = lean_unsigned_to_nat(50u);
x_4 = l_Lean_Parser_Term_unicodeInfixL(x_1, x_2, x_3);
x_4 = l_Lean_Parser_unicodeInfixL(x_1, x_2, x_3);
return x_4;
}
}
@ -33432,7 +33432,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_lt___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(50u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -33537,7 +33537,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_gt___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(50u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -33642,7 +33642,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_eq___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(50u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -33747,7 +33747,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_ne___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(50u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -33852,7 +33852,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_beq___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(50u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -33957,7 +33957,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_bne___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(50u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -34071,7 +34071,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_heq___elambda__1___closed__3;
x_2 = l_Lean_Parser_Term_heq___elambda__1___closed__4;
x_3 = lean_unsigned_to_nat(50u);
x_4 = l_Lean_Parser_Term_unicodeInfixL(x_1, x_2, x_3);
x_4 = l_Lean_Parser_unicodeInfixL(x_1, x_2, x_3);
return x_4;
}
}
@ -34176,7 +34176,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_equiv___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(50u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -34281,7 +34281,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_subst___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(75u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -34395,7 +34395,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_and___elambda__1___closed__3;
x_2 = l_Lean_Parser_Term_and___elambda__1___closed__4;
x_3 = lean_unsigned_to_nat(35u);
x_4 = l_Lean_Parser_Term_unicodeInfixR(x_1, x_2, x_3);
x_4 = l_Lean_Parser_unicodeInfixR(x_1, x_2, x_3);
return x_4;
}
}
@ -34509,7 +34509,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_or___elambda__1___closed__3;
x_2 = l_Lean_Parser_Term_or___elambda__1___closed__4;
x_3 = lean_unsigned_to_nat(30u);
x_4 = l_Lean_Parser_Term_unicodeInfixR(x_1, x_2, x_3);
x_4 = l_Lean_Parser_unicodeInfixR(x_1, x_2, x_3);
return x_4;
}
}
@ -34623,7 +34623,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_iff___elambda__1___closed__3;
x_2 = l_Lean_Parser_Term_iff___elambda__1___closed__4;
x_3 = lean_unsigned_to_nat(20u);
x_4 = l_Lean_Parser_Term_unicodeInfixL(x_1, x_2, x_3);
x_4 = l_Lean_Parser_unicodeInfixL(x_1, x_2, x_3);
return x_4;
}
}
@ -34728,7 +34728,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_band___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(35u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -34833,7 +34833,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_bor___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(30u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -34938,7 +34938,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_append___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(65u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -35043,7 +35043,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_cons___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(67u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -35148,7 +35148,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_orelse___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(2u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -35253,7 +35253,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_orM___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(30u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -35358,7 +35358,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_andM___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(35u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -35463,7 +35463,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_andthen___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(60u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -35568,7 +35568,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_bindOp___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(55u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -35673,7 +35673,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_mapRev___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(100u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -35778,7 +35778,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_seq___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(60u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -35883,7 +35883,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_seqLeft___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(60u);
x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
x_3 = l_Lean_Parser_infixL(x_1, x_2);
return x_3;
}
}
@ -35988,7 +35988,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_seqRight___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(60u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -36093,7 +36093,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_map___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(100u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -36198,7 +36198,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_mapConst___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(100u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}
@ -36303,7 +36303,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_mapConstRev___elambda__1___closed__3;
x_2 = lean_unsigned_to_nat(100u);
x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
x_3 = l_Lean_Parser_infixR(x_1, x_2);
return x_3;
}
}