diff --git a/stage0/src/Init/Lean/Parser/Level.lean b/stage0/src/Init/Lean/Parser/Level.lean
index aebf4e3d5b..c5c2a2f51d 100644
--- a/stage0/src/Init/Lean/Parser/Level.lean
+++ b/stage0/src/Init/Lean/Parser/Level.lean
@@ -23,7 +23,7 @@ namespace Level
 @[builtinLevelParser] def hole   := parser! "_"
 @[builtinLevelParser] def num    := parser! numLit
 @[builtinLevelParser] def ident  := parser! ident
-@[builtinLevelParser] def addLit := tparser! pushLeading >> symbol "+" (65:Nat) >> numLit
+@[builtinLevelParser] def addLit := tparser! symbol "+" (65:Nat) >> numLit
 
 end Level
 
diff --git a/stage0/src/Init/Lean/Parser/Parser.lean b/stage0/src/Init/Lean/Parser/Parser.lean
index 8d6e662fb7..50b18e66e1 100644
--- a/stage0/src/Init/Lean/Parser/Parser.lean
+++ b/stage0/src/Init/Lean/Parser/Parser.lean
@@ -1714,6 +1714,7 @@ def compileParserDescr (categories : ParserCategories) : forall {k : ParserKind}
 | _, ParserDescr.sepBy d₁ d₂                         => sepBy <$> compileParserDescr d₁ <*> compileParserDescr d₂
 | _, ParserDescr.sepBy1 d₁ d₂                        => sepBy1 <$> compileParserDescr d₁ <*> compileParserDescr d₂
 | _, ParserDescr.node k d                            => node k <$> compileParserDescr d
+| ParserKind.trailing, ParserDescr.trailingNode k d  => trailingNode k <$> compileParserDescr d
 | _, ParserDescr.symbol tk lbp                       => pure $ symbolAux tk lbp
 | _, ParserDescr.numLit                              => pure $ numLit
 | _, ParserDescr.strLit                              => pure $ strLit
diff --git a/stage0/src/Init/Lean/Parser/Syntax.lean b/stage0/src/Init/Lean/Parser/Syntax.lean
index 6097389243..87783a86e2 100644
--- a/stage0/src/Init/Lean/Parser/Syntax.lean
+++ b/stage0/src/Init/Lean/Parser/Syntax.lean
@@ -35,10 +35,10 @@ namespace Syntax
 @[builtinSyntaxParser] def sepBy     := parser! nonReservedSymbol "sepBy " >> syntaxParser appPrec >> syntaxParser appPrec
 @[builtinSyntaxParser] def sepBy1    := parser! nonReservedSymbol "sepBy1 " >> syntaxParser appPrec >> syntaxParser appPrec
 
-@[builtinSyntaxParser] def optional  := tparser! pushLeading >> symbolAux "?" none
-@[builtinSyntaxParser] def many      := tparser! pushLeading >> symbolAux "*" none
-@[builtinSyntaxParser] def many1     := tparser! pushLeading >> symbolAux "+" none
-@[builtinSyntaxParser] def orelse    := tparser! pushLeading >> " <|> " >> syntaxParser 1
+@[builtinSyntaxParser] def optional  := tparser! symbolAux "?" none
+@[builtinSyntaxParser] def many      := tparser! symbolAux "*" none
+@[builtinSyntaxParser] def many1     := tparser! symbolAux "+" none
+@[builtinSyntaxParser] def orelse    := tparser! " <|> " >> syntaxParser 1
 
 end Syntax
 
diff --git a/stage0/src/Init/Lean/Parser/Tactic.lean b/stage0/src/Init/Lean/Parser/Tactic.lean
index 366860c861..64b6ea869b 100644
--- a/stage0/src/Init/Lean/Parser/Tactic.lean
+++ b/stage0/src/Init/Lean/Parser/Tactic.lean
@@ -54,7 +54,7 @@ def nonEmptySeq : Parser := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "
 @[builtinTacticParser] def paren        := parser! "(" >> nonEmptySeq >> ")"
 @[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
 @[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"
-@[builtinTacticParser] def orelse := tparser! pushLeading >> " <|> " >> tacticParser 1
+@[builtinTacticParser] def orelse := tparser! " <|> " >> tacticParser 1
 
 end Tactic
 
diff --git a/stage0/src/Init/Lean/Parser/Term.lean b/stage0/src/Init/Lean/Parser/Term.lean
index 3cbcd98684..3e8942b53d 100644
--- a/stage0/src/Init/Lean/Parser/Term.lean
+++ b/stage0/src/Init/Lean/Parser/Term.lean
@@ -17,16 +17,16 @@ namespace Term
 /- Helper functions for defining simple parsers -/
 
 def unicodeInfixR (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
-pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser (lbp - 1)
+unicodeSymbol sym asciiSym lbp >> termParser (lbp - 1)
 
 def infixR (sym : String) (lbp : Nat) : TrailingParser :=
-pushLeading >> symbol sym lbp >> termParser (lbp - 1)
+symbol sym lbp >> termParser (lbp - 1)
 
 def unicodeInfixL (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
-pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser lbp
+unicodeSymbol sym asciiSym lbp >> termParser lbp
 
 def infixL (sym : String) (lbp : Nat) : TrailingParser :=
-pushLeading >> symbol sym lbp >> termParser lbp
+symbol sym lbp >> termParser lbp
 
 /- Built-in parsers -/
 -- NOTE: `checkNoWsBefore` should be used *before* `parser!` so that it is also applied to the generated
@@ -122,18 +122,18 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}"
 @[builtinTermParser] def uminus := parser! "-" >> termParser 100
 
 def namedArgument  := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
-@[builtinTermParser] def app      := tparser! pushLeading >> many1 ((toTrailing namedArgument) <|> termParser appPrec)
+@[builtinTermParser] def app      := tparser! many1 ((toTrailing namedArgument) <|> termParser appPrec)
 
 def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Term.type || leading.isOfKind `Lean.Parser.Term.sort)
-@[builtinTermParser] def sortApp  := tparser! checkIsSort >> pushLeading >> levelParser appPrec
-@[builtinTermParser] def proj     := tparser! pushLeading >> symbolNoWs "." (appPrec+1) >> (fieldIdx <|> ident)
+@[builtinTermParser] def sortApp  := tparser! checkIsSort >> levelParser appPrec
+@[builtinTermParser] def proj     := tparser! symbolNoWs "." (appPrec+1) >> (fieldIdx <|> ident)
 @[builtinTermParser] def arrow    := tparser! unicodeInfixR " → " " -> " 25
-@[builtinTermParser] def arrayRef := tparser! pushLeading >> symbolNoWs "[" (appPrec+1) >> termParser >>"]"
+@[builtinTermParser] def arrayRef := tparser! symbolNoWs "[" (appPrec+1) >> termParser >>"]"
 
-@[builtinTermParser] def dollar     := tparser! try (pushLeading >> dollarSymbol >> checkWsBefore "space expected") >> termParser 0
-@[builtinTermParser] def dollarProj := tparser! pushLeading >> symbol "$." 1 >> (fieldIdx <|> ident)
+@[builtinTermParser] def dollar     := tparser! try (dollarSymbol >> checkWsBefore "space expected") >> termParser 0
+@[builtinTermParser] def dollarProj := tparser! symbol "$." 1 >> (fieldIdx <|> ident)
 
-@[builtinTermParser] def «where»    := tparser! pushLeading >> symbol " where " 1 >> sepBy1 (toTrailing letDecl) (group ("; " >> " where "))
+@[builtinTermParser] def «where»    := tparser! symbol " where " 1 >> sepBy1 (toTrailing letDecl) (group ("; " >> " where "))
 
 @[builtinTermParser] def fcomp  := tparser! infixR " ∘ " 90
 
diff --git a/stage0/src/Init/LeanInit.lean b/stage0/src/Init/LeanInit.lean
index 2e477a29b6..f55b41b631 100644
--- a/stage0/src/Init/LeanInit.lean
+++ b/stage0/src/Init/LeanInit.lean
@@ -149,6 +149,7 @@ inductive ParserDescrCore : ParserKind → Type
 | sepBy {k : ParserKind}         : ParserDescrCore k → ParserDescrCore k → ParserDescrCore k
 | sepBy1 {k : ParserKind}        : ParserDescrCore k → ParserDescrCore k → ParserDescrCore k
 | node {k : ParserKind}          : Name → ParserDescrCore k → ParserDescrCore k
+| trailingNode                   : Name → ParserDescrCore ParserKind.trailing → ParserDescrCore ParserKind.trailing
 | symbol {k : ParserKind}        : String → Option Nat → ParserDescrCore k
 | nonReservedSymbol              : String → Bool → ParserDescrCore ParserKind.leading
 | numLit {k : ParserKind}        : ParserDescrCore k
@@ -174,6 +175,7 @@ abbrev TrailingParserDescr := ParserDescrCore ParserKind.trailing
 @[matchPattern] abbrev ParserDescr.sepBy := @ParserDescrCore.sepBy
 @[matchPattern] abbrev ParserDescr.sepBy1 := @ParserDescrCore.sepBy1
 @[matchPattern] abbrev ParserDescr.node := @ParserDescrCore.node
+@[matchPattern] abbrev ParserDescr.trailingNode := @ParserDescrCore.trailingNode
 @[matchPattern] abbrev ParserDescr.symbol := @ParserDescrCore.symbol
 @[matchPattern] abbrev ParserDescr.numLit := @ParserDescrCore.numLit
 @[matchPattern] abbrev ParserDescr.strLit := @ParserDescrCore.strLit
diff --git a/stage0/stdlib/Init/Lean/Parser/Level.c b/stage0/stdlib/Init/Lean/Parser/Level.c
index d5ecc40f82..29c9944082 100644
--- a/stage0/stdlib/Init/Lean/Parser/Level.c
+++ b/stage0/stdlib/Init/Lean/Parser/Level.c
@@ -108,7 +108,6 @@ lean_object* l_Lean_Parser_Level_ident___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Level_paren___closed__4;
 lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Level_paren___closed__9;
-lean_object* l_Lean_Parser_Level_addLit___closed__7;
 lean_object* l_Lean_Parser_categoryParserFn(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__2;
@@ -130,7 +129,6 @@ lean_object* l_Lean_Parser_Level_max___closed__5;
 lean_object* l_Lean_Parser_Level_num___closed__3;
 lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__10;
 lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*);
-extern lean_object* l_Lean_Parser_epsilonInfo;
 lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__6;
 extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
 extern lean_object* l_Lean_mkHole___closed__1;
@@ -2081,7 +2079,7 @@ return x_3;
 lean_object* l_Lean_Parser_Level_addLit___elambda__1(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_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
 x_4 = l_Lean_Parser_Level_addLit___elambda__1___closed__4;
 x_5 = lean_ctor_get(x_4, 1);
 lean_inc(x_5);
@@ -2089,98 +2087,88 @@ x_6 = lean_ctor_get(x_3, 0);
 lean_inc(x_6);
 x_7 = lean_array_get_size(x_6);
 lean_dec(x_6);
-x_8 = lean_ctor_get(x_3, 3);
-lean_inc(x_8);
-if (lean_obj_tag(x_8) == 0)
-{
-lean_object* x_9; lean_object* x_10; lean_object* x_11; 
-x_9 = lean_ctor_get(x_3, 1);
-lean_inc(x_9);
+x_16 = lean_ctor_get(x_3, 1);
+lean_inc(x_16);
 lean_inc(x_2);
-x_10 = l_Lean_Parser_tokenFn(x_2, x_3);
-x_11 = lean_ctor_get(x_10, 3);
-lean_inc(x_11);
-if (lean_obj_tag(x_11) == 0)
+x_17 = l_Lean_Parser_tokenFn(x_2, x_3);
+x_18 = lean_ctor_get(x_17, 3);
+lean_inc(x_18);
+if (lean_obj_tag(x_18) == 0)
 {
-lean_object* x_12; lean_object* x_13; 
-x_12 = lean_ctor_get(x_10, 0);
-lean_inc(x_12);
-x_13 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_12);
-lean_dec(x_12);
-if (lean_obj_tag(x_13) == 2)
+lean_object* x_19; lean_object* x_20; 
+x_19 = lean_ctor_get(x_17, 0);
+lean_inc(x_19);
+x_20 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_19);
+lean_dec(x_19);
+if (lean_obj_tag(x_20) == 2)
 {
-lean_object* x_14; lean_object* x_15; uint8_t x_16; 
-x_14 = lean_ctor_get(x_13, 1);
-lean_inc(x_14);
-lean_dec(x_13);
-x_15 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
-x_16 = lean_string_dec_eq(x_14, x_15);
-lean_dec(x_14);
-if (x_16 == 0)
+lean_object* x_21; lean_object* x_22; uint8_t x_23; 
+x_21 = lean_ctor_get(x_20, 1);
+lean_inc(x_21);
+lean_dec(x_20);
+x_22 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
+x_23 = lean_string_dec_eq(x_21, x_22);
+lean_dec(x_21);
+if (x_23 == 0)
 {
-lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; 
-lean_dec(x_5);
-lean_dec(x_2);
-lean_dec(x_1);
-x_17 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
-x_18 = l_Lean_Parser_ParserState_mkErrorsAt(x_10, x_17, x_9);
-x_19 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
-x_20 = l_Lean_Parser_ParserState_mkTrailingNode(x_18, x_19, x_7);
-lean_dec(x_7);
-return x_20;
-}
-else
-{
-lean_object* x_21; lean_object* x_22; lean_object* x_23; 
-lean_dec(x_9);
-x_21 = lean_apply_3(x_5, x_1, x_2, x_10);
-x_22 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
-x_23 = l_Lean_Parser_ParserState_mkTrailingNode(x_21, x_22, x_7);
-lean_dec(x_7);
-return x_23;
-}
-}
-else
-{
-lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; 
-lean_dec(x_13);
-lean_dec(x_5);
-lean_dec(x_2);
-lean_dec(x_1);
+lean_object* x_24; lean_object* x_25; 
 x_24 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
-x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_10, x_24, x_9);
-x_26 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
-x_27 = l_Lean_Parser_ParserState_mkTrailingNode(x_25, x_26, x_7);
-lean_dec(x_7);
-return x_27;
+x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_24, x_16);
+x_8 = x_25;
+goto block_15;
+}
+else
+{
+lean_dec(x_16);
+x_8 = x_17;
+goto block_15;
 }
 }
 else
 {
-lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; 
-lean_dec(x_11);
-lean_dec(x_5);
-lean_dec(x_2);
-lean_dec(x_1);
+lean_object* x_26; lean_object* x_27; 
+lean_dec(x_20);
+x_26 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
+x_27 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_26, x_16);
+x_8 = x_27;
+goto block_15;
+}
+}
+else
+{
+lean_object* x_28; lean_object* x_29; 
+lean_dec(x_18);
 x_28 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
-x_29 = l_Lean_Parser_ParserState_mkErrorsAt(x_10, x_28, x_9);
-x_30 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
-x_31 = l_Lean_Parser_ParserState_mkTrailingNode(x_29, x_30, x_7);
-lean_dec(x_7);
-return x_31;
+x_29 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_28, x_16);
+x_8 = x_29;
+goto block_15;
 }
+block_15:
+{
+lean_object* x_9; 
+x_9 = lean_ctor_get(x_8, 3);
+lean_inc(x_9);
+if (lean_obj_tag(x_9) == 0)
+{
+lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_10 = lean_apply_3(x_5, x_1, x_2, x_8);
+x_11 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
+x_12 = l_Lean_Parser_ParserState_mkTrailingNode(x_10, x_11, x_7);
+lean_dec(x_7);
+return x_12;
 }
 else
 {
-lean_object* x_32; lean_object* x_33; 
-lean_dec(x_8);
+lean_object* x_13; lean_object* x_14; 
+lean_dec(x_9);
 lean_dec(x_5);
 lean_dec(x_2);
 lean_dec(x_1);
-x_32 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
-x_33 = l_Lean_Parser_ParserState_mkTrailingNode(x_3, x_32, x_7);
+x_13 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
+x_14 = l_Lean_Parser_ParserState_mkTrailingNode(x_8, x_13, x_7);
 lean_dec(x_7);
-return x_33;
+return x_14;
+}
 }
 }
 }
@@ -2220,23 +2208,13 @@ lean_object* _init_l_Lean_Parser_Level_addLit___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_epsilonInfo;
-x_2 = l_Lean_Parser_Level_addLit___closed__3;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Level_addLit___closed__5() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
-x_2 = l_Lean_Parser_Level_addLit___closed__4;
+x_2 = l_Lean_Parser_Level_addLit___closed__3;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Level_addLit___closed__6() {
+lean_object* _init_l_Lean_Parser_Level_addLit___closed__5() {
 _start:
 {
 lean_object* x_1; 
@@ -2244,12 +2222,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Level_addLit___elambda__1), 3, 0)
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Level_addLit___closed__7() {
+lean_object* _init_l_Lean_Parser_Level_addLit___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Level_addLit___closed__5;
-x_2 = l_Lean_Parser_Level_addLit___closed__6;
+x_1 = l_Lean_Parser_Level_addLit___closed__4;
+x_2 = l_Lean_Parser_Level_addLit___closed__5;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -2260,7 +2238,7 @@ lean_object* _init_l_Lean_Parser_Level_addLit() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Level_addLit___closed__7;
+x_1 = l_Lean_Parser_Level_addLit___closed__6;
 return x_1;
 }
 }
@@ -2504,8 +2482,6 @@ l_Lean_Parser_Level_addLit___closed__5 = _init_l_Lean_Parser_Level_addLit___clos
 lean_mark_persistent(l_Lean_Parser_Level_addLit___closed__5);
 l_Lean_Parser_Level_addLit___closed__6 = _init_l_Lean_Parser_Level_addLit___closed__6();
 lean_mark_persistent(l_Lean_Parser_Level_addLit___closed__6);
-l_Lean_Parser_Level_addLit___closed__7 = _init_l_Lean_Parser_Level_addLit___closed__7();
-lean_mark_persistent(l_Lean_Parser_Level_addLit___closed__7);
 l_Lean_Parser_Level_addLit = _init_l_Lean_Parser_Level_addLit();
 lean_mark_persistent(l_Lean_Parser_Level_addLit);
 res = l___regBuiltinParser_Lean_Parser_Level_addLit(lean_io_mk_world());
diff --git a/stage0/stdlib/Init/Lean/Parser/Parser.c b/stage0/stdlib/Init/Lean/Parser/Parser.c
index c2b13a142e..3045f321c6 100644
--- a/stage0/stdlib/Init/Lean/Parser/Parser.c
+++ b/stage0/stdlib/Init/Lean/Parser/Parser.c
@@ -32573,7 +32573,7 @@ return x_267;
 }
 }
 }
-case 10:
+case 11:
 {
 lean_object* x_268; lean_object* x_269; lean_object* x_270; lean_object* x_271; lean_object* x_272; lean_object* x_273; lean_object* x_274; 
 lean_dec(x_1);
@@ -32595,7 +32595,7 @@ x_274 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_274, 0, x_273);
 return x_274;
 }
-case 11:
+case 12:
 {
 lean_object* x_275; uint8_t x_276; lean_object* x_277; lean_object* x_278; lean_object* x_279; lean_object* x_280; lean_object* x_281; 
 lean_dec(x_1);
@@ -32616,7 +32616,7 @@ x_281 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_281, 0, x_280);
 return x_281;
 }
-case 12:
+case 13:
 {
 lean_object* x_282; lean_object* x_283; 
 lean_dec(x_3);
@@ -32626,7 +32626,7 @@ x_283 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_283, 0, x_282);
 return x_283;
 }
-case 13:
+case 14:
 {
 lean_object* x_284; lean_object* x_285; 
 lean_dec(x_3);
@@ -32636,7 +32636,7 @@ x_285 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_285, 0, x_284);
 return x_285;
 }
-case 14:
+case 15:
 {
 lean_object* x_286; lean_object* x_287; 
 lean_dec(x_3);
@@ -32646,7 +32646,7 @@ x_287 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_287, 0, x_286);
 return x_287;
 }
-case 15:
+case 16:
 {
 lean_object* x_288; lean_object* x_289; 
 lean_dec(x_3);
@@ -32656,7 +32656,7 @@ x_289 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_289, 0, x_288);
 return x_289;
 }
-case 16:
+case 17:
 {
 lean_object* x_290; lean_object* x_291; 
 lean_dec(x_3);
@@ -33712,110 +33712,194 @@ return x_561;
 }
 case 10:
 {
-lean_object* x_562; lean_object* x_563; lean_object* x_564; lean_object* x_565; lean_object* x_566; lean_object* x_567; lean_object* x_568; 
-lean_dec(x_1);
+lean_object* x_562; lean_object* x_563; lean_object* x_564; 
 x_562 = lean_ctor_get(x_3, 0);
 lean_inc(x_562);
 x_563 = lean_ctor_get(x_3, 1);
 lean_inc(x_563);
 lean_dec(x_3);
-x_564 = l_String_trim(x_562);
+x_564 = l_Lean_Parser_compileParserDescr___main(x_1, x_2, x_563);
+if (lean_obj_tag(x_564) == 0)
+{
+uint8_t x_565; 
 lean_dec(x_562);
-lean_inc(x_564);
-x_565 = l_Lean_Parser_symbolInfo(x_564, x_563);
-x_566 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
-lean_closure_set(x_566, 0, x_564);
-x_567 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_567, 0, x_565);
-lean_ctor_set(x_567, 1, x_566);
-x_568 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_568, 0, x_567);
-return x_568;
-}
-case 12:
+x_565 = !lean_is_exclusive(x_564);
+if (x_565 == 0)
 {
-lean_object* x_569; lean_object* x_570; 
-lean_dec(x_3);
-lean_dec(x_1);
-x_569 = l_Lean_Parser_numLit(x_2);
-x_570 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_570, 0, x_569);
-return x_570;
-}
-case 13:
-{
-lean_object* x_571; lean_object* x_572; 
-lean_dec(x_3);
-lean_dec(x_1);
-x_571 = l_Lean_Parser_strLit(x_2);
-x_572 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_572, 0, x_571);
-return x_572;
-}
-case 14:
-{
-lean_object* x_573; lean_object* x_574; 
-lean_dec(x_3);
-lean_dec(x_1);
-x_573 = l_Lean_Parser_charLit(x_2);
-x_574 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_574, 0, x_573);
-return x_574;
-}
-case 15:
-{
-lean_object* x_575; lean_object* x_576; 
-lean_dec(x_3);
-lean_dec(x_1);
-x_575 = l_Lean_Parser_nameLit(x_2);
-x_576 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_576, 0, x_575);
-return x_576;
-}
-case 16:
-{
-lean_object* x_577; lean_object* x_578; 
-lean_dec(x_3);
-lean_dec(x_1);
-x_577 = l_Lean_Parser_ident(x_2);
-x_578 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_578, 0, x_577);
-return x_578;
-}
-case 17:
-{
-lean_object* x_579; 
-lean_dec(x_1);
-x_579 = l_Lean_Parser_compileParserDescr___main___closed__1;
-return x_579;
-}
-default: 
-{
-lean_object* x_580; lean_object* x_581; lean_object* x_582; 
-x_580 = lean_ctor_get(x_3, 0);
-lean_inc(x_580);
-x_581 = lean_ctor_get(x_3, 1);
-lean_inc(x_581);
-lean_dec(x_3);
-x_582 = l_PersistentHashMap_find_x3f___at_Lean_Parser_addLeadingParser___spec__1(x_1, x_580);
-if (lean_obj_tag(x_582) == 0)
-{
-lean_object* x_583; 
-lean_dec(x_581);
-x_583 = l_Lean_Parser_throwUnknownParserCategory___rarg(x_580);
-return x_583;
+return x_564;
 }
 else
 {
-lean_object* x_584; lean_object* x_585; 
-lean_dec(x_582);
-x_584 = l_Lean_Parser_categoryParser(x_2, x_580, x_581);
+lean_object* x_566; lean_object* x_567; 
+x_566 = lean_ctor_get(x_564, 0);
+lean_inc(x_566);
+lean_dec(x_564);
+x_567 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_567, 0, x_566);
+return x_567;
+}
+}
+else
+{
+uint8_t x_568; 
+x_568 = !lean_is_exclusive(x_564);
+if (x_568 == 0)
+{
+lean_object* x_569; lean_object* x_570; lean_object* x_571; lean_object* x_572; uint8_t x_573; lean_object* x_574; lean_object* x_575; lean_object* x_576; 
+x_569 = lean_ctor_get(x_564, 0);
+x_570 = lean_ctor_get(x_569, 0);
+lean_inc(x_570);
+lean_inc(x_562);
+x_571 = l_Lean_Parser_nodeInfo(x_562, x_570);
+x_572 = lean_ctor_get(x_569, 1);
+lean_inc(x_572);
+lean_dec(x_569);
+x_573 = 1;
+x_574 = lean_box(x_573);
+x_575 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn___boxed), 6, 3);
+lean_closure_set(x_575, 0, x_574);
+lean_closure_set(x_575, 1, x_562);
+lean_closure_set(x_575, 2, x_572);
+x_576 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_576, 0, x_571);
+lean_ctor_set(x_576, 1, x_575);
+lean_ctor_set(x_564, 0, x_576);
+return x_564;
+}
+else
+{
+lean_object* x_577; lean_object* x_578; lean_object* x_579; lean_object* x_580; uint8_t x_581; lean_object* x_582; lean_object* x_583; lean_object* x_584; lean_object* x_585; 
+x_577 = lean_ctor_get(x_564, 0);
+lean_inc(x_577);
+lean_dec(x_564);
+x_578 = lean_ctor_get(x_577, 0);
+lean_inc(x_578);
+lean_inc(x_562);
+x_579 = l_Lean_Parser_nodeInfo(x_562, x_578);
+x_580 = lean_ctor_get(x_577, 1);
+lean_inc(x_580);
+lean_dec(x_577);
+x_581 = 1;
+x_582 = lean_box(x_581);
+x_583 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn___boxed), 6, 3);
+lean_closure_set(x_583, 0, x_582);
+lean_closure_set(x_583, 1, x_562);
+lean_closure_set(x_583, 2, x_580);
+x_584 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_584, 0, x_579);
+lean_ctor_set(x_584, 1, x_583);
 x_585 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_585, 0, x_584);
 return x_585;
 }
 }
 }
+case 11:
+{
+lean_object* x_586; lean_object* x_587; lean_object* x_588; lean_object* x_589; lean_object* x_590; lean_object* x_591; lean_object* x_592; 
+lean_dec(x_1);
+x_586 = lean_ctor_get(x_3, 0);
+lean_inc(x_586);
+x_587 = lean_ctor_get(x_3, 1);
+lean_inc(x_587);
+lean_dec(x_3);
+x_588 = l_String_trim(x_586);
+lean_dec(x_586);
+lean_inc(x_588);
+x_589 = l_Lean_Parser_symbolInfo(x_588, x_587);
+x_590 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
+lean_closure_set(x_590, 0, x_588);
+x_591 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_591, 0, x_589);
+lean_ctor_set(x_591, 1, x_590);
+x_592 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_592, 0, x_591);
+return x_592;
+}
+case 13:
+{
+lean_object* x_593; lean_object* x_594; 
+lean_dec(x_3);
+lean_dec(x_1);
+x_593 = l_Lean_Parser_numLit(x_2);
+x_594 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_594, 0, x_593);
+return x_594;
+}
+case 14:
+{
+lean_object* x_595; lean_object* x_596; 
+lean_dec(x_3);
+lean_dec(x_1);
+x_595 = l_Lean_Parser_strLit(x_2);
+x_596 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_596, 0, x_595);
+return x_596;
+}
+case 15:
+{
+lean_object* x_597; lean_object* x_598; 
+lean_dec(x_3);
+lean_dec(x_1);
+x_597 = l_Lean_Parser_charLit(x_2);
+x_598 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_598, 0, x_597);
+return x_598;
+}
+case 16:
+{
+lean_object* x_599; lean_object* x_600; 
+lean_dec(x_3);
+lean_dec(x_1);
+x_599 = l_Lean_Parser_nameLit(x_2);
+x_600 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_600, 0, x_599);
+return x_600;
+}
+case 17:
+{
+lean_object* x_601; lean_object* x_602; 
+lean_dec(x_3);
+lean_dec(x_1);
+x_601 = l_Lean_Parser_ident(x_2);
+x_602 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_602, 0, x_601);
+return x_602;
+}
+case 18:
+{
+lean_object* x_603; 
+lean_dec(x_1);
+x_603 = l_Lean_Parser_compileParserDescr___main___closed__1;
+return x_603;
+}
+default: 
+{
+lean_object* x_604; lean_object* x_605; lean_object* x_606; 
+x_604 = lean_ctor_get(x_3, 0);
+lean_inc(x_604);
+x_605 = lean_ctor_get(x_3, 1);
+lean_inc(x_605);
+lean_dec(x_3);
+x_606 = l_PersistentHashMap_find_x3f___at_Lean_Parser_addLeadingParser___spec__1(x_1, x_604);
+if (lean_obj_tag(x_606) == 0)
+{
+lean_object* x_607; 
+lean_dec(x_605);
+x_607 = l_Lean_Parser_throwUnknownParserCategory___rarg(x_604);
+return x_607;
+}
+else
+{
+lean_object* x_608; lean_object* x_609; 
+lean_dec(x_606);
+x_608 = l_Lean_Parser_categoryParser(x_2, x_604, x_605);
+x_609 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_609, 0, x_608);
+return x_609;
+}
+}
+}
 }
 }
 }
diff --git a/stage0/stdlib/Init/Lean/Parser/Syntax.c b/stage0/stdlib/Init/Lean/Parser/Syntax.c
index 9b9130f4e4..6c1d631c7a 100644
--- a/stage0/stdlib/Init/Lean/Parser/Syntax.c
+++ b/stage0/stdlib/Init/Lean/Parser/Syntax.c
@@ -353,7 +353,6 @@ lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__3;
 lean_object* l_Lean_Parser_precedenceLit___closed__1;
 lean_object* l_Lean_Parser_Syntax_sepBy1___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Command_macroTailDefault___closed__3;
-lean_object* l_Lean_Parser_Syntax_orelse___closed__6;
 lean_object* l_Lean_Parser_Syntax_char___closed__1;
 lean_object* l_Lean_Parser_Syntax_ident___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__3;
@@ -445,7 +444,6 @@ lean_object* l_Lean_Parser_Syntax_num___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Syntax_many___elambda__1___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Syntax_paren___closed__2;
 lean_object* l_Lean_Parser_Command_mixfixKind___elambda__1(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Parser_Syntax_many1___closed__5;
 extern lean_object* l_Lean_Parser_Term_haveAssign___closed__1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_num(lean_object*);
 lean_object* l_Lean_Parser_Command_macro___closed__6;
@@ -483,7 +481,6 @@ lean_object* l_Lean_Parser_Syntax_many1___closed__3;
 lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
 lean_object* l_Lean_Parser_Command_infix___closed__3;
-lean_object* l_Lean_Parser_Syntax_optional___closed__5;
 lean_object* l_Lean_Parser_Syntax_ident___closed__4;
 lean_object* l_Lean_Parser_Syntax_atom___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Command_notation___elambda__1___closed__4;
@@ -494,6 +491,7 @@ extern lean_object* l_Lean_Parser_Term_match___elambda__1___closed__9;
 lean_object* l_Lean_Parser_maxPrec___closed__5;
 lean_object* l_Lean_Parser_Command_macroTailTactic___closed__6;
 lean_object* l_Lean_Parser_Command_notation___closed__1;
+extern lean_object* l_Lean_Parser_mkAntiquotAux___closed__11;
 lean_object* l_Lean_Parser_Command_macroTailCommand___closed__4;
 lean_object* l_Lean_Parser_Command_infixl___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Syntax_lookahead___elambda__1(lean_object*, lean_object*, lean_object*);
@@ -614,7 +612,6 @@ lean_object* l_Lean_Parser_Syntax_atom___closed__2;
 lean_object* l_Lean_Parser_precedence___closed__2;
 lean_object* l_Lean_Parser_Syntax_char___elambda__1(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_regBuiltinTacticParserAttr___closed__4;
-extern lean_object* l_Lean_Parser_mkAntiquotAux___closed__13;
 lean_object* l_Lean_Parser_Command_optKind___closed__3;
 lean_object* l_Lean_Parser_Command_infixr___closed__4;
 lean_object* l_Lean_Parser_Syntax_try___elambda__1___closed__3;
@@ -4211,90 +4208,74 @@ return x_3;
 lean_object* l_Lean_Parser_Syntax_optional___elambda__1___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_3 = lean_ctor_get(x_2, 0);
 lean_inc(x_3);
 x_4 = lean_array_get_size(x_3);
 lean_dec(x_3);
-x_5 = lean_ctor_get(x_2, 3);
+x_5 = lean_ctor_get(x_2, 1);
 lean_inc(x_5);
-if (lean_obj_tag(x_5) == 0)
+x_6 = l_Lean_Parser_tokenFn(x_1, x_2);
+x_7 = lean_ctor_get(x_6, 3);
+lean_inc(x_7);
+if (lean_obj_tag(x_7) == 0)
 {
-lean_object* x_6; lean_object* x_7; lean_object* x_8; 
-x_6 = lean_ctor_get(x_2, 1);
-lean_inc(x_6);
-x_7 = l_Lean_Parser_tokenFn(x_1, x_2);
-x_8 = lean_ctor_get(x_7, 3);
+lean_object* x_8; lean_object* x_9; 
+x_8 = lean_ctor_get(x_6, 0);
 lean_inc(x_8);
-if (lean_obj_tag(x_8) == 0)
-{
-lean_object* x_9; lean_object* x_10; 
-x_9 = lean_ctor_get(x_7, 0);
-lean_inc(x_9);
-x_10 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_9);
-lean_dec(x_9);
-if (lean_obj_tag(x_10) == 2)
-{
-lean_object* x_11; lean_object* x_12; uint8_t x_13; 
-x_11 = lean_ctor_get(x_10, 1);
-lean_inc(x_11);
-lean_dec(x_10);
-x_12 = l_Lean_Parser_Term_namedHole___elambda__1___closed__5;
-x_13 = lean_string_dec_eq(x_11, x_12);
-lean_dec(x_11);
-if (x_13 == 0)
-{
-lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
-x_14 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
-x_15 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_14, x_6);
-x_16 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
-x_17 = l_Lean_Parser_ParserState_mkTrailingNode(x_15, x_16, x_4);
-lean_dec(x_4);
-return x_17;
-}
-else
-{
-lean_object* x_18; lean_object* x_19; 
-lean_dec(x_6);
-x_18 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
-x_19 = l_Lean_Parser_ParserState_mkTrailingNode(x_7, x_18, x_4);
-lean_dec(x_4);
-return x_19;
-}
-}
-else
-{
-lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
-lean_dec(x_10);
-x_20 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
-x_21 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_20, x_6);
-x_22 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
-x_23 = l_Lean_Parser_ParserState_mkTrailingNode(x_21, x_22, x_4);
-lean_dec(x_4);
-return x_23;
-}
-}
-else
-{
-lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; 
+x_9 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_8);
 lean_dec(x_8);
-x_24 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
-x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_24, x_6);
-x_26 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
-x_27 = l_Lean_Parser_ParserState_mkTrailingNode(x_25, x_26, x_4);
+if (lean_obj_tag(x_9) == 2)
+{
+lean_object* x_10; lean_object* x_11; uint8_t x_12; 
+x_10 = lean_ctor_get(x_9, 1);
+lean_inc(x_10);
+lean_dec(x_9);
+x_11 = l_Lean_Parser_Term_namedHole___elambda__1___closed__5;
+x_12 = lean_string_dec_eq(x_10, x_11);
+lean_dec(x_10);
+if (x_12 == 0)
+{
+lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
+x_13 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
+x_14 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_13, x_5);
+x_15 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
+x_16 = l_Lean_Parser_ParserState_mkTrailingNode(x_14, x_15, x_4);
 lean_dec(x_4);
-return x_27;
+return x_16;
+}
+else
+{
+lean_object* x_17; lean_object* x_18; 
+lean_dec(x_5);
+x_17 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
+x_18 = l_Lean_Parser_ParserState_mkTrailingNode(x_6, x_17, x_4);
+lean_dec(x_4);
+return x_18;
 }
 }
 else
 {
-lean_object* x_28; lean_object* x_29; 
-lean_dec(x_5);
-lean_dec(x_1);
-x_28 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
-x_29 = l_Lean_Parser_ParserState_mkTrailingNode(x_2, x_28, x_4);
+lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+lean_dec(x_9);
+x_19 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
+x_20 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_19, x_5);
+x_21 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
+x_22 = l_Lean_Parser_ParserState_mkTrailingNode(x_20, x_21, x_4);
 lean_dec(x_4);
-return x_29;
+return x_22;
+}
+}
+else
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
+lean_dec(x_7);
+x_23 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
+x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_23, x_5);
+x_25 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
+x_26 = l_Lean_Parser_ParserState_mkTrailingNode(x_24, x_25, x_4);
+lean_dec(x_4);
+return x_26;
 }
 }
 }
@@ -4320,23 +4301,13 @@ lean_object* _init_l_Lean_Parser_Syntax_optional___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_epsilonInfo;
-x_2 = l_Lean_Parser_Syntax_optional___closed__1;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Syntax_optional___closed__3() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
-x_2 = l_Lean_Parser_Syntax_optional___closed__2;
+x_2 = l_Lean_Parser_Syntax_optional___closed__1;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Syntax_optional___closed__4() {
+lean_object* _init_l_Lean_Parser_Syntax_optional___closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -4344,12 +4315,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Syntax_optional___elambda__1___bo
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Syntax_optional___closed__5() {
+lean_object* _init_l_Lean_Parser_Syntax_optional___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Syntax_optional___closed__3;
-x_2 = l_Lean_Parser_Syntax_optional___closed__4;
+x_1 = l_Lean_Parser_Syntax_optional___closed__2;
+x_2 = l_Lean_Parser_Syntax_optional___closed__3;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -4360,7 +4331,7 @@ lean_object* _init_l_Lean_Parser_Syntax_optional() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Syntax_optional___closed__5;
+x_1 = l_Lean_Parser_Syntax_optional___closed__4;
 return x_1;
 }
 }
@@ -4438,90 +4409,74 @@ return x_3;
 lean_object* l_Lean_Parser_Syntax_many___elambda__1___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_3 = lean_ctor_get(x_2, 0);
 lean_inc(x_3);
 x_4 = lean_array_get_size(x_3);
 lean_dec(x_3);
-x_5 = lean_ctor_get(x_2, 3);
+x_5 = lean_ctor_get(x_2, 1);
 lean_inc(x_5);
-if (lean_obj_tag(x_5) == 0)
+x_6 = l_Lean_Parser_tokenFn(x_1, x_2);
+x_7 = lean_ctor_get(x_6, 3);
+lean_inc(x_7);
+if (lean_obj_tag(x_7) == 0)
 {
-lean_object* x_6; lean_object* x_7; lean_object* x_8; 
-x_6 = lean_ctor_get(x_2, 1);
-lean_inc(x_6);
-x_7 = l_Lean_Parser_tokenFn(x_1, x_2);
-x_8 = lean_ctor_get(x_7, 3);
+lean_object* x_8; lean_object* x_9; 
+x_8 = lean_ctor_get(x_6, 0);
 lean_inc(x_8);
-if (lean_obj_tag(x_8) == 0)
-{
-lean_object* x_9; lean_object* x_10; 
-x_9 = lean_ctor_get(x_7, 0);
-lean_inc(x_9);
-x_10 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_9);
-lean_dec(x_9);
-if (lean_obj_tag(x_10) == 2)
-{
-lean_object* x_11; lean_object* x_12; uint8_t x_13; 
-x_11 = lean_ctor_get(x_10, 1);
-lean_inc(x_11);
-lean_dec(x_10);
-x_12 = l_Lean_Parser_mkAntiquotAux___closed__10;
-x_13 = lean_string_dec_eq(x_11, x_12);
-lean_dec(x_11);
-if (x_13 == 0)
-{
-lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
-x_14 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__5;
-x_15 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_14, x_6);
-x_16 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
-x_17 = l_Lean_Parser_ParserState_mkTrailingNode(x_15, x_16, x_4);
-lean_dec(x_4);
-return x_17;
-}
-else
-{
-lean_object* x_18; lean_object* x_19; 
-lean_dec(x_6);
-x_18 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
-x_19 = l_Lean_Parser_ParserState_mkTrailingNode(x_7, x_18, x_4);
-lean_dec(x_4);
-return x_19;
-}
-}
-else
-{
-lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
-lean_dec(x_10);
-x_20 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__5;
-x_21 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_20, x_6);
-x_22 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
-x_23 = l_Lean_Parser_ParserState_mkTrailingNode(x_21, x_22, x_4);
-lean_dec(x_4);
-return x_23;
-}
-}
-else
-{
-lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; 
+x_9 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_8);
 lean_dec(x_8);
-x_24 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__5;
-x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_24, x_6);
-x_26 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
-x_27 = l_Lean_Parser_ParserState_mkTrailingNode(x_25, x_26, x_4);
+if (lean_obj_tag(x_9) == 2)
+{
+lean_object* x_10; lean_object* x_11; uint8_t x_12; 
+x_10 = lean_ctor_get(x_9, 1);
+lean_inc(x_10);
+lean_dec(x_9);
+x_11 = l_Lean_Parser_mkAntiquotAux___closed__10;
+x_12 = lean_string_dec_eq(x_10, x_11);
+lean_dec(x_10);
+if (x_12 == 0)
+{
+lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
+x_13 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__5;
+x_14 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_13, x_5);
+x_15 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
+x_16 = l_Lean_Parser_ParserState_mkTrailingNode(x_14, x_15, x_4);
 lean_dec(x_4);
-return x_27;
+return x_16;
+}
+else
+{
+lean_object* x_17; lean_object* x_18; 
+lean_dec(x_5);
+x_17 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
+x_18 = l_Lean_Parser_ParserState_mkTrailingNode(x_6, x_17, x_4);
+lean_dec(x_4);
+return x_18;
 }
 }
 else
 {
-lean_object* x_28; lean_object* x_29; 
-lean_dec(x_5);
-lean_dec(x_1);
-x_28 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
-x_29 = l_Lean_Parser_ParserState_mkTrailingNode(x_2, x_28, x_4);
+lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+lean_dec(x_9);
+x_19 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__5;
+x_20 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_19, x_5);
+x_21 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
+x_22 = l_Lean_Parser_ParserState_mkTrailingNode(x_20, x_21, x_4);
 lean_dec(x_4);
-return x_29;
+return x_22;
+}
+}
+else
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
+lean_dec(x_7);
+x_23 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__5;
+x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_23, x_5);
+x_25 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
+x_26 = l_Lean_Parser_ParserState_mkTrailingNode(x_24, x_25, x_4);
+lean_dec(x_4);
+return x_26;
 }
 }
 }
@@ -4538,7 +4493,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
-x_2 = l_Lean_Parser_mkAntiquotAux___closed__13;
+x_2 = l_Lean_Parser_mkAntiquotAux___closed__11;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
@@ -4613,90 +4568,74 @@ return x_3;
 lean_object* l_Lean_Parser_Syntax_many1___elambda__1___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_3 = lean_ctor_get(x_2, 0);
 lean_inc(x_3);
 x_4 = lean_array_get_size(x_3);
 lean_dec(x_3);
-x_5 = lean_ctor_get(x_2, 3);
+x_5 = lean_ctor_get(x_2, 1);
 lean_inc(x_5);
-if (lean_obj_tag(x_5) == 0)
+x_6 = l_Lean_Parser_tokenFn(x_1, x_2);
+x_7 = lean_ctor_get(x_6, 3);
+lean_inc(x_7);
+if (lean_obj_tag(x_7) == 0)
 {
-lean_object* x_6; lean_object* x_7; lean_object* x_8; 
-x_6 = lean_ctor_get(x_2, 1);
-lean_inc(x_6);
-x_7 = l_Lean_Parser_tokenFn(x_1, x_2);
-x_8 = lean_ctor_get(x_7, 3);
+lean_object* x_8; lean_object* x_9; 
+x_8 = lean_ctor_get(x_6, 0);
 lean_inc(x_8);
-if (lean_obj_tag(x_8) == 0)
-{
-lean_object* x_9; lean_object* x_10; 
-x_9 = lean_ctor_get(x_7, 0);
-lean_inc(x_9);
-x_10 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_9);
-lean_dec(x_9);
-if (lean_obj_tag(x_10) == 2)
-{
-lean_object* x_11; lean_object* x_12; uint8_t x_13; 
-x_11 = lean_ctor_get(x_10, 1);
-lean_inc(x_11);
-lean_dec(x_10);
-x_12 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
-x_13 = lean_string_dec_eq(x_11, x_12);
-lean_dec(x_11);
-if (x_13 == 0)
-{
-lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
-x_14 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
-x_15 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_14, x_6);
-x_16 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
-x_17 = l_Lean_Parser_ParserState_mkTrailingNode(x_15, x_16, x_4);
-lean_dec(x_4);
-return x_17;
-}
-else
-{
-lean_object* x_18; lean_object* x_19; 
-lean_dec(x_6);
-x_18 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
-x_19 = l_Lean_Parser_ParserState_mkTrailingNode(x_7, x_18, x_4);
-lean_dec(x_4);
-return x_19;
-}
-}
-else
-{
-lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
-lean_dec(x_10);
-x_20 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
-x_21 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_20, x_6);
-x_22 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
-x_23 = l_Lean_Parser_ParserState_mkTrailingNode(x_21, x_22, x_4);
-lean_dec(x_4);
-return x_23;
-}
-}
-else
-{
-lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; 
+x_9 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_8);
 lean_dec(x_8);
-x_24 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
-x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_24, x_6);
-x_26 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
-x_27 = l_Lean_Parser_ParserState_mkTrailingNode(x_25, x_26, x_4);
+if (lean_obj_tag(x_9) == 2)
+{
+lean_object* x_10; lean_object* x_11; uint8_t x_12; 
+x_10 = lean_ctor_get(x_9, 1);
+lean_inc(x_10);
+lean_dec(x_9);
+x_11 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
+x_12 = lean_string_dec_eq(x_10, x_11);
+lean_dec(x_10);
+if (x_12 == 0)
+{
+lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
+x_13 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
+x_14 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_13, x_5);
+x_15 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
+x_16 = l_Lean_Parser_ParserState_mkTrailingNode(x_14, x_15, x_4);
 lean_dec(x_4);
-return x_27;
+return x_16;
+}
+else
+{
+lean_object* x_17; lean_object* x_18; 
+lean_dec(x_5);
+x_17 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
+x_18 = l_Lean_Parser_ParserState_mkTrailingNode(x_6, x_17, x_4);
+lean_dec(x_4);
+return x_18;
 }
 }
 else
 {
-lean_object* x_28; lean_object* x_29; 
-lean_dec(x_5);
-lean_dec(x_1);
-x_28 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
-x_29 = l_Lean_Parser_ParserState_mkTrailingNode(x_2, x_28, x_4);
+lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+lean_dec(x_9);
+x_19 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
+x_20 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_19, x_5);
+x_21 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
+x_22 = l_Lean_Parser_ParserState_mkTrailingNode(x_20, x_21, x_4);
 lean_dec(x_4);
-return x_29;
+return x_22;
+}
+}
+else
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
+lean_dec(x_7);
+x_23 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
+x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_23, x_5);
+x_25 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
+x_26 = l_Lean_Parser_ParserState_mkTrailingNode(x_24, x_25, x_4);
+lean_dec(x_4);
+return x_26;
 }
 }
 }
@@ -4722,23 +4661,13 @@ lean_object* _init_l_Lean_Parser_Syntax_many1___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_epsilonInfo;
-x_2 = l_Lean_Parser_Syntax_many1___closed__1;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Syntax_many1___closed__3() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
-x_2 = l_Lean_Parser_Syntax_many1___closed__2;
+x_2 = l_Lean_Parser_Syntax_many1___closed__1;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Syntax_many1___closed__4() {
+lean_object* _init_l_Lean_Parser_Syntax_many1___closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -4746,12 +4675,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Syntax_many1___elambda__1___boxed
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Syntax_many1___closed__5() {
+lean_object* _init_l_Lean_Parser_Syntax_many1___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Syntax_many1___closed__3;
-x_2 = l_Lean_Parser_Syntax_many1___closed__4;
+x_1 = l_Lean_Parser_Syntax_many1___closed__2;
+x_2 = l_Lean_Parser_Syntax_many1___closed__3;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -4762,7 +4691,7 @@ lean_object* _init_l_Lean_Parser_Syntax_many1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Syntax_many1___closed__5;
+x_1 = l_Lean_Parser_Syntax_many1___closed__4;
 return x_1;
 }
 }
@@ -4800,97 +4729,93 @@ return x_3;
 lean_object* l_Lean_Parser_Syntax_orelse___elambda__1___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
 x_3 = lean_ctor_get(x_2, 0);
 lean_inc(x_3);
 x_4 = lean_array_get_size(x_3);
 lean_dec(x_3);
-x_5 = lean_ctor_get(x_2, 3);
-lean_inc(x_5);
-if (lean_obj_tag(x_5) == 0)
-{
-lean_object* x_6; lean_object* x_7; lean_object* x_8; 
-x_6 = lean_ctor_get(x_2, 1);
-lean_inc(x_6);
+x_15 = lean_ctor_get(x_2, 1);
+lean_inc(x_15);
 lean_inc(x_1);
-x_7 = l_Lean_Parser_tokenFn(x_1, x_2);
-x_8 = lean_ctor_get(x_7, 3);
-lean_inc(x_8);
-if (lean_obj_tag(x_8) == 0)
+x_16 = l_Lean_Parser_tokenFn(x_1, x_2);
+x_17 = lean_ctor_get(x_16, 3);
+lean_inc(x_17);
+if (lean_obj_tag(x_17) == 0)
 {
-lean_object* x_9; lean_object* x_10; 
-x_9 = lean_ctor_get(x_7, 0);
-lean_inc(x_9);
-x_10 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_9);
-lean_dec(x_9);
-if (lean_obj_tag(x_10) == 2)
+lean_object* x_18; lean_object* x_19; 
+x_18 = lean_ctor_get(x_16, 0);
+lean_inc(x_18);
+x_19 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_18);
+lean_dec(x_18);
+if (lean_obj_tag(x_19) == 2)
 {
-lean_object* x_11; lean_object* x_12; uint8_t x_13; 
-x_11 = lean_ctor_get(x_10, 1);
-lean_inc(x_11);
-lean_dec(x_10);
-x_12 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__2;
-x_13 = lean_string_dec_eq(x_11, x_12);
-lean_dec(x_11);
-if (x_13 == 0)
+lean_object* x_20; lean_object* x_21; uint8_t x_22; 
+x_20 = lean_ctor_get(x_19, 1);
+lean_inc(x_20);
+lean_dec(x_19);
+x_21 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__2;
+x_22 = lean_string_dec_eq(x_20, x_21);
+lean_dec(x_20);
+if (x_22 == 0)
 {
-lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
-lean_dec(x_1);
-x_14 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
-x_15 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_14, x_6);
-x_16 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
-x_17 = l_Lean_Parser_ParserState_mkTrailingNode(x_15, x_16, x_4);
-lean_dec(x_4);
-return x_17;
-}
-else
-{
-lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
-lean_dec(x_6);
-x_18 = l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__4;
-x_19 = lean_unsigned_to_nat(1u);
-x_20 = l_Lean_Parser_categoryParserFn(x_18, x_19, x_1, x_7);
-x_21 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
-x_22 = l_Lean_Parser_ParserState_mkTrailingNode(x_20, x_21, x_4);
-lean_dec(x_4);
-return x_22;
-}
-}
-else
-{
-lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
-lean_dec(x_10);
-lean_dec(x_1);
+lean_object* x_23; lean_object* x_24; 
 x_23 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
-x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_23, x_6);
-x_25 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
-x_26 = l_Lean_Parser_ParserState_mkTrailingNode(x_24, x_25, x_4);
-lean_dec(x_4);
-return x_26;
+x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_23, x_15);
+x_5 = x_24;
+goto block_14;
+}
+else
+{
+lean_dec(x_15);
+x_5 = x_16;
+goto block_14;
 }
 }
 else
 {
-lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; 
-lean_dec(x_8);
-lean_dec(x_1);
+lean_object* x_25; lean_object* x_26; 
+lean_dec(x_19);
+x_25 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
+x_26 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_25, x_15);
+x_5 = x_26;
+goto block_14;
+}
+}
+else
+{
+lean_object* x_27; lean_object* x_28; 
+lean_dec(x_17);
 x_27 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
-x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_27, x_6);
-x_29 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
-x_30 = l_Lean_Parser_ParserState_mkTrailingNode(x_28, x_29, x_4);
-lean_dec(x_4);
-return x_30;
+x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_27, x_15);
+x_5 = x_28;
+goto block_14;
 }
+block_14:
+{
+lean_object* x_6; 
+x_6 = lean_ctor_get(x_5, 3);
+lean_inc(x_6);
+if (lean_obj_tag(x_6) == 0)
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_7 = l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__4;
+x_8 = lean_unsigned_to_nat(1u);
+x_9 = l_Lean_Parser_categoryParserFn(x_7, x_8, x_1, x_5);
+x_10 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
+x_11 = l_Lean_Parser_ParserState_mkTrailingNode(x_9, x_10, x_4);
+lean_dec(x_4);
+return x_11;
 }
 else
 {
-lean_object* x_31; lean_object* x_32; 
-lean_dec(x_5);
+lean_object* x_12; lean_object* x_13; 
+lean_dec(x_6);
 lean_dec(x_1);
-x_31 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
-x_32 = l_Lean_Parser_ParserState_mkTrailingNode(x_2, x_31, x_4);
+x_12 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
+x_13 = l_Lean_Parser_ParserState_mkTrailingNode(x_5, x_12, x_4);
 lean_dec(x_4);
-return x_32;
+return x_13;
+}
 }
 }
 }
@@ -4929,23 +4854,13 @@ lean_object* _init_l_Lean_Parser_Syntax_orelse___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_epsilonInfo;
-x_2 = l_Lean_Parser_Syntax_orelse___closed__2;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Syntax_orelse___closed__4() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
-x_2 = l_Lean_Parser_Syntax_orelse___closed__3;
+x_2 = l_Lean_Parser_Syntax_orelse___closed__2;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Syntax_orelse___closed__5() {
+lean_object* _init_l_Lean_Parser_Syntax_orelse___closed__4() {
 _start:
 {
 lean_object* x_1; 
@@ -4953,12 +4868,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Syntax_orelse___elambda__1___boxe
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Syntax_orelse___closed__6() {
+lean_object* _init_l_Lean_Parser_Syntax_orelse___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Syntax_orelse___closed__4;
-x_2 = l_Lean_Parser_Syntax_orelse___closed__5;
+x_1 = l_Lean_Parser_Syntax_orelse___closed__3;
+x_2 = l_Lean_Parser_Syntax_orelse___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);
@@ -4969,7 +4884,7 @@ lean_object* _init_l_Lean_Parser_Syntax_orelse() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Syntax_orelse___closed__6;
+x_1 = l_Lean_Parser_Syntax_orelse___closed__5;
 return x_1;
 }
 }
@@ -13622,8 +13537,6 @@ l_Lean_Parser_Syntax_optional___closed__3 = _init_l_Lean_Parser_Syntax_optional_
 lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__3);
 l_Lean_Parser_Syntax_optional___closed__4 = _init_l_Lean_Parser_Syntax_optional___closed__4();
 lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__4);
-l_Lean_Parser_Syntax_optional___closed__5 = _init_l_Lean_Parser_Syntax_optional___closed__5();
-lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__5);
 l_Lean_Parser_Syntax_optional = _init_l_Lean_Parser_Syntax_optional();
 lean_mark_persistent(l_Lean_Parser_Syntax_optional);
 res = l___regBuiltinParser_Lean_Parser_Syntax_optional(lean_io_mk_world());
@@ -13662,8 +13575,6 @@ l_Lean_Parser_Syntax_many1___closed__3 = _init_l_Lean_Parser_Syntax_many1___clos
 lean_mark_persistent(l_Lean_Parser_Syntax_many1___closed__3);
 l_Lean_Parser_Syntax_many1___closed__4 = _init_l_Lean_Parser_Syntax_many1___closed__4();
 lean_mark_persistent(l_Lean_Parser_Syntax_many1___closed__4);
-l_Lean_Parser_Syntax_many1___closed__5 = _init_l_Lean_Parser_Syntax_many1___closed__5();
-lean_mark_persistent(l_Lean_Parser_Syntax_many1___closed__5);
 l_Lean_Parser_Syntax_many1 = _init_l_Lean_Parser_Syntax_many1();
 lean_mark_persistent(l_Lean_Parser_Syntax_many1);
 res = l___regBuiltinParser_Lean_Parser_Syntax_many1(lean_io_mk_world());
@@ -13681,8 +13592,6 @@ l_Lean_Parser_Syntax_orelse___closed__4 = _init_l_Lean_Parser_Syntax_orelse___cl
 lean_mark_persistent(l_Lean_Parser_Syntax_orelse___closed__4);
 l_Lean_Parser_Syntax_orelse___closed__5 = _init_l_Lean_Parser_Syntax_orelse___closed__5();
 lean_mark_persistent(l_Lean_Parser_Syntax_orelse___closed__5);
-l_Lean_Parser_Syntax_orelse___closed__6 = _init_l_Lean_Parser_Syntax_orelse___closed__6();
-lean_mark_persistent(l_Lean_Parser_Syntax_orelse___closed__6);
 l_Lean_Parser_Syntax_orelse = _init_l_Lean_Parser_Syntax_orelse();
 lean_mark_persistent(l_Lean_Parser_Syntax_orelse);
 res = l___regBuiltinParser_Lean_Parser_Syntax_orelse(lean_io_mk_world());
diff --git a/stage0/stdlib/Init/Lean/Parser/Tactic.c b/stage0/stdlib/Init/Lean/Parser/Tactic.c
index e3ce83e3f5..d439dd236b 100644
--- a/stage0/stdlib/Init/Lean/Parser/Tactic.c
+++ b/stage0/stdlib/Init/Lean/Parser/Tactic.c
@@ -79,7 +79,6 @@ lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___closed__7;
 lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__1;
-lean_object* l_Lean_Parser_Tactic_orelse___closed__7;
 lean_object* l_Lean_Parser_regTacticParserAttribute___closed__1;
 lean_object* l_Lean_Parser_Tactic_underscore(uint8_t);
 lean_object* l_Lean_Parser_Tactic_traceState___elambda__1___closed__4;
@@ -289,7 +288,6 @@ lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__4;
 lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_underscoreFn___rarg___closed__2;
 lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__6;
-extern lean_object* l_Lean_Parser_epsilonInfo;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___closed__4;
 lean_object* l_Lean_Parser_Tactic_assumption___closed__3;
 lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__7;
@@ -4884,97 +4882,93 @@ return x_3;
 lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
 x_3 = lean_ctor_get(x_2, 0);
 lean_inc(x_3);
 x_4 = lean_array_get_size(x_3);
 lean_dec(x_3);
-x_5 = lean_ctor_get(x_2, 3);
-lean_inc(x_5);
-if (lean_obj_tag(x_5) == 0)
-{
-lean_object* x_6; lean_object* x_7; lean_object* x_8; 
-x_6 = lean_ctor_get(x_2, 1);
-lean_inc(x_6);
+x_15 = lean_ctor_get(x_2, 1);
+lean_inc(x_15);
 lean_inc(x_1);
-x_7 = l_Lean_Parser_tokenFn(x_1, x_2);
-x_8 = lean_ctor_get(x_7, 3);
-lean_inc(x_8);
-if (lean_obj_tag(x_8) == 0)
+x_16 = l_Lean_Parser_tokenFn(x_1, x_2);
+x_17 = lean_ctor_get(x_16, 3);
+lean_inc(x_17);
+if (lean_obj_tag(x_17) == 0)
 {
-lean_object* x_9; lean_object* x_10; 
-x_9 = lean_ctor_get(x_7, 0);
-lean_inc(x_9);
-x_10 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_9);
-lean_dec(x_9);
-if (lean_obj_tag(x_10) == 2)
+lean_object* x_18; lean_object* x_19; 
+x_18 = lean_ctor_get(x_16, 0);
+lean_inc(x_18);
+x_19 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_18);
+lean_dec(x_18);
+if (lean_obj_tag(x_19) == 2)
 {
-lean_object* x_11; lean_object* x_12; uint8_t x_13; 
-x_11 = lean_ctor_get(x_10, 1);
-lean_inc(x_11);
-lean_dec(x_10);
-x_12 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__2;
-x_13 = lean_string_dec_eq(x_11, x_12);
-lean_dec(x_11);
-if (x_13 == 0)
+lean_object* x_20; lean_object* x_21; uint8_t x_22; 
+x_20 = lean_ctor_get(x_19, 1);
+lean_inc(x_20);
+lean_dec(x_19);
+x_21 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__2;
+x_22 = lean_string_dec_eq(x_20, x_21);
+lean_dec(x_20);
+if (x_22 == 0)
 {
-lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
-lean_dec(x_1);
-x_14 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
-x_15 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_14, x_6);
-x_16 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
-x_17 = l_Lean_Parser_ParserState_mkTrailingNode(x_15, x_16, x_4);
-lean_dec(x_4);
-return x_17;
-}
-else
-{
-lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
-lean_dec(x_6);
-x_18 = l_Lean_Parser_regBuiltinTacticParserAttr___closed__4;
-x_19 = lean_unsigned_to_nat(1u);
-x_20 = l_Lean_Parser_categoryParserFn(x_18, x_19, x_1, x_7);
-x_21 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
-x_22 = l_Lean_Parser_ParserState_mkTrailingNode(x_20, x_21, x_4);
-lean_dec(x_4);
-return x_22;
-}
-}
-else
-{
-lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
-lean_dec(x_10);
-lean_dec(x_1);
+lean_object* x_23; lean_object* x_24; 
 x_23 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
-x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_23, x_6);
-x_25 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
-x_26 = l_Lean_Parser_ParserState_mkTrailingNode(x_24, x_25, x_4);
-lean_dec(x_4);
-return x_26;
+x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_23, x_15);
+x_5 = x_24;
+goto block_14;
+}
+else
+{
+lean_dec(x_15);
+x_5 = x_16;
+goto block_14;
 }
 }
 else
 {
-lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; 
-lean_dec(x_8);
-lean_dec(x_1);
+lean_object* x_25; lean_object* x_26; 
+lean_dec(x_19);
+x_25 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
+x_26 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_25, x_15);
+x_5 = x_26;
+goto block_14;
+}
+}
+else
+{
+lean_object* x_27; lean_object* x_28; 
+lean_dec(x_17);
 x_27 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
-x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_27, x_6);
-x_29 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
-x_30 = l_Lean_Parser_ParserState_mkTrailingNode(x_28, x_29, x_4);
-lean_dec(x_4);
-return x_30;
+x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_27, x_15);
+x_5 = x_28;
+goto block_14;
 }
+block_14:
+{
+lean_object* x_6; 
+x_6 = lean_ctor_get(x_5, 3);
+lean_inc(x_6);
+if (lean_obj_tag(x_6) == 0)
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_7 = l_Lean_Parser_regBuiltinTacticParserAttr___closed__4;
+x_8 = lean_unsigned_to_nat(1u);
+x_9 = l_Lean_Parser_categoryParserFn(x_7, x_8, x_1, x_5);
+x_10 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
+x_11 = l_Lean_Parser_ParserState_mkTrailingNode(x_9, x_10, x_4);
+lean_dec(x_4);
+return x_11;
 }
 else
 {
-lean_object* x_31; lean_object* x_32; 
-lean_dec(x_5);
+lean_object* x_12; lean_object* x_13; 
+lean_dec(x_6);
 lean_dec(x_1);
-x_31 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
-x_32 = l_Lean_Parser_ParserState_mkTrailingNode(x_2, x_31, x_4);
+x_12 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
+x_13 = l_Lean_Parser_ParserState_mkTrailingNode(x_5, x_12, x_4);
 lean_dec(x_4);
-return x_32;
+return x_13;
+}
 }
 }
 }
@@ -5023,23 +5017,13 @@ lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_epsilonInfo;
-x_2 = l_Lean_Parser_Tactic_orelse___closed__3;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__5() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
-x_2 = l_Lean_Parser_Tactic_orelse___closed__4;
+x_2 = l_Lean_Parser_Tactic_orelse___closed__3;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__6() {
+lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__5() {
 _start:
 {
 lean_object* x_1; 
@@ -5047,12 +5031,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_orelse___elambda__1___boxe
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__7() {
+lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_orelse___closed__5;
-x_2 = l_Lean_Parser_Tactic_orelse___closed__6;
+x_1 = l_Lean_Parser_Tactic_orelse___closed__4;
+x_2 = l_Lean_Parser_Tactic_orelse___closed__5;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -5063,7 +5047,7 @@ lean_object* _init_l_Lean_Parser_Tactic_orelse() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Tactic_orelse___closed__7;
+x_1 = l_Lean_Parser_Tactic_orelse___closed__6;
 return x_1;
 }
 }
@@ -6281,8 +6265,6 @@ l_Lean_Parser_Tactic_orelse___closed__5 = _init_l_Lean_Parser_Tactic_orelse___cl
 lean_mark_persistent(l_Lean_Parser_Tactic_orelse___closed__5);
 l_Lean_Parser_Tactic_orelse___closed__6 = _init_l_Lean_Parser_Tactic_orelse___closed__6();
 lean_mark_persistent(l_Lean_Parser_Tactic_orelse___closed__6);
-l_Lean_Parser_Tactic_orelse___closed__7 = _init_l_Lean_Parser_Tactic_orelse___closed__7();
-lean_mark_persistent(l_Lean_Parser_Tactic_orelse___closed__7);
 l_Lean_Parser_Tactic_orelse = _init_l_Lean_Parser_Tactic_orelse();
 lean_mark_persistent(l_Lean_Parser_Tactic_orelse);
 res = l___regBuiltinParser_Lean_Parser_Tactic_orelse(lean_io_mk_world());
diff --git a/stage0/stdlib/Init/Lean/Parser/Term.c b/stage0/stdlib/Init/Lean/Parser/Term.c
index df1c1a372e..1924a48955 100644
--- a/stage0/stdlib/Init/Lean/Parser/Term.c
+++ b/stage0/stdlib/Init/Lean/Parser/Term.c
@@ -35,7 +35,7 @@ lean_object* l_Lean_Parser_Term_letIdDecl;
 lean_object* l_Lean_Parser_Term_heq___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Term_matchAlts___closed__3;
-lean_object* l_Lean_Parser_Term_infixL___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Term_infixL___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_dollar___elambda__1___boxed(lean_object*);
 lean_object* l___regBuiltinParser_Lean_Parser_Term_iff(lean_object*);
 lean_object* l___regBuiltinParser_Lean_Parser_Term_suffices(lean_object*);
@@ -155,7 +155,6 @@ lean_object* l_Lean_Parser_Term_subtype___closed__6;
 lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__7;
 lean_object* l___regBuiltinParser_Lean_Parser_Term_append(lean_object*);
 lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__5;
-lean_object* l_Lean_Parser_Term_proj___closed__10;
 lean_object* l_Lean_Parser_Term_haveAssign___closed__2;
 lean_object* l_Lean_Parser_Term_forall___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_structInstSource___elambda__1(lean_object*, lean_object*, lean_object*);
@@ -329,7 +328,6 @@ lean_object* l_Lean_Parser_Term_or___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_have___elambda__1___closed__11;
 lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__12;
 lean_object* l_Lean_Parser_Term_match__syntax___closed__3;
-lean_object* l_Lean_Parser_Term_arrayRef___closed__8;
 extern lean_object* l_Lean_Parser_symbolNoWsFn___closed__1;
 lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Term_bor___elambda__1(lean_object*, lean_object*, lean_object*);
@@ -518,7 +516,7 @@ lean_object* l_Lean_Parser_Term_subtype___elambda__1___closed__2;
 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_infixR___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Term_infixR___elambda__1(lean_object*, 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;
@@ -664,7 +662,6 @@ lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Term_tupleTail___closed__1;
 lean_object* l_Lean_Parser_Term_not___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_le___elambda__1___closed__5;
-lean_object* l_Lean_Parser_Term_sortApp___closed__6;
 lean_object* l_Lean_Parser_Term_structInstSource___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Term_letEqnsDecl___closed__3;
 lean_object* l_Lean_Parser_Term_str___elambda__1(lean_object*, lean_object*, lean_object*);
@@ -945,7 +942,6 @@ lean_object* l_Lean_Parser_Term_append___closed__1;
 lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__4;
 extern lean_object* l_List_reprAux___main___rarg___closed__1;
-lean_object* l_Lean_Parser_Term_dollar___closed__7;
 lean_object* l_Lean_Parser_Term_id___closed__6;
 lean_object* l_Lean_Parser_Term_map___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_namedArgument___elambda__1(lean_object*, lean_object*, lean_object*);
@@ -1572,9 +1568,7 @@ lean_object* l_Lean_Parser_Term_parser_x21___closed__2;
 lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_typeSpec___closed__4;
 lean_object* l_Lean_Parser_Term_mapRev___elambda__1___closed__1;
-lean_object* l_Lean_Parser_Term_app___closed__6;
 lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___rarg___closed__1;
-lean_object* l_Lean_Parser_Term_dollarProj___closed__6;
 lean_object* l_Lean_Parser_Term_hole;
 lean_object* l_Lean_Parser_Term_app___closed__1;
 lean_object* l_Lean_Parser_Term_emptyC___closed__5;
@@ -1886,13 +1880,12 @@ 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_unicodeInfixR___elambda__1(lean_object*, 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_unicodeInfixL___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Term_unicodeInfixL___elambda__1(lean_object*, 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_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(lean_object*);
-lean_object* l_Lean_Parser_Term_where___closed__10;
 lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Term_namedArgument___closed__4;
 lean_object* l_Lean_Parser_Term_dollar___closed__2;
@@ -2100,32 +2093,35 @@ lean_dec(x_1);
 return x_2;
 }
 }
-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_Term_unicodeInfixR___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
-lean_object* x_5; 
-x_5 = lean_ctor_get(x_4, 3);
-lean_inc(x_5);
-if (lean_obj_tag(x_5) == 0)
+lean_object* x_6; lean_object* x_7; 
+lean_inc(x_4);
+lean_inc(x_3);
+x_6 = lean_apply_3(x_1, x_3, x_4, x_5);
+x_7 = lean_ctor_get(x_6, 3);
+lean_inc(x_7);
+if (lean_obj_tag(x_7) == 0)
 {
-lean_object* x_6; 
-x_6 = lean_apply_3(x_1, x_2, x_3, x_4);
-return x_6;
+lean_object* x_8; 
+x_8 = lean_apply_3(x_2, x_3, x_4, x_6);
+return x_8;
 }
 else
 {
-lean_dec(x_5);
+lean_dec(x_7);
+lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
-lean_dec(x_1);
-return x_4;
+return x_6;
 }
 }
 }
 lean_object* l_Lean_Parser_Term_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; 
+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_inc(x_3);
 x_4 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_4, 0, x_3);
@@ -2151,17 +2147,13 @@ x_15 = l_Lean_Parser_andthenInfo(x_7, x_14);
 x_16 = lean_alloc_closure((void*)(l_Lean_Parser_categoryParser___elambda__1___rarg___boxed), 5, 2);
 lean_closure_set(x_16, 0, x_12);
 lean_closure_set(x_16, 1, x_10);
-x_17 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
+x_17 = lean_alloc_closure((void*)(l_Lean_Parser_Term_unicodeInfixR___elambda__1), 5, 2);
 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);
-lean_closure_set(x_20, 0, x_17);
-x_21 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_21, 0, x_19);
-lean_ctor_set(x_21, 1, x_20);
-return x_21;
+x_18 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_18, 0, x_15);
+lean_ctor_set(x_18, 1, x_17);
+return x_18;
 }
 }
 lean_object* l_Lean_Parser_Term_unicodeInfixR___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@@ -2174,32 +2166,35 @@ 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_Term_infixR___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
-lean_object* x_5; 
-x_5 = lean_ctor_get(x_4, 3);
-lean_inc(x_5);
-if (lean_obj_tag(x_5) == 0)
+lean_object* x_6; lean_object* x_7; 
+lean_inc(x_4);
+lean_inc(x_3);
+x_6 = lean_apply_3(x_1, x_3, x_4, x_5);
+x_7 = lean_ctor_get(x_6, 3);
+lean_inc(x_7);
+if (lean_obj_tag(x_7) == 0)
 {
-lean_object* x_6; 
-x_6 = lean_apply_3(x_1, x_2, x_3, x_4);
-return x_6;
+lean_object* x_8; 
+x_8 = lean_apply_3(x_2, x_3, x_4, x_6);
+return x_8;
 }
 else
 {
-lean_dec(x_5);
+lean_dec(x_7);
+lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
-lean_dec(x_1);
-return x_4;
+return x_6;
 }
 }
 }
 lean_object* l_Lean_Parser_Term_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; 
+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_inc(x_2);
 x_3 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_3, 0, x_2);
@@ -2222,17 +2217,13 @@ x_13 = l_Lean_Parser_andthenInfo(x_5, x_12);
 x_14 = lean_alloc_closure((void*)(l_Lean_Parser_categoryParser___elambda__1___rarg___boxed), 5, 2);
 lean_closure_set(x_14, 0, x_10);
 lean_closure_set(x_14, 1, x_8);
-x_15 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
+x_15 = lean_alloc_closure((void*)(l_Lean_Parser_Term_infixR___elambda__1), 5, 2);
 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);
-lean_closure_set(x_18, 0, x_15);
-x_19 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_19, 0, x_17);
-lean_ctor_set(x_19, 1, x_18);
-return x_19;
+x_16 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_16, 0, x_13);
+lean_ctor_set(x_16, 1, x_15);
+return x_16;
 }
 }
 lean_object* l_Lean_Parser_Term_infixR___boxed(lean_object* x_1, lean_object* x_2) {
@@ -2244,32 +2235,35 @@ 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_Term_unicodeInfixL___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
-lean_object* x_5; 
-x_5 = lean_ctor_get(x_4, 3);
-lean_inc(x_5);
-if (lean_obj_tag(x_5) == 0)
+lean_object* x_6; lean_object* x_7; 
+lean_inc(x_4);
+lean_inc(x_3);
+x_6 = lean_apply_3(x_1, x_3, x_4, x_5);
+x_7 = lean_ctor_get(x_6, 3);
+lean_inc(x_7);
+if (lean_obj_tag(x_7) == 0)
 {
-lean_object* x_6; 
-x_6 = lean_apply_3(x_1, x_2, x_3, x_4);
-return x_6;
+lean_object* x_8; 
+x_8 = lean_apply_3(x_2, x_3, x_4, x_6);
+return x_8;
 }
 else
 {
-lean_dec(x_5);
+lean_dec(x_7);
+lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
-lean_dec(x_1);
-return x_4;
+return x_6;
 }
 }
 }
 lean_object* l_Lean_Parser_Term_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; 
+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_inc(x_3);
 x_4 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_4, 0, x_3);
@@ -2292,17 +2286,13 @@ x_13 = l_Lean_Parser_andthenInfo(x_7, x_12);
 x_14 = lean_alloc_closure((void*)(l_Lean_Parser_categoryParser___elambda__1___rarg___boxed), 5, 2);
 lean_closure_set(x_14, 0, x_10);
 lean_closure_set(x_14, 1, x_3);
-x_15 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
+x_15 = lean_alloc_closure((void*)(l_Lean_Parser_Term_unicodeInfixL___elambda__1), 5, 2);
 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);
-lean_closure_set(x_18, 0, x_15);
-x_19 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_19, 0, x_17);
-lean_ctor_set(x_19, 1, x_18);
-return x_19;
+x_16 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_16, 0, x_13);
+lean_ctor_set(x_16, 1, x_15);
+return x_16;
 }
 }
 lean_object* l_Lean_Parser_Term_unicodeInfixL___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@@ -2315,32 +2305,35 @@ 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_Term_infixL___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
-lean_object* x_5; 
-x_5 = lean_ctor_get(x_4, 3);
-lean_inc(x_5);
-if (lean_obj_tag(x_5) == 0)
+lean_object* x_6; lean_object* x_7; 
+lean_inc(x_4);
+lean_inc(x_3);
+x_6 = lean_apply_3(x_1, x_3, x_4, x_5);
+x_7 = lean_ctor_get(x_6, 3);
+lean_inc(x_7);
+if (lean_obj_tag(x_7) == 0)
 {
-lean_object* x_6; 
-x_6 = lean_apply_3(x_1, x_2, x_3, x_4);
-return x_6;
+lean_object* x_8; 
+x_8 = lean_apply_3(x_2, x_3, x_4, x_6);
+return x_8;
 }
 else
 {
-lean_dec(x_5);
+lean_dec(x_7);
+lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
-lean_dec(x_1);
-return x_4;
+return x_6;
 }
 }
 }
 lean_object* l_Lean_Parser_Term_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; 
+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_inc(x_2);
 x_3 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_3, 0, x_2);
@@ -2360,17 +2353,13 @@ x_11 = l_Lean_Parser_andthenInfo(x_5, x_10);
 x_12 = lean_alloc_closure((void*)(l_Lean_Parser_categoryParser___elambda__1___rarg___boxed), 5, 2);
 lean_closure_set(x_12, 0, x_8);
 lean_closure_set(x_12, 1, x_2);
-x_13 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
+x_13 = lean_alloc_closure((void*)(l_Lean_Parser_Term_infixL___elambda__1), 5, 2);
 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);
-lean_closure_set(x_16, 0, x_13);
-x_17 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_17, 0, x_15);
-lean_ctor_set(x_17, 1, x_16);
-return x_17;
+x_14 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_14, 0, x_11);
+lean_ctor_set(x_14, 1, x_13);
+return x_14;
 }
 }
 lean_object* l_Lean_Parser_Term_infixL___boxed(lean_object* x_1, lean_object* x_2) {
@@ -30848,112 +30837,96 @@ return x_17;
 lean_object* l_Lean_Parser_Term_app___elambda__1(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_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
 x_4 = lean_ctor_get(x_3, 0);
 lean_inc(x_4);
 x_5 = lean_array_get_size(x_4);
 lean_dec(x_4);
-x_6 = lean_ctor_get(x_3, 3);
+x_6 = lean_ctor_get(x_3, 1);
 lean_inc(x_6);
-if (lean_obj_tag(x_6) == 0)
-{
-lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-x_7 = lean_ctor_get(x_3, 1);
-lean_inc(x_7);
-x_8 = lean_unsigned_to_nat(0u);
+x_7 = lean_unsigned_to_nat(0u);
 lean_inc(x_2);
-x_9 = l_Lean_Parser_Term_namedArgument___elambda__1(x_8, x_2, x_3);
-x_10 = lean_ctor_get(x_9, 3);
-lean_inc(x_10);
-if (lean_obj_tag(x_10) == 0)
+x_8 = l_Lean_Parser_Term_namedArgument___elambda__1(x_7, x_2, x_3);
+x_9 = lean_ctor_get(x_8, 3);
+lean_inc(x_9);
+if (lean_obj_tag(x_9) == 0)
 {
-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_dec(x_7);
-x_11 = 1;
-x_12 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_app___elambda__1___spec__1(x_11, x_1, x_2, x_9);
-x_13 = l_Lean_nullKind;
+uint8_t x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
+lean_dec(x_6);
+x_10 = 1;
+x_11 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_app___elambda__1___spec__1(x_10, x_1, x_2, x_8);
+x_12 = l_Lean_nullKind;
 lean_inc(x_5);
-x_14 = l_Lean_Parser_ParserState_mkNode(x_12, x_13, x_5);
-x_15 = l_Lean_mkAppStx___closed__8;
-x_16 = l_Lean_Parser_ParserState_mkTrailingNode(x_14, x_15, x_5);
+x_13 = l_Lean_Parser_ParserState_mkNode(x_11, x_12, x_5);
+x_14 = l_Lean_mkAppStx___closed__8;
+x_15 = l_Lean_Parser_ParserState_mkTrailingNode(x_13, x_14, x_5);
 lean_dec(x_5);
-return x_16;
+return x_15;
 }
 else
 {
-lean_object* x_17; lean_object* x_18; uint8_t x_19; 
-x_17 = lean_ctor_get(x_10, 0);
+lean_object* x_16; lean_object* x_17; uint8_t x_18; 
+x_16 = lean_ctor_get(x_9, 0);
+lean_inc(x_16);
+lean_dec(x_9);
+x_17 = lean_ctor_get(x_8, 1);
 lean_inc(x_17);
-lean_dec(x_10);
-x_18 = lean_ctor_get(x_9, 1);
-lean_inc(x_18);
-x_19 = lean_nat_dec_eq(x_18, x_7);
-lean_dec(x_18);
-if (x_19 == 0)
-{
-lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
+x_18 = lean_nat_dec_eq(x_17, x_6);
 lean_dec(x_17);
-lean_dec(x_7);
-lean_dec(x_2);
-x_20 = l_Lean_nullKind;
-lean_inc(x_5);
-x_21 = l_Lean_Parser_ParserState_mkNode(x_9, x_20, x_5);
-x_22 = l_Lean_mkAppStx___closed__8;
-x_23 = l_Lean_Parser_ParserState_mkTrailingNode(x_21, x_22, x_5);
-lean_dec(x_5);
-return x_23;
-}
-else
+if (x_18 == 0)
 {
-lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; 
-lean_inc(x_7);
-x_24 = l_Lean_Parser_ParserState_restore(x_9, x_5, x_7);
-x_25 = l_Lean_Parser_termParser___closed__2;
-x_26 = l_Lean_Parser_appPrec;
-lean_inc(x_2);
-x_27 = l_Lean_Parser_categoryParserFn(x_25, x_26, x_2, x_24);
-x_28 = l_Lean_Parser_mergeOrElseErrors(x_27, x_17, x_7);
-lean_dec(x_7);
-x_29 = lean_ctor_get(x_28, 3);
-lean_inc(x_29);
-if (lean_obj_tag(x_29) == 0)
-{
-uint8_t x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; 
-x_30 = 1;
-x_31 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_app___elambda__1___spec__1(x_30, x_1, x_2, x_28);
-x_32 = l_Lean_nullKind;
-lean_inc(x_5);
-x_33 = l_Lean_Parser_ParserState_mkNode(x_31, x_32, x_5);
-x_34 = l_Lean_mkAppStx___closed__8;
-x_35 = l_Lean_Parser_ParserState_mkTrailingNode(x_33, x_34, x_5);
-lean_dec(x_5);
-return x_35;
-}
-else
-{
-lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; 
-lean_dec(x_29);
-lean_dec(x_2);
-x_36 = l_Lean_nullKind;
-lean_inc(x_5);
-x_37 = l_Lean_Parser_ParserState_mkNode(x_28, x_36, x_5);
-x_38 = l_Lean_mkAppStx___closed__8;
-x_39 = l_Lean_Parser_ParserState_mkTrailingNode(x_37, x_38, x_5);
-lean_dec(x_5);
-return x_39;
-}
-}
-}
-}
-else
-{
-lean_object* x_40; lean_object* x_41; 
+lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+lean_dec(x_16);
 lean_dec(x_6);
 lean_dec(x_2);
-x_40 = l_Lean_mkAppStx___closed__8;
-x_41 = l_Lean_Parser_ParserState_mkTrailingNode(x_3, x_40, x_5);
+x_19 = l_Lean_nullKind;
+lean_inc(x_5);
+x_20 = l_Lean_Parser_ParserState_mkNode(x_8, x_19, x_5);
+x_21 = l_Lean_mkAppStx___closed__8;
+x_22 = l_Lean_Parser_ParserState_mkTrailingNode(x_20, x_21, x_5);
 lean_dec(x_5);
-return x_41;
+return x_22;
+}
+else
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+lean_inc(x_6);
+x_23 = l_Lean_Parser_ParserState_restore(x_8, x_5, x_6);
+x_24 = l_Lean_Parser_termParser___closed__2;
+x_25 = l_Lean_Parser_appPrec;
+lean_inc(x_2);
+x_26 = l_Lean_Parser_categoryParserFn(x_24, x_25, x_2, x_23);
+x_27 = l_Lean_Parser_mergeOrElseErrors(x_26, x_16, x_6);
+lean_dec(x_6);
+x_28 = lean_ctor_get(x_27, 3);
+lean_inc(x_28);
+if (lean_obj_tag(x_28) == 0)
+{
+uint8_t x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; 
+x_29 = 1;
+x_30 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_app___elambda__1___spec__1(x_29, x_1, x_2, x_27);
+x_31 = l_Lean_nullKind;
+lean_inc(x_5);
+x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_5);
+x_33 = l_Lean_mkAppStx___closed__8;
+x_34 = l_Lean_Parser_ParserState_mkTrailingNode(x_32, x_33, x_5);
+lean_dec(x_5);
+return x_34;
+}
+else
+{
+lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; 
+lean_dec(x_28);
+lean_dec(x_2);
+x_35 = l_Lean_nullKind;
+lean_inc(x_5);
+x_36 = l_Lean_Parser_ParserState_mkNode(x_27, x_35, x_5);
+x_37 = l_Lean_mkAppStx___closed__8;
+x_38 = l_Lean_Parser_ParserState_mkTrailingNode(x_36, x_37, x_5);
+lean_dec(x_5);
+return x_38;
+}
+}
 }
 }
 }
@@ -30986,23 +30959,13 @@ lean_object* _init_l_Lean_Parser_Term_app___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_epsilonInfo;
-x_2 = l_Lean_Parser_Term_app___closed__2;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Term_app___closed__4() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_mkAppStx___closed__8;
-x_2 = l_Lean_Parser_Term_app___closed__3;
+x_2 = l_Lean_Parser_Term_app___closed__2;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_app___closed__5() {
+lean_object* _init_l_Lean_Parser_Term_app___closed__4() {
 _start:
 {
 lean_object* x_1; 
@@ -31010,12 +30973,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_app___elambda__1___boxed), 3
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_app___closed__6() {
+lean_object* _init_l_Lean_Parser_Term_app___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_app___closed__4;
-x_2 = l_Lean_Parser_Term_app___closed__5;
+x_1 = l_Lean_Parser_Term_app___closed__3;
+x_2 = l_Lean_Parser_Term_app___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);
@@ -31026,7 +30989,7 @@ lean_object* _init_l_Lean_Parser_Term_app() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Term_app___closed__6;
+x_1 = l_Lean_Parser_Term_app___closed__5;
 return x_1;
 }
 }
@@ -31230,23 +31193,13 @@ lean_object* _init_l_Lean_Parser_Term_sortApp___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_epsilonInfo;
-x_2 = l_Lean_Parser_Term_sortApp___closed__2;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Term_sortApp___closed__4() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_sortApp___elambda__1___rarg___closed__2;
-x_2 = l_Lean_Parser_Term_sortApp___closed__3;
+x_2 = l_Lean_Parser_Term_sortApp___closed__2;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_sortApp___closed__5() {
+lean_object* _init_l_Lean_Parser_Term_sortApp___closed__4() {
 _start:
 {
 lean_object* x_1; 
@@ -31254,12 +31207,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_sortApp___elambda__1___boxed
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_sortApp___closed__6() {
+lean_object* _init_l_Lean_Parser_Term_sortApp___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_sortApp___closed__4;
-x_2 = l_Lean_Parser_Term_sortApp___closed__5;
+x_1 = l_Lean_Parser_Term_sortApp___closed__3;
+x_2 = l_Lean_Parser_Term_sortApp___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);
@@ -31270,7 +31223,7 @@ lean_object* _init_l_Lean_Parser_Term_sortApp() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Term_sortApp___closed__6;
+x_1 = l_Lean_Parser_Term_sortApp___closed__5;
 return x_1;
 }
 }
@@ -31375,7 +31328,7 @@ return x_2;
 lean_object* l_Lean_Parser_Term_proj___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_42; uint8_t x_43; 
 x_4 = l_Lean_Parser_Term_proj___elambda__1___closed__4;
 x_5 = lean_ctor_get(x_4, 1);
 lean_inc(x_5);
@@ -31386,215 +31339,194 @@ x_8 = lean_ctor_get(x_3, 0);
 lean_inc(x_8);
 x_9 = lean_ctor_get(x_3, 1);
 lean_inc(x_9);
-x_10 = lean_ctor_get(x_3, 3);
-lean_inc(x_10);
-x_11 = lean_array_get_size(x_8);
-if (lean_obj_tag(x_10) == 0)
-{
-lean_object* x_43; uint8_t x_44; 
-x_43 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_8);
+x_10 = lean_array_get_size(x_8);
+x_42 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_8);
 lean_dec(x_8);
-x_44 = l_Lean_Parser_checkTailNoWs(x_43);
-lean_dec(x_43);
-if (x_44 == 0)
+x_43 = l_Lean_Parser_checkTailNoWs(x_42);
+lean_dec(x_42);
+if (x_43 == 0)
 {
-lean_object* x_45; lean_object* x_46; 
+lean_object* x_44; lean_object* x_45; 
 lean_dec(x_9);
-x_45 = l_Lean_Parser_Term_proj___elambda__1___closed__7;
-x_46 = l_Lean_Parser_ParserState_mkError(x_3, x_45);
-x_12 = x_46;
-goto block_42;
+x_44 = l_Lean_Parser_Term_proj___elambda__1___closed__7;
+x_45 = l_Lean_Parser_ParserState_mkError(x_3, x_44);
+x_11 = x_45;
+goto block_41;
 }
 else
 {
-lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; 
-x_47 = lean_ctor_get(x_2, 0);
+lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; 
+x_46 = lean_ctor_get(x_2, 0);
+lean_inc(x_46);
+x_47 = lean_ctor_get(x_46, 0);
 lean_inc(x_47);
-x_48 = lean_ctor_get(x_47, 0);
-lean_inc(x_48);
-lean_dec(x_47);
-x_49 = l_Lean_Parser_Term_proj___elambda__1___closed__3;
-x_50 = l_Lean_Parser_Term_proj___elambda__1___closed__7;
-x_51 = lean_unsigned_to_nat(0u);
-x_52 = l_Lean_Parser_strAux___main(x_49, x_50, x_51, x_2, x_3);
-x_53 = lean_ctor_get(x_52, 3);
-lean_inc(x_53);
-if (lean_obj_tag(x_53) == 0)
+lean_dec(x_46);
+x_48 = l_Lean_Parser_Term_proj___elambda__1___closed__3;
+x_49 = l_Lean_Parser_Term_proj___elambda__1___closed__7;
+x_50 = lean_unsigned_to_nat(0u);
+x_51 = l_Lean_Parser_strAux___main(x_48, x_49, x_50, x_2, x_3);
+x_52 = lean_ctor_get(x_51, 3);
+lean_inc(x_52);
+if (lean_obj_tag(x_52) == 0)
 {
-lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; 
+lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; 
 lean_inc_n(x_9, 2);
-lean_inc(x_48);
-x_54 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_54, 0, x_48);
-lean_ctor_set(x_54, 1, x_9);
-lean_ctor_set(x_54, 2, x_9);
-x_55 = l_Lean_Parser_Term_proj___elambda__1___closed__8;
-x_56 = lean_nat_add(x_9, x_55);
-lean_inc(x_56);
+lean_inc(x_47);
+x_53 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_53, 0, x_47);
+lean_ctor_set(x_53, 1, x_9);
+lean_ctor_set(x_53, 2, x_9);
+x_54 = l_Lean_Parser_Term_proj___elambda__1___closed__8;
+x_55 = lean_nat_add(x_9, x_54);
+lean_inc(x_55);
+x_56 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_56, 0, x_47);
+lean_ctor_set(x_56, 1, x_55);
+lean_ctor_set(x_56, 2, x_55);
 x_57 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_57, 0, x_48);
-lean_ctor_set(x_57, 1, x_56);
+lean_ctor_set(x_57, 0, x_53);
+lean_ctor_set(x_57, 1, x_9);
 lean_ctor_set(x_57, 2, x_56);
-x_58 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_58, 0, x_54);
-lean_ctor_set(x_58, 1, x_9);
-lean_ctor_set(x_58, 2, x_57);
-x_59 = lean_alloc_ctor(1, 1, 0);
+x_58 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_58, 0, x_57);
+x_59 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_59, 0, x_58);
-x_60 = lean_alloc_ctor(2, 2, 0);
-lean_ctor_set(x_60, 0, x_59);
-lean_ctor_set(x_60, 1, x_49);
-x_61 = l_Lean_Parser_ParserState_pushSyntax(x_52, x_60);
-x_12 = x_61;
-goto block_42;
+lean_ctor_set(x_59, 1, x_48);
+x_60 = l_Lean_Parser_ParserState_pushSyntax(x_51, x_59);
+x_11 = x_60;
+goto block_41;
 }
 else
 {
-lean_dec(x_53);
-lean_dec(x_48);
+lean_dec(x_52);
+lean_dec(x_47);
 lean_dec(x_9);
-x_12 = x_52;
-goto block_42;
+x_11 = x_51;
+goto block_41;
 }
 }
-}
-else
+block_41:
 {
-lean_object* x_62; lean_object* x_63; 
-lean_dec(x_10);
-lean_dec(x_9);
-lean_dec(x_8);
-lean_dec(x_7);
-lean_dec(x_5);
-lean_dec(x_2);
-lean_dec(x_1);
-x_62 = l_Lean_Parser_Term_proj___elambda__1___closed__2;
-x_63 = l_Lean_Parser_ParserState_mkTrailingNode(x_3, x_62, x_11);
-lean_dec(x_11);
-return x_63;
-}
-block_42:
+lean_object* x_12; 
+x_12 = lean_ctor_get(x_11, 3);
+lean_inc(x_12);
+if (lean_obj_tag(x_12) == 0)
 {
-lean_object* x_13; 
-x_13 = lean_ctor_get(x_12, 3);
+lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_31; lean_object* x_32; 
+x_13 = lean_ctor_get(x_11, 0);
 lean_inc(x_13);
-if (lean_obj_tag(x_13) == 0)
-{
-lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_32; lean_object* x_33; 
-x_14 = lean_ctor_get(x_12, 0);
-lean_inc(x_14);
-x_15 = lean_array_get_size(x_14);
-lean_dec(x_14);
-x_16 = lean_ctor_get(x_12, 1);
-lean_inc(x_16);
+x_14 = lean_array_get_size(x_13);
+lean_dec(x_13);
+x_15 = lean_ctor_get(x_11, 1);
+lean_inc(x_15);
 lean_inc(x_2);
 lean_inc(x_1);
-x_32 = lean_apply_3(x_5, x_1, x_2, x_12);
-x_33 = lean_ctor_get(x_32, 3);
+x_31 = lean_apply_3(x_5, x_1, x_2, x_11);
+x_32 = lean_ctor_get(x_31, 3);
+lean_inc(x_32);
+if (lean_obj_tag(x_32) == 0)
+{
+x_16 = x_31;
+goto block_30;
+}
+else
+{
+lean_object* x_33; lean_object* x_34; uint8_t x_35; 
+x_33 = lean_ctor_get(x_32, 0);
 lean_inc(x_33);
-if (lean_obj_tag(x_33) == 0)
-{
-x_17 = x_32;
-goto block_31;
-}
-else
-{
-lean_object* x_34; lean_object* x_35; uint8_t x_36; 
-x_34 = lean_ctor_get(x_33, 0);
+lean_dec(x_32);
+x_34 = lean_ctor_get(x_31, 1);
 lean_inc(x_34);
-lean_dec(x_33);
-x_35 = lean_ctor_get(x_32, 1);
-lean_inc(x_35);
-x_36 = lean_nat_dec_eq(x_35, x_16);
-lean_dec(x_35);
-if (x_36 == 0)
-{
+x_35 = lean_nat_dec_eq(x_34, x_15);
 lean_dec(x_34);
-x_17 = x_32;
-goto block_31;
+if (x_35 == 0)
+{
+lean_dec(x_33);
+x_16 = x_31;
+goto block_30;
 }
 else
 {
-lean_object* x_37; lean_object* x_38; lean_object* x_39; 
-lean_inc(x_16);
-x_37 = l_Lean_Parser_ParserState_restore(x_32, x_15, x_16);
-x_38 = l_Lean_Parser_fieldIdxFn(x_2, x_37);
-x_39 = l_Lean_Parser_mergeOrElseErrors(x_38, x_34, x_16);
-x_17 = x_39;
-goto block_31;
+lean_object* x_36; lean_object* x_37; lean_object* x_38; 
+lean_inc(x_15);
+x_36 = l_Lean_Parser_ParserState_restore(x_31, x_14, x_15);
+x_37 = l_Lean_Parser_fieldIdxFn(x_2, x_36);
+x_38 = l_Lean_Parser_mergeOrElseErrors(x_37, x_33, x_15);
+x_16 = x_38;
+goto block_30;
 }
 }
-block_31:
+block_30:
 {
-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_17; 
+x_17 = lean_ctor_get(x_16, 3);
+lean_inc(x_17);
+if (lean_obj_tag(x_17) == 0)
 {
-lean_object* x_19; lean_object* x_20; 
-lean_dec(x_16);
+lean_object* x_18; lean_object* x_19; 
 lean_dec(x_15);
+lean_dec(x_14);
 lean_dec(x_7);
 lean_dec(x_2);
 lean_dec(x_1);
-x_19 = l_Lean_Parser_Term_proj___elambda__1___closed__2;
-x_20 = l_Lean_Parser_ParserState_mkTrailingNode(x_17, x_19, x_11);
-lean_dec(x_11);
-return x_20;
+x_18 = l_Lean_Parser_Term_proj___elambda__1___closed__2;
+x_19 = l_Lean_Parser_ParserState_mkTrailingNode(x_16, x_18, x_10);
+lean_dec(x_10);
+return x_19;
 }
 else
 {
-lean_object* x_21; lean_object* x_22; uint8_t x_23; 
-x_21 = lean_ctor_get(x_18, 0);
+lean_object* x_20; lean_object* x_21; uint8_t x_22; 
+x_20 = lean_ctor_get(x_17, 0);
+lean_inc(x_20);
+lean_dec(x_17);
+x_21 = lean_ctor_get(x_16, 1);
 lean_inc(x_21);
-lean_dec(x_18);
-x_22 = lean_ctor_get(x_17, 1);
-lean_inc(x_22);
-x_23 = lean_nat_dec_eq(x_22, x_16);
-lean_dec(x_22);
-if (x_23 == 0)
-{
-lean_object* x_24; lean_object* x_25; 
+x_22 = lean_nat_dec_eq(x_21, x_15);
 lean_dec(x_21);
-lean_dec(x_16);
+if (x_22 == 0)
+{
+lean_object* x_23; lean_object* x_24; 
+lean_dec(x_20);
 lean_dec(x_15);
+lean_dec(x_14);
 lean_dec(x_7);
 lean_dec(x_2);
 lean_dec(x_1);
-x_24 = l_Lean_Parser_Term_proj___elambda__1___closed__2;
-x_25 = l_Lean_Parser_ParserState_mkTrailingNode(x_17, x_24, x_11);
-lean_dec(x_11);
-return x_25;
+x_23 = l_Lean_Parser_Term_proj___elambda__1___closed__2;
+x_24 = l_Lean_Parser_ParserState_mkTrailingNode(x_16, x_23, x_10);
+lean_dec(x_10);
+return x_24;
 }
 else
 {
-lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; 
-lean_inc(x_16);
-x_26 = l_Lean_Parser_ParserState_restore(x_17, x_15, x_16);
+lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; 
+lean_inc(x_15);
+x_25 = l_Lean_Parser_ParserState_restore(x_16, x_14, x_15);
+lean_dec(x_14);
+x_26 = lean_apply_3(x_7, x_1, x_2, x_25);
+x_27 = l_Lean_Parser_mergeOrElseErrors(x_26, x_20, x_15);
 lean_dec(x_15);
-x_27 = lean_apply_3(x_7, x_1, x_2, x_26);
-x_28 = l_Lean_Parser_mergeOrElseErrors(x_27, x_21, x_16);
-lean_dec(x_16);
-x_29 = l_Lean_Parser_Term_proj___elambda__1___closed__2;
-x_30 = l_Lean_Parser_ParserState_mkTrailingNode(x_28, x_29, x_11);
-lean_dec(x_11);
-return x_30;
+x_28 = l_Lean_Parser_Term_proj___elambda__1___closed__2;
+x_29 = l_Lean_Parser_ParserState_mkTrailingNode(x_27, x_28, x_10);
+lean_dec(x_10);
+return x_29;
 }
 }
 }
 }
 else
 {
-lean_object* x_40; lean_object* x_41; 
-lean_dec(x_13);
+lean_object* x_39; lean_object* x_40; 
+lean_dec(x_12);
 lean_dec(x_7);
 lean_dec(x_5);
 lean_dec(x_2);
 lean_dec(x_1);
-x_40 = l_Lean_Parser_Term_proj___elambda__1___closed__2;
-x_41 = l_Lean_Parser_ParserState_mkTrailingNode(x_12, x_40, x_11);
-lean_dec(x_11);
-return x_41;
+x_39 = l_Lean_Parser_Term_proj___elambda__1___closed__2;
+x_40 = l_Lean_Parser_ParserState_mkTrailingNode(x_11, x_39, x_10);
+lean_dec(x_10);
+return x_40;
 }
 }
 }
@@ -31667,23 +31599,13 @@ lean_object* _init_l_Lean_Parser_Term_proj___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_Term_proj___closed__6;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Term_proj___closed__8() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_proj___elambda__1___closed__2;
-x_2 = l_Lean_Parser_Term_proj___closed__7;
+x_2 = l_Lean_Parser_Term_proj___closed__6;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_proj___closed__9() {
+lean_object* _init_l_Lean_Parser_Term_proj___closed__8() {
 _start:
 {
 lean_object* x_1; 
@@ -31691,12 +31613,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_proj___elambda__1), 3, 0);
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_proj___closed__10() {
+lean_object* _init_l_Lean_Parser_Term_proj___closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_proj___closed__8;
-x_2 = l_Lean_Parser_Term_proj___closed__9;
+x_1 = l_Lean_Parser_Term_proj___closed__7;
+x_2 = l_Lean_Parser_Term_proj___closed__8;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -31707,7 +31629,7 @@ lean_object* _init_l_Lean_Parser_Term_proj() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Term_proj___closed__10;
+x_1 = l_Lean_Parser_Term_proj___closed__9;
 return x_1;
 }
 }
@@ -31862,197 +31784,179 @@ return x_2;
 lean_object* l_Lean_Parser_Term_arrayRef___elambda__1___rarg(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_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_39; uint8_t x_40; 
 x_3 = lean_ctor_get(x_2, 0);
 lean_inc(x_3);
 x_4 = lean_ctor_get(x_2, 1);
 lean_inc(x_4);
-x_5 = lean_ctor_get(x_2, 3);
-lean_inc(x_5);
-x_6 = lean_array_get_size(x_3);
-if (lean_obj_tag(x_5) == 0)
-{
-lean_object* x_40; uint8_t x_41; 
-x_40 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_3);
+x_5 = lean_array_get_size(x_3);
+x_39 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_3);
 lean_dec(x_3);
-x_41 = l_Lean_Parser_checkTailNoWs(x_40);
-lean_dec(x_40);
-if (x_41 == 0)
+x_40 = l_Lean_Parser_checkTailNoWs(x_39);
+lean_dec(x_39);
+if (x_40 == 0)
 {
-lean_object* x_42; lean_object* x_43; 
+lean_object* x_41; lean_object* x_42; 
 lean_dec(x_4);
-x_42 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__3;
-x_43 = l_Lean_Parser_ParserState_mkError(x_2, x_42);
-x_7 = x_43;
-goto block_39;
+x_41 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__3;
+x_42 = l_Lean_Parser_ParserState_mkError(x_2, x_41);
+x_6 = x_42;
+goto block_38;
 }
 else
 {
-lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; 
-x_44 = lean_ctor_get(x_1, 0);
+lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; 
+x_43 = lean_ctor_get(x_1, 0);
+lean_inc(x_43);
+x_44 = lean_ctor_get(x_43, 0);
 lean_inc(x_44);
-x_45 = lean_ctor_get(x_44, 0);
-lean_inc(x_45);
-lean_dec(x_44);
-x_46 = l_Lean_Parser_Term_listLit___elambda__1___closed__5;
-x_47 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__3;
-x_48 = lean_unsigned_to_nat(0u);
-x_49 = l_Lean_Parser_strAux___main(x_46, x_47, x_48, x_1, x_2);
-x_50 = lean_ctor_get(x_49, 3);
-lean_inc(x_50);
-if (lean_obj_tag(x_50) == 0)
+lean_dec(x_43);
+x_45 = l_Lean_Parser_Term_listLit___elambda__1___closed__5;
+x_46 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__3;
+x_47 = lean_unsigned_to_nat(0u);
+x_48 = l_Lean_Parser_strAux___main(x_45, x_46, x_47, x_1, x_2);
+x_49 = lean_ctor_get(x_48, 3);
+lean_inc(x_49);
+if (lean_obj_tag(x_49) == 0)
 {
-lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; 
+lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; 
 lean_inc_n(x_4, 2);
-lean_inc(x_45);
-x_51 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_51, 0, x_45);
-lean_ctor_set(x_51, 1, x_4);
-lean_ctor_set(x_51, 2, x_4);
-x_52 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__4;
-x_53 = lean_nat_add(x_4, x_52);
-lean_inc(x_53);
+lean_inc(x_44);
+x_50 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_50, 0, x_44);
+lean_ctor_set(x_50, 1, x_4);
+lean_ctor_set(x_50, 2, x_4);
+x_51 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__4;
+x_52 = lean_nat_add(x_4, x_51);
+lean_inc(x_52);
+x_53 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_53, 0, x_44);
+lean_ctor_set(x_53, 1, x_52);
+lean_ctor_set(x_53, 2, x_52);
 x_54 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_54, 0, x_45);
-lean_ctor_set(x_54, 1, x_53);
+lean_ctor_set(x_54, 0, x_50);
+lean_ctor_set(x_54, 1, x_4);
 lean_ctor_set(x_54, 2, x_53);
-x_55 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_55, 0, x_51);
-lean_ctor_set(x_55, 1, x_4);
-lean_ctor_set(x_55, 2, x_54);
-x_56 = lean_alloc_ctor(1, 1, 0);
+x_55 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_55, 0, x_54);
+x_56 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_56, 0, x_55);
-x_57 = lean_alloc_ctor(2, 2, 0);
-lean_ctor_set(x_57, 0, x_56);
-lean_ctor_set(x_57, 1, x_46);
-x_58 = l_Lean_Parser_ParserState_pushSyntax(x_49, x_57);
-x_7 = x_58;
-goto block_39;
+lean_ctor_set(x_56, 1, x_45);
+x_57 = l_Lean_Parser_ParserState_pushSyntax(x_48, x_56);
+x_6 = x_57;
+goto block_38;
 }
 else
 {
-lean_dec(x_50);
-lean_dec(x_45);
+lean_dec(x_49);
+lean_dec(x_44);
 lean_dec(x_4);
-x_7 = x_49;
-goto block_39;
+x_6 = x_48;
+goto block_38;
 }
 }
-}
-else
+block_38:
 {
-lean_object* x_59; lean_object* x_60; 
-lean_dec(x_5);
-lean_dec(x_4);
-lean_dec(x_3);
-lean_dec(x_1);
-x_59 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
-x_60 = l_Lean_Parser_ParserState_mkTrailingNode(x_2, x_59, x_6);
-lean_dec(x_6);
-return x_60;
-}
-block_39:
+lean_object* x_7; 
+x_7 = lean_ctor_get(x_6, 3);
+lean_inc(x_7);
+if (lean_obj_tag(x_7) == 0)
 {
-lean_object* x_8; 
-x_8 = lean_ctor_get(x_7, 3);
-lean_inc(x_8);
-if (lean_obj_tag(x_8) == 0)
-{
-lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
-x_9 = l_Lean_Parser_termParser___closed__2;
-x_10 = lean_unsigned_to_nat(0u);
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_8 = l_Lean_Parser_termParser___closed__2;
+x_9 = lean_unsigned_to_nat(0u);
 lean_inc(x_1);
-x_11 = l_Lean_Parser_categoryParserFn(x_9, x_10, x_1, x_7);
-x_12 = lean_ctor_get(x_11, 3);
+x_10 = l_Lean_Parser_categoryParserFn(x_8, x_9, x_1, x_6);
+x_11 = lean_ctor_get(x_10, 3);
+lean_inc(x_11);
+if (lean_obj_tag(x_11) == 0)
+{
+lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+x_12 = lean_ctor_get(x_10, 1);
 lean_inc(x_12);
-if (lean_obj_tag(x_12) == 0)
+x_13 = l_Lean_Parser_tokenFn(x_1, x_10);
+x_14 = lean_ctor_get(x_13, 3);
+lean_inc(x_14);
+if (lean_obj_tag(x_14) == 0)
 {
-lean_object* x_13; lean_object* x_14; lean_object* x_15; 
-x_13 = lean_ctor_get(x_11, 1);
-lean_inc(x_13);
-x_14 = l_Lean_Parser_tokenFn(x_1, x_11);
-x_15 = lean_ctor_get(x_14, 3);
+lean_object* x_15; lean_object* x_16; 
+x_15 = lean_ctor_get(x_13, 0);
 lean_inc(x_15);
-if (lean_obj_tag(x_15) == 0)
-{
-lean_object* x_16; lean_object* x_17; 
-x_16 = lean_ctor_get(x_14, 0);
-lean_inc(x_16);
-x_17 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_16);
-lean_dec(x_16);
-if (lean_obj_tag(x_17) == 2)
-{
-lean_object* x_18; lean_object* x_19; uint8_t x_20; 
-x_18 = lean_ctor_get(x_17, 1);
-lean_inc(x_18);
-lean_dec(x_17);
-x_19 = l_Lean_Parser_Term_listLit___elambda__1___closed__6;
-x_20 = lean_string_dec_eq(x_18, x_19);
-lean_dec(x_18);
-if (x_20 == 0)
-{
-lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; 
-x_21 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
-x_22 = l_Lean_Parser_ParserState_mkErrorsAt(x_14, x_21, x_13);
-x_23 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
-x_24 = l_Lean_Parser_ParserState_mkTrailingNode(x_22, x_23, x_6);
-lean_dec(x_6);
-return x_24;
-}
-else
-{
-lean_object* x_25; lean_object* x_26; 
-lean_dec(x_13);
-x_25 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
-x_26 = l_Lean_Parser_ParserState_mkTrailingNode(x_14, x_25, x_6);
-lean_dec(x_6);
-return x_26;
-}
-}
-else
-{
-lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; 
-lean_dec(x_17);
-x_27 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
-x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_14, x_27, x_13);
-x_29 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
-x_30 = l_Lean_Parser_ParserState_mkTrailingNode(x_28, x_29, x_6);
-lean_dec(x_6);
-return x_30;
-}
-}
-else
-{
-lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; 
+x_16 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_15);
 lean_dec(x_15);
-x_31 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
-x_32 = l_Lean_Parser_ParserState_mkErrorsAt(x_14, x_31, x_13);
-x_33 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
-x_34 = l_Lean_Parser_ParserState_mkTrailingNode(x_32, x_33, x_6);
-lean_dec(x_6);
-return x_34;
-}
+if (lean_obj_tag(x_16) == 2)
+{
+lean_object* x_17; lean_object* x_18; uint8_t x_19; 
+x_17 = lean_ctor_get(x_16, 1);
+lean_inc(x_17);
+lean_dec(x_16);
+x_18 = l_Lean_Parser_Term_listLit___elambda__1___closed__6;
+x_19 = lean_string_dec_eq(x_17, x_18);
+lean_dec(x_17);
+if (x_19 == 0)
+{
+lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
+x_20 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_21 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_20, x_12);
+x_22 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
+x_23 = l_Lean_Parser_ParserState_mkTrailingNode(x_21, x_22, x_5);
+lean_dec(x_5);
+return x_23;
 }
 else
 {
-lean_object* x_35; lean_object* x_36; 
+lean_object* x_24; lean_object* x_25; 
 lean_dec(x_12);
-lean_dec(x_1);
-x_35 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
-x_36 = l_Lean_Parser_ParserState_mkTrailingNode(x_11, x_35, x_6);
-lean_dec(x_6);
-return x_36;
+x_24 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
+x_25 = l_Lean_Parser_ParserState_mkTrailingNode(x_13, x_24, x_5);
+lean_dec(x_5);
+return x_25;
 }
 }
 else
 {
-lean_object* x_37; lean_object* x_38; 
-lean_dec(x_8);
+lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; 
+lean_dec(x_16);
+x_26 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_27 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_26, x_12);
+x_28 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
+x_29 = l_Lean_Parser_ParserState_mkTrailingNode(x_27, x_28, x_5);
+lean_dec(x_5);
+return x_29;
+}
+}
+else
+{
+lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; 
+lean_dec(x_14);
+x_30 = l_Lean_Parser_Term_listLit___elambda__1___closed__9;
+x_31 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_30, x_12);
+x_32 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
+x_33 = l_Lean_Parser_ParserState_mkTrailingNode(x_31, x_32, x_5);
+lean_dec(x_5);
+return x_33;
+}
+}
+else
+{
+lean_object* x_34; lean_object* x_35; 
+lean_dec(x_11);
 lean_dec(x_1);
-x_37 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
-x_38 = l_Lean_Parser_ParserState_mkTrailingNode(x_7, x_37, x_6);
-lean_dec(x_6);
-return x_38;
+x_34 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
+x_35 = l_Lean_Parser_ParserState_mkTrailingNode(x_10, x_34, x_5);
+lean_dec(x_5);
+return x_35;
+}
+}
+else
+{
+lean_object* x_36; lean_object* x_37; 
+lean_dec(x_7);
+lean_dec(x_1);
+x_36 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
+x_37 = l_Lean_Parser_ParserState_mkTrailingNode(x_6, x_36, x_5);
+lean_dec(x_5);
+return x_37;
 }
 }
 }
@@ -32112,23 +32016,13 @@ lean_object* _init_l_Lean_Parser_Term_arrayRef___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_epsilonInfo;
-x_2 = l_Lean_Parser_Term_arrayRef___closed__4;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Term_arrayRef___closed__6() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_arrayRef___elambda__1___rarg___closed__2;
-x_2 = l_Lean_Parser_Term_arrayRef___closed__5;
+x_2 = l_Lean_Parser_Term_arrayRef___closed__4;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_arrayRef___closed__7() {
+lean_object* _init_l_Lean_Parser_Term_arrayRef___closed__6() {
 _start:
 {
 lean_object* x_1; 
@@ -32136,12 +32030,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_arrayRef___elambda__1___boxe
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_arrayRef___closed__8() {
+lean_object* _init_l_Lean_Parser_Term_arrayRef___closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_arrayRef___closed__6;
-x_2 = l_Lean_Parser_Term_arrayRef___closed__7;
+x_1 = l_Lean_Parser_Term_arrayRef___closed__5;
+x_2 = l_Lean_Parser_Term_arrayRef___closed__6;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -32152,7 +32046,7 @@ lean_object* _init_l_Lean_Parser_Term_arrayRef() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Term_arrayRef___closed__8;
+x_1 = l_Lean_Parser_Term_arrayRef___closed__7;
 return x_1;
 }
 }
@@ -32206,114 +32100,136 @@ return x_1;
 lean_object* l_Lean_Parser_Term_dollar___elambda__1___rarg(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; lean_object* x_10; lean_object* x_11; 
+lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_3 = lean_ctor_get(x_2, 0);
 lean_inc(x_3);
 x_4 = lean_ctor_get(x_2, 1);
 lean_inc(x_4);
-x_5 = lean_ctor_get(x_2, 2);
-lean_inc(x_5);
-x_6 = lean_ctor_get(x_2, 3);
-lean_inc(x_6);
-x_7 = lean_array_get_size(x_3);
-if (lean_obj_tag(x_6) == 0)
-{
-lean_object* x_25; lean_object* x_26; 
-lean_dec(x_5);
+x_5 = lean_array_get_size(x_3);
 lean_dec(x_3);
 lean_inc(x_1);
-x_25 = l_Lean_Parser_dollarSymbol___elambda__1___rarg(x_1, x_2);
-x_26 = lean_ctor_get(x_25, 3);
-lean_inc(x_26);
-if (lean_obj_tag(x_26) == 0)
+x_6 = l_Lean_Parser_dollarSymbol___elambda__1___rarg(x_1, x_2);
+x_7 = lean_ctor_get(x_6, 3);
+lean_inc(x_7);
+if (lean_obj_tag(x_7) == 0)
 {
-lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; 
-x_27 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__3;
-x_28 = l_Lean_Parser_checkWsBeforeFn(x_27, x_1, x_25);
-x_29 = lean_ctor_get(x_28, 0);
-lean_inc(x_29);
-x_30 = lean_ctor_get(x_28, 2);
-lean_inc(x_30);
-x_31 = lean_ctor_get(x_28, 3);
-lean_inc(x_31);
-x_8 = x_28;
-x_9 = x_29;
-x_10 = x_30;
-x_11 = x_31;
-goto block_24;
-}
-else
+lean_object* x_8; lean_object* x_9; lean_object* x_10; 
+x_8 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__3;
+x_9 = l_Lean_Parser_checkWsBeforeFn(x_8, x_1, x_6);
+x_10 = lean_ctor_get(x_9, 3);
+lean_inc(x_10);
+if (lean_obj_tag(x_10) == 0)
 {
-lean_object* x_32; lean_object* x_33; lean_object* x_34; 
-lean_dec(x_26);
-x_32 = lean_ctor_get(x_25, 0);
-lean_inc(x_32);
-x_33 = lean_ctor_get(x_25, 2);
-lean_inc(x_33);
-x_34 = lean_ctor_get(x_25, 3);
-lean_inc(x_34);
-x_8 = x_25;
-x_9 = x_32;
-x_10 = x_33;
-x_11 = x_34;
-goto block_24;
-}
-}
-else
-{
-x_8 = x_2;
-x_9 = x_3;
-x_10 = x_5;
-x_11 = x_6;
-goto block_24;
-}
-block_24:
-{
-if (lean_obj_tag(x_11) == 0)
-{
-lean_object* x_12; 
-lean_dec(x_10);
-lean_dec(x_9);
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
 lean_dec(x_4);
-x_12 = lean_ctor_get(x_8, 3);
-lean_inc(x_12);
-if (lean_obj_tag(x_12) == 0)
-{
-lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
-x_13 = l_Lean_Parser_termParser___closed__2;
-x_14 = lean_unsigned_to_nat(0u);
-x_15 = l_Lean_Parser_categoryParserFn(x_13, x_14, x_1, x_8);
-x_16 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__2;
-x_17 = l_Lean_Parser_ParserState_mkTrailingNode(x_15, x_16, x_7);
-lean_dec(x_7);
-return x_17;
+x_11 = l_Lean_Parser_termParser___closed__2;
+x_12 = lean_unsigned_to_nat(0u);
+x_13 = l_Lean_Parser_categoryParserFn(x_11, x_12, x_1, x_9);
+x_14 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__2;
+x_15 = l_Lean_Parser_ParserState_mkTrailingNode(x_13, x_14, x_5);
+lean_dec(x_5);
+return x_15;
 }
 else
 {
-lean_object* x_18; lean_object* x_19; 
-lean_dec(x_12);
+uint8_t x_16; 
 lean_dec(x_1);
-x_18 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__2;
-x_19 = l_Lean_Parser_ParserState_mkTrailingNode(x_8, x_18, x_7);
-lean_dec(x_7);
-return x_19;
+x_16 = !lean_is_exclusive(x_9);
+if (x_16 == 0)
+{
+lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+x_17 = lean_ctor_get(x_9, 0);
+x_18 = lean_ctor_get(x_9, 3);
+lean_dec(x_18);
+x_19 = lean_ctor_get(x_9, 1);
+lean_dec(x_19);
+x_20 = l_Array_shrink___main___rarg(x_17, x_5);
+lean_ctor_set(x_9, 1, x_4);
+lean_ctor_set(x_9, 0, x_20);
+x_21 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__2;
+x_22 = l_Lean_Parser_ParserState_mkTrailingNode(x_9, x_21, x_5);
+lean_dec(x_5);
+return x_22;
+}
+else
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_23 = lean_ctor_get(x_9, 0);
+x_24 = lean_ctor_get(x_9, 2);
+lean_inc(x_24);
+lean_inc(x_23);
+lean_dec(x_9);
+x_25 = l_Array_shrink___main___rarg(x_23, x_5);
+x_26 = lean_alloc_ctor(0, 4, 0);
+lean_ctor_set(x_26, 0, x_25);
+lean_ctor_set(x_26, 1, x_4);
+lean_ctor_set(x_26, 2, x_24);
+lean_ctor_set(x_26, 3, x_10);
+x_27 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__2;
+x_28 = l_Lean_Parser_ParserState_mkTrailingNode(x_26, x_27, x_5);
+lean_dec(x_5);
+return x_28;
+}
 }
 }
 else
 {
-lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
-lean_dec(x_8);
-lean_dec(x_1);
-x_20 = l_Array_shrink___main___rarg(x_9, x_7);
-x_21 = lean_alloc_ctor(0, 4, 0);
-lean_ctor_set(x_21, 0, x_20);
-lean_ctor_set(x_21, 1, x_4);
-lean_ctor_set(x_21, 2, x_10);
-lean_ctor_set(x_21, 3, x_11);
-x_22 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__2;
-x_23 = l_Lean_Parser_ParserState_mkTrailingNode(x_21, x_22, x_7);
+lean_object* x_29; 
 lean_dec(x_7);
-return x_23;
+x_29 = lean_ctor_get(x_6, 3);
+lean_inc(x_29);
+if (lean_obj_tag(x_29) == 0)
+{
+lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; 
+lean_dec(x_4);
+x_30 = l_Lean_Parser_termParser___closed__2;
+x_31 = lean_unsigned_to_nat(0u);
+x_32 = l_Lean_Parser_categoryParserFn(x_30, x_31, x_1, x_6);
+x_33 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__2;
+x_34 = l_Lean_Parser_ParserState_mkTrailingNode(x_32, x_33, x_5);
+lean_dec(x_5);
+return x_34;
+}
+else
+{
+uint8_t x_35; 
+lean_dec(x_1);
+x_35 = !lean_is_exclusive(x_6);
+if (x_35 == 0)
+{
+lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; 
+x_36 = lean_ctor_get(x_6, 0);
+x_37 = lean_ctor_get(x_6, 3);
+lean_dec(x_37);
+x_38 = lean_ctor_get(x_6, 1);
+lean_dec(x_38);
+x_39 = l_Array_shrink___main___rarg(x_36, x_5);
+lean_ctor_set(x_6, 1, x_4);
+lean_ctor_set(x_6, 0, x_39);
+x_40 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__2;
+x_41 = l_Lean_Parser_ParserState_mkTrailingNode(x_6, x_40, x_5);
+lean_dec(x_5);
+return x_41;
+}
+else
+{
+lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; 
+x_42 = lean_ctor_get(x_6, 0);
+x_43 = lean_ctor_get(x_6, 2);
+lean_inc(x_43);
+lean_inc(x_42);
+lean_dec(x_6);
+x_44 = l_Array_shrink___main___rarg(x_42, x_5);
+x_45 = lean_alloc_ctor(0, 4, 0);
+lean_ctor_set(x_45, 0, x_44);
+lean_ctor_set(x_45, 1, x_4);
+lean_ctor_set(x_45, 2, x_43);
+lean_ctor_set(x_45, 3, x_29);
+x_46 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__2;
+x_47 = l_Lean_Parser_ParserState_mkTrailingNode(x_45, x_46, x_5);
+lean_dec(x_5);
+return x_47;
+}
 }
 }
 }
@@ -32350,36 +32266,26 @@ return x_4;
 lean_object* _init_l_Lean_Parser_Term_dollar___closed__3() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_epsilonInfo;
-x_2 = l_Lean_Parser_Term_dollar___closed__2;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_Parser_Term_arrayRef___closed__2;
+x_2 = lean_ctor_get(x_1, 0);
+lean_inc(x_2);
+x_3 = l_Lean_Parser_Term_dollar___closed__2;
+x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
+return x_4;
 }
 }
 lean_object* _init_l_Lean_Parser_Term_dollar___closed__4() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Parser_Term_arrayRef___closed__2;
-x_2 = lean_ctor_get(x_1, 0);
-lean_inc(x_2);
-x_3 = l_Lean_Parser_Term_dollar___closed__3;
-x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
-return x_4;
-}
-}
-lean_object* _init_l_Lean_Parser_Term_dollar___closed__5() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_dollar___elambda__1___rarg___closed__2;
-x_2 = l_Lean_Parser_Term_dollar___closed__4;
+x_2 = l_Lean_Parser_Term_dollar___closed__3;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_dollar___closed__6() {
+lean_object* _init_l_Lean_Parser_Term_dollar___closed__5() {
 _start:
 {
 lean_object* x_1; 
@@ -32387,12 +32293,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_dollar___elambda__1___boxed)
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_dollar___closed__7() {
+lean_object* _init_l_Lean_Parser_Term_dollar___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_dollar___closed__5;
-x_2 = l_Lean_Parser_Term_dollar___closed__6;
+x_1 = l_Lean_Parser_Term_dollar___closed__4;
+x_2 = l_Lean_Parser_Term_dollar___closed__5;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -32403,7 +32309,7 @@ lean_object* _init_l_Lean_Parser_Term_dollar() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Term_dollar___closed__7;
+x_1 = l_Lean_Parser_Term_dollar___closed__6;
 return x_1;
 }
 }
@@ -32498,7 +32404,7 @@ return x_3;
 lean_object* l_Lean_Parser_Term_dollarProj___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_41; 
+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_41; lean_object* x_42; lean_object* x_43; 
 x_4 = l_Lean_Parser_Term_proj___elambda__1___closed__4;
 x_5 = lean_ctor_get(x_4, 1);
 lean_inc(x_5);
@@ -32509,80 +32415,61 @@ x_8 = lean_ctor_get(x_3, 0);
 lean_inc(x_8);
 x_9 = lean_array_get_size(x_8);
 lean_dec(x_8);
-x_41 = lean_ctor_get(x_3, 3);
+x_41 = lean_ctor_get(x_3, 1);
 lean_inc(x_41);
-if (lean_obj_tag(x_41) == 0)
-{
-lean_object* x_42; lean_object* x_43; lean_object* x_44; 
-x_42 = lean_ctor_get(x_3, 1);
-lean_inc(x_42);
 lean_inc(x_2);
-x_43 = l_Lean_Parser_tokenFn(x_2, x_3);
-x_44 = lean_ctor_get(x_43, 3);
+x_42 = l_Lean_Parser_tokenFn(x_2, x_3);
+x_43 = lean_ctor_get(x_42, 3);
+lean_inc(x_43);
+if (lean_obj_tag(x_43) == 0)
+{
+lean_object* x_44; lean_object* x_45; 
+x_44 = lean_ctor_get(x_42, 0);
 lean_inc(x_44);
-if (lean_obj_tag(x_44) == 0)
-{
-lean_object* x_45; lean_object* x_46; 
-x_45 = lean_ctor_get(x_43, 0);
-lean_inc(x_45);
-x_46 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_45);
-lean_dec(x_45);
-if (lean_obj_tag(x_46) == 2)
-{
-lean_object* x_47; lean_object* x_48; uint8_t x_49; 
-x_47 = lean_ctor_get(x_46, 1);
-lean_inc(x_47);
-lean_dec(x_46);
-x_48 = l_Lean_Parser_Term_dollarProj___elambda__1___closed__4;
-x_49 = lean_string_dec_eq(x_47, x_48);
-lean_dec(x_47);
-if (x_49 == 0)
-{
-lean_object* x_50; lean_object* x_51; 
-x_50 = l_Lean_Parser_Term_dollarProj___elambda__1___closed__7;
-x_51 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_50, x_42);
-x_10 = x_51;
-goto block_40;
-}
-else
-{
-lean_dec(x_42);
-x_10 = x_43;
-goto block_40;
-}
-}
-else
-{
-lean_object* x_52; lean_object* x_53; 
-lean_dec(x_46);
-x_52 = l_Lean_Parser_Term_dollarProj___elambda__1___closed__7;
-x_53 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_52, x_42);
-x_10 = x_53;
-goto block_40;
-}
-}
-else
-{
-lean_object* x_54; lean_object* x_55; 
+x_45 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_44);
 lean_dec(x_44);
-x_54 = l_Lean_Parser_Term_dollarProj___elambda__1___closed__7;
-x_55 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_54, x_42);
-x_10 = x_55;
+if (lean_obj_tag(x_45) == 2)
+{
+lean_object* x_46; lean_object* x_47; uint8_t x_48; 
+x_46 = lean_ctor_get(x_45, 1);
+lean_inc(x_46);
+lean_dec(x_45);
+x_47 = l_Lean_Parser_Term_dollarProj___elambda__1___closed__4;
+x_48 = lean_string_dec_eq(x_46, x_47);
+lean_dec(x_46);
+if (x_48 == 0)
+{
+lean_object* x_49; lean_object* x_50; 
+x_49 = l_Lean_Parser_Term_dollarProj___elambda__1___closed__7;
+x_50 = l_Lean_Parser_ParserState_mkErrorsAt(x_42, x_49, x_41);
+x_10 = x_50;
+goto block_40;
+}
+else
+{
+lean_dec(x_41);
+x_10 = x_42;
 goto block_40;
 }
 }
 else
 {
-lean_object* x_56; lean_object* x_57; 
-lean_dec(x_41);
-lean_dec(x_7);
-lean_dec(x_5);
-lean_dec(x_2);
-lean_dec(x_1);
-x_56 = l_Lean_Parser_Term_dollarProj___elambda__1___closed__2;
-x_57 = l_Lean_Parser_ParserState_mkTrailingNode(x_3, x_56, x_9);
-lean_dec(x_9);
-return x_57;
+lean_object* x_51; lean_object* x_52; 
+lean_dec(x_45);
+x_51 = l_Lean_Parser_Term_dollarProj___elambda__1___closed__7;
+x_52 = l_Lean_Parser_ParserState_mkErrorsAt(x_42, x_51, x_41);
+x_10 = x_52;
+goto block_40;
+}
+}
+else
+{
+lean_object* x_53; lean_object* x_54; 
+lean_dec(x_43);
+x_53 = l_Lean_Parser_Term_dollarProj___elambda__1___closed__7;
+x_54 = l_Lean_Parser_ParserState_mkErrorsAt(x_42, x_53, x_41);
+x_10 = x_54;
+goto block_40;
 }
 block_40:
 {
@@ -32734,23 +32621,13 @@ lean_object* _init_l_Lean_Parser_Term_dollarProj___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_epsilonInfo;
-x_2 = l_Lean_Parser_Term_dollarProj___closed__2;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Term_dollarProj___closed__4() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_dollarProj___elambda__1___closed__2;
-x_2 = l_Lean_Parser_Term_dollarProj___closed__3;
+x_2 = l_Lean_Parser_Term_dollarProj___closed__2;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_dollarProj___closed__5() {
+lean_object* _init_l_Lean_Parser_Term_dollarProj___closed__4() {
 _start:
 {
 lean_object* x_1; 
@@ -32758,12 +32635,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_dollarProj___elambda__1), 3,
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_dollarProj___closed__6() {
+lean_object* _init_l_Lean_Parser_Term_dollarProj___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_dollarProj___closed__4;
-x_2 = l_Lean_Parser_Term_dollarProj___closed__5;
+x_1 = l_Lean_Parser_Term_dollarProj___closed__3;
+x_2 = l_Lean_Parser_Term_dollarProj___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);
@@ -32774,7 +32651,7 @@ lean_object* _init_l_Lean_Parser_Term_dollarProj() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Term_dollarProj___closed__6;
+x_1 = l_Lean_Parser_Term_dollarProj___closed__5;
 return x_1;
 }
 }
@@ -33142,97 +33019,93 @@ return x_3;
 lean_object* l_Lean_Parser_Term_where___elambda__1(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_4; lean_object* x_5; lean_object* x_6; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
 x_4 = lean_ctor_get(x_3, 0);
 lean_inc(x_4);
 x_5 = lean_array_get_size(x_4);
 lean_dec(x_4);
-x_6 = lean_ctor_get(x_3, 3);
-lean_inc(x_6);
-if (lean_obj_tag(x_6) == 0)
-{
-lean_object* x_7; lean_object* x_8; lean_object* x_9; 
-x_7 = lean_ctor_get(x_3, 1);
-lean_inc(x_7);
+x_16 = lean_ctor_get(x_3, 1);
+lean_inc(x_16);
 lean_inc(x_2);
-x_8 = l_Lean_Parser_tokenFn(x_2, x_3);
-x_9 = lean_ctor_get(x_8, 3);
-lean_inc(x_9);
-if (lean_obj_tag(x_9) == 0)
+x_17 = l_Lean_Parser_tokenFn(x_2, x_3);
+x_18 = lean_ctor_get(x_17, 3);
+lean_inc(x_18);
+if (lean_obj_tag(x_18) == 0)
 {
-lean_object* x_10; lean_object* x_11; 
-x_10 = lean_ctor_get(x_8, 0);
-lean_inc(x_10);
-x_11 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_10);
-lean_dec(x_10);
-if (lean_obj_tag(x_11) == 2)
+lean_object* x_19; lean_object* x_20; 
+x_19 = lean_ctor_get(x_17, 0);
+lean_inc(x_19);
+x_20 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_19);
+lean_dec(x_19);
+if (lean_obj_tag(x_20) == 2)
 {
-lean_object* x_12; lean_object* x_13; uint8_t x_14; 
-x_12 = lean_ctor_get(x_11, 1);
-lean_inc(x_12);
-lean_dec(x_11);
-x_13 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__2;
-x_14 = lean_string_dec_eq(x_12, x_13);
-lean_dec(x_12);
-if (x_14 == 0)
+lean_object* x_21; lean_object* x_22; uint8_t x_23; 
+x_21 = lean_ctor_get(x_20, 1);
+lean_inc(x_21);
+lean_dec(x_20);
+x_22 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__2;
+x_23 = lean_string_dec_eq(x_21, x_22);
+lean_dec(x_21);
+if (x_23 == 0)
 {
-lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
-lean_dec(x_2);
-x_15 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__5;
-x_16 = l_Lean_Parser_ParserState_mkErrorsAt(x_8, x_15, x_7);
-x_17 = l_Lean_Parser_Term_where___elambda__1___closed__2;
-x_18 = l_Lean_Parser_ParserState_mkTrailingNode(x_16, x_17, x_5);
-lean_dec(x_5);
-return x_18;
-}
-else
-{
-uint8_t x_19; uint8_t x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
-lean_dec(x_7);
-x_19 = 1;
-x_20 = 0;
-x_21 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_where___elambda__1___spec__1(x_19, x_20, x_20, x_1, x_2, x_8);
-x_22 = l_Lean_Parser_Term_where___elambda__1___closed__2;
-x_23 = l_Lean_Parser_ParserState_mkTrailingNode(x_21, x_22, x_5);
-lean_dec(x_5);
-return x_23;
-}
-}
-else
-{
-lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; 
-lean_dec(x_11);
-lean_dec(x_2);
+lean_object* x_24; lean_object* x_25; 
 x_24 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__5;
-x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_8, x_24, x_7);
-x_26 = l_Lean_Parser_Term_where___elambda__1___closed__2;
-x_27 = l_Lean_Parser_ParserState_mkTrailingNode(x_25, x_26, x_5);
-lean_dec(x_5);
-return x_27;
+x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_24, x_16);
+x_6 = x_25;
+goto block_15;
+}
+else
+{
+lean_dec(x_16);
+x_6 = x_17;
+goto block_15;
 }
 }
 else
 {
-lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; 
-lean_dec(x_9);
-lean_dec(x_2);
+lean_object* x_26; lean_object* x_27; 
+lean_dec(x_20);
+x_26 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__5;
+x_27 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_26, x_16);
+x_6 = x_27;
+goto block_15;
+}
+}
+else
+{
+lean_object* x_28; lean_object* x_29; 
+lean_dec(x_18);
 x_28 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__5;
-x_29 = l_Lean_Parser_ParserState_mkErrorsAt(x_8, x_28, x_7);
-x_30 = l_Lean_Parser_Term_where___elambda__1___closed__2;
-x_31 = l_Lean_Parser_ParserState_mkTrailingNode(x_29, x_30, x_5);
-lean_dec(x_5);
-return x_31;
+x_29 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_28, x_16);
+x_6 = x_29;
+goto block_15;
 }
+block_15:
+{
+lean_object* x_7; 
+x_7 = lean_ctor_get(x_6, 3);
+lean_inc(x_7);
+if (lean_obj_tag(x_7) == 0)
+{
+uint8_t x_8; uint8_t x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_8 = 1;
+x_9 = 0;
+x_10 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_where___elambda__1___spec__1(x_8, x_9, x_9, x_1, x_2, x_6);
+x_11 = l_Lean_Parser_Term_where___elambda__1___closed__2;
+x_12 = l_Lean_Parser_ParserState_mkTrailingNode(x_10, x_11, x_5);
+lean_dec(x_5);
+return x_12;
 }
 else
 {
-lean_object* x_32; lean_object* x_33; 
-lean_dec(x_6);
+lean_object* x_13; lean_object* x_14; 
+lean_dec(x_7);
 lean_dec(x_2);
-x_32 = l_Lean_Parser_Term_where___elambda__1___closed__2;
-x_33 = l_Lean_Parser_ParserState_mkTrailingNode(x_3, x_32, x_5);
+x_13 = l_Lean_Parser_Term_where___elambda__1___closed__2;
+x_14 = l_Lean_Parser_ParserState_mkTrailingNode(x_6, x_13, x_5);
 lean_dec(x_5);
-return x_33;
+return x_14;
+}
 }
 }
 }
@@ -33302,23 +33175,13 @@ lean_object* _init_l_Lean_Parser_Term_where___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_Term_where___closed__6;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Term_where___closed__8() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_where___elambda__1___closed__2;
-x_2 = l_Lean_Parser_Term_where___closed__7;
+x_2 = l_Lean_Parser_Term_where___closed__6;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_where___closed__9() {
+lean_object* _init_l_Lean_Parser_Term_where___closed__8() {
 _start:
 {
 lean_object* x_1; 
@@ -33326,12 +33189,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_where___elambda__1___boxed),
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Term_where___closed__10() {
+lean_object* _init_l_Lean_Parser_Term_where___closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_where___closed__8;
-x_2 = l_Lean_Parser_Term_where___closed__9;
+x_1 = l_Lean_Parser_Term_where___closed__7;
+x_2 = l_Lean_Parser_Term_where___closed__8;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -33342,7 +33205,7 @@ lean_object* _init_l_Lean_Parser_Term_where() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Term_where___closed__10;
+x_1 = l_Lean_Parser_Term_where___closed__9;
 return x_1;
 }
 }
@@ -39868,8 +39731,6 @@ l_Lean_Parser_Term_app___closed__4 = _init_l_Lean_Parser_Term_app___closed__4();
 lean_mark_persistent(l_Lean_Parser_Term_app___closed__4);
 l_Lean_Parser_Term_app___closed__5 = _init_l_Lean_Parser_Term_app___closed__5();
 lean_mark_persistent(l_Lean_Parser_Term_app___closed__5);
-l_Lean_Parser_Term_app___closed__6 = _init_l_Lean_Parser_Term_app___closed__6();
-lean_mark_persistent(l_Lean_Parser_Term_app___closed__6);
 l_Lean_Parser_Term_app = _init_l_Lean_Parser_Term_app();
 lean_mark_persistent(l_Lean_Parser_Term_app);
 res = l___regBuiltinParser_Lean_Parser_Term_app(lean_io_mk_world());
@@ -39895,8 +39756,6 @@ l_Lean_Parser_Term_sortApp___closed__4 = _init_l_Lean_Parser_Term_sortApp___clos
 lean_mark_persistent(l_Lean_Parser_Term_sortApp___closed__4);
 l_Lean_Parser_Term_sortApp___closed__5 = _init_l_Lean_Parser_Term_sortApp___closed__5();
 lean_mark_persistent(l_Lean_Parser_Term_sortApp___closed__5);
-l_Lean_Parser_Term_sortApp___closed__6 = _init_l_Lean_Parser_Term_sortApp___closed__6();
-lean_mark_persistent(l_Lean_Parser_Term_sortApp___closed__6);
 l_Lean_Parser_Term_sortApp = _init_l_Lean_Parser_Term_sortApp();
 lean_mark_persistent(l_Lean_Parser_Term_sortApp);
 res = l___regBuiltinParser_Lean_Parser_Term_sortApp(lean_io_mk_world());
@@ -39936,8 +39795,6 @@ l_Lean_Parser_Term_proj___closed__8 = _init_l_Lean_Parser_Term_proj___closed__8(
 lean_mark_persistent(l_Lean_Parser_Term_proj___closed__8);
 l_Lean_Parser_Term_proj___closed__9 = _init_l_Lean_Parser_Term_proj___closed__9();
 lean_mark_persistent(l_Lean_Parser_Term_proj___closed__9);
-l_Lean_Parser_Term_proj___closed__10 = _init_l_Lean_Parser_Term_proj___closed__10();
-lean_mark_persistent(l_Lean_Parser_Term_proj___closed__10);
 l_Lean_Parser_Term_proj = _init_l_Lean_Parser_Term_proj();
 lean_mark_persistent(l_Lean_Parser_Term_proj);
 res = l___regBuiltinParser_Lean_Parser_Term_proj(lean_io_mk_world());
@@ -39982,8 +39839,6 @@ l_Lean_Parser_Term_arrayRef___closed__6 = _init_l_Lean_Parser_Term_arrayRef___cl
 lean_mark_persistent(l_Lean_Parser_Term_arrayRef___closed__6);
 l_Lean_Parser_Term_arrayRef___closed__7 = _init_l_Lean_Parser_Term_arrayRef___closed__7();
 lean_mark_persistent(l_Lean_Parser_Term_arrayRef___closed__7);
-l_Lean_Parser_Term_arrayRef___closed__8 = _init_l_Lean_Parser_Term_arrayRef___closed__8();
-lean_mark_persistent(l_Lean_Parser_Term_arrayRef___closed__8);
 l_Lean_Parser_Term_arrayRef = _init_l_Lean_Parser_Term_arrayRef();
 lean_mark_persistent(l_Lean_Parser_Term_arrayRef);
 res = l___regBuiltinParser_Lean_Parser_Term_arrayRef(lean_io_mk_world());
@@ -40007,8 +39862,6 @@ l_Lean_Parser_Term_dollar___closed__5 = _init_l_Lean_Parser_Term_dollar___closed
 lean_mark_persistent(l_Lean_Parser_Term_dollar___closed__5);
 l_Lean_Parser_Term_dollar___closed__6 = _init_l_Lean_Parser_Term_dollar___closed__6();
 lean_mark_persistent(l_Lean_Parser_Term_dollar___closed__6);
-l_Lean_Parser_Term_dollar___closed__7 = _init_l_Lean_Parser_Term_dollar___closed__7();
-lean_mark_persistent(l_Lean_Parser_Term_dollar___closed__7);
 l_Lean_Parser_Term_dollar = _init_l_Lean_Parser_Term_dollar();
 lean_mark_persistent(l_Lean_Parser_Term_dollar);
 res = l___regBuiltinParser_Lean_Parser_Term_dollar(lean_io_mk_world());
@@ -40038,8 +39891,6 @@ l_Lean_Parser_Term_dollarProj___closed__4 = _init_l_Lean_Parser_Term_dollarProj_
 lean_mark_persistent(l_Lean_Parser_Term_dollarProj___closed__4);
 l_Lean_Parser_Term_dollarProj___closed__5 = _init_l_Lean_Parser_Term_dollarProj___closed__5();
 lean_mark_persistent(l_Lean_Parser_Term_dollarProj___closed__5);
-l_Lean_Parser_Term_dollarProj___closed__6 = _init_l_Lean_Parser_Term_dollarProj___closed__6();
-lean_mark_persistent(l_Lean_Parser_Term_dollarProj___closed__6);
 l_Lean_Parser_Term_dollarProj = _init_l_Lean_Parser_Term_dollarProj();
 lean_mark_persistent(l_Lean_Parser_Term_dollarProj);
 res = l___regBuiltinParser_Lean_Parser_Term_dollarProj(lean_io_mk_world());
@@ -40077,8 +39928,6 @@ l_Lean_Parser_Term_where___closed__8 = _init_l_Lean_Parser_Term_where___closed__
 lean_mark_persistent(l_Lean_Parser_Term_where___closed__8);
 l_Lean_Parser_Term_where___closed__9 = _init_l_Lean_Parser_Term_where___closed__9();
 lean_mark_persistent(l_Lean_Parser_Term_where___closed__9);
-l_Lean_Parser_Term_where___closed__10 = _init_l_Lean_Parser_Term_where___closed__10();
-lean_mark_persistent(l_Lean_Parser_Term_where___closed__10);
 l_Lean_Parser_Term_where = _init_l_Lean_Parser_Term_where();
 lean_mark_persistent(l_Lean_Parser_Term_where);
 res = l___regBuiltinParser_Lean_Parser_Term_where(lean_io_mk_world());
diff --git a/stage0/stdlib/Init/LeanInit.c b/stage0/stdlib/Init/LeanInit.c
index 2f2db9429c..8b83777eb1 100644
--- a/stage0/stdlib/Init/LeanInit.c
+++ b/stage0/stdlib/Init/LeanInit.c
@@ -267,6 +267,7 @@ lean_object* l_Lean_ParserDescrCore_inhabited___boxed(lean_object*);
 uint8_t l_Lean_Name_hasMacroScopes___main(lean_object*);
 lean_object* l_Lean_ParserDescr_strLit___boxed(lean_object*);
 lean_object* l_Lean_identKind;
+lean_object* l_Lean_ParserDescr_trailingNode(lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_sepBy1(uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_mkCTermId(lean_object*);
 uint8_t l_UInt32_decEq(uint32_t, uint32_t);
@@ -1536,7 +1537,7 @@ _start:
 lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_2 = lean_box(0);
 x_3 = l_String_splitAux___main___closed__1;
-x_4 = lean_alloc_ctor(10, 2, 1);
+x_4 = lean_alloc_ctor(11, 2, 1);
 lean_ctor_set(x_4, 0, x_3);
 lean_ctor_set(x_4, 1, x_2);
 lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
@@ -1758,11 +1759,21 @@ x_5 = l_Lean_ParserDescr_node(x_4, x_2, x_3);
 return x_5;
 }
 }
+lean_object* l_Lean_ParserDescr_trailingNode(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_3, 0, x_1);
+lean_ctor_set(x_3, 1, x_2);
+return x_3;
+}
+}
 lean_object* l_Lean_ParserDescr_symbol(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; 
-x_4 = lean_alloc_ctor(10, 2, 1);
+x_4 = lean_alloc_ctor(11, 2, 1);
 lean_ctor_set(x_4, 0, x_2);
 lean_ctor_set(x_4, 1, x_3);
 lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
@@ -1783,7 +1794,7 @@ lean_object* l_Lean_ParserDescr_numLit(uint8_t x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_ctor(12, 0, 1);
+x_2 = lean_alloc_ctor(13, 0, 1);
 lean_ctor_set_uint8(x_2, 0, x_1);
 return x_2;
 }
@@ -1802,7 +1813,7 @@ lean_object* l_Lean_ParserDescr_strLit(uint8_t x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_ctor(13, 0, 1);
+x_2 = lean_alloc_ctor(14, 0, 1);
 lean_ctor_set_uint8(x_2, 0, x_1);
 return x_2;
 }
@@ -1821,7 +1832,7 @@ lean_object* l_Lean_ParserDescr_charLit(uint8_t x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_ctor(14, 0, 1);
+x_2 = lean_alloc_ctor(15, 0, 1);
 lean_ctor_set_uint8(x_2, 0, x_1);
 return x_2;
 }
@@ -1840,7 +1851,7 @@ lean_object* l_Lean_ParserDescr_nameLit(uint8_t x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_ctor(15, 0, 1);
+x_2 = lean_alloc_ctor(16, 0, 1);
 lean_ctor_set_uint8(x_2, 0, x_1);
 return x_2;
 }
@@ -1859,7 +1870,7 @@ lean_object* l_Lean_ParserDescr_ident(uint8_t x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_ctor(16, 0, 1);
+x_2 = lean_alloc_ctor(17, 0, 1);
 lean_ctor_set_uint8(x_2, 0, x_1);
 return x_2;
 }
@@ -1878,7 +1889,7 @@ lean_object* l_Lean_ParserDescr_nonReservedSymbol(lean_object* x_1, uint8_t x_2)
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_alloc_ctor(11, 1, 1);
+x_3 = lean_alloc_ctor(12, 1, 1);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
 return x_3;
@@ -1898,7 +1909,7 @@ lean_object* _init_l_Lean_ParserDescr_pushLeading() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_box(17);
+x_1 = lean_box(18);
 return x_1;
 }
 }
@@ -1906,7 +1917,7 @@ lean_object* l_Lean_ParserDescr_parser(uint8_t x_1, lean_object* x_2, lean_objec
 _start:
 {
 lean_object* x_4; 
-x_4 = lean_alloc_ctor(18, 2, 1);
+x_4 = lean_alloc_ctor(19, 2, 1);
 lean_ctor_set(x_4, 0, x_2);
 lean_ctor_set(x_4, 1, x_3);
 lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);