chore: update stage0

2020-01-14 18:23:24 -08:00 · 2020-01-14 18:23:24 -08:00 · 07abef89c5
commit 07abef89c5
parent 664172d266
27 changed files with 10217 additions and 4104 deletions
--- a/stage0/src/Init/Default.lean
+++ b/stage0/src/Init/Default.lean
@ -13,3 +13,4 @@ import Init.Data
 import Init.System
 import Init.Util
 import Init.Fix
+import Init.LeanExt
--- a/stage0/src/Init/Lean/Data/Name.lean
+++ b/stage0/src/Init/Lean/Data/Name.lean
@ -14,29 +14,6 @@ import Init.Data.RBTree

 namespace Lean

-instance Name.inhabited : Inhabited Name :=
-⟨Name.anonymous⟩
-
-def Name.hash : Name → USize
-| Name.anonymous => 1723
-| Name.str p s h => h
-| Name.num p v h => h
-
-instance Name.hashable : Hashable Name := ⟨Name.hash⟩
-
-@[export lean_name_hash] def Name.hashEx : Name → USize := Name.hash
-
-@[export lean_name_mk_string]
-def mkNameStr (p : Name) (s : String) : Name :=
-Name.str p s $ mixHash (hash p) (hash s)
-
-@[export lean_name_mk_numeral]
-def mkNameNum (p : Name) (v : Nat) : Name :=
-Name.num p v $ mixHash (hash p) (hash v)
-
-def mkNameSimple (s : String) : Name :=
-mkNameStr Name.anonymous s
-
 instance stringToName : HasCoe String Name :=
 ⟨mkNameSimple⟩

--- a/stage0/src/Init/Lean/Elab.lean
+++ b/stage0/src/Init/Lean/Elab.lean
@ -16,3 +16,4 @@ import Init.Lean.Elab.Frontend
 import Init.Lean.Elab.BuiltinNotation
 import Init.Lean.Elab.Declaration
 import Init.Lean.Elab.Tactic
+import Init.Lean.Elab.Syntax
--- a/stage0/src/Init/Lean/Elab/Command.lean
+++ b/stage0/src/Init/Lean/Elab/Command.lean
@ -570,19 +570,6 @@ fun stx => do
  | Syntax.atom _ "false" => setOption ref optionName (DataValue.ofBool false)
  | _ => logError val ("unexpected set_option value " ++ toString val)

-@[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab :=
-fun stx => do
-  let catName  := stx.getIdAt 1;
-  let attrName := catName.appendAfter "Parser";
-  env ← getEnv;
-  env ← liftIO stx $ Parser.registerParserCategory env attrName catName;
-  setEnv env
-
-
-@[builtinCommandElab syntax] def elabSyntax : CommandElab :=
-fun stx =>
-  throwError stx ("not implemented yet " ++ toString stx)
-
@[inline] def withDeclId (declId : Syntax) (f : Name → CommandElabM Unit) : CommandElabM Unit := do
 -- ident >> optional (".{" >> sepBy1 ident ", " >> "}")
 let id             := declId.getIdAt 0;
--- a/stage0/src/Init/Lean/Elab/Quotation.lean
+++ b/stage0/src/Init/Lean/Elab/Quotation.lean
@ -39,23 +39,29 @@ private def quoteName : Name → Syntax
 | Name.str n s _ => Unhygienic.run `(_root_.Lean.mkNameStr $(quoteName n) $(quote s))
 | Name.num n i _ => Unhygienic.run `(_root_.Lean.mkNameNum $(quoteName n) $(quote i))

-instance Name.HasQuote : HasQuote Name := ⟨quoteName⟩
+instance Name.hasQuote : HasQuote Name := ⟨quoteName⟩

 private def appN (fn : Syntax) (args : Array Syntax) : Syntax :=
 args.foldl (fun fn arg => Unhygienic.run `($fn $arg)) fn

-instance Prod.HasQuote {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) :=
+instance Prod.hasQuote {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) :=
 ⟨fun ⟨a, b⟩ => Unhygienic.run `(_root_.Prod.mk $(quote a) $(quote b))⟩

 private def quoteList {α : Type} [HasQuote α] : List α → Syntax
 | [] =>      Unhygienic.run `(_root_.List.nil)
 | (x::xs) => Unhygienic.run `(_root_.List.cons $(quote x) $(quoteList xs))

-instance List.HasQuote {α : Type} [HasQuote α] : HasQuote (List α) := ⟨quoteList⟩
+instance List.hasQuote {α : Type} [HasQuote α] : HasQuote (List α) := ⟨quoteList⟩

-instance Array.HasQuote {α : Type} [HasQuote α] : HasQuote (Array α) :=
+instance Array.hasQuote {α : Type} [HasQuote α] : HasQuote (Array α) :=
 ⟨fun xs => let stx := quote xs.toList; Unhygienic.run `(_root_.List.toArray $stx)⟩

+private def quoteOption {α : Type} [HasQuote α] : Option α → Syntax
+| none     => Unhygienic.run `(_root_.Option.none)
+| (some x) => Unhygienic.run `(_root_.Option.some $(quote x))
+
+instance Option.hasQuote {α : Type} [HasQuote α] : HasQuote (Option α) := ⟨quoteOption⟩
+
 namespace Elab
 namespace Term

--- a/stage0/src/Init/Lean/Elab/Syntax.lean
+++ b/stage0/src/Init/Lean/Elab/Syntax.lean
@ -0,0 +1,117 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Elab.Command
+import Init.Lean.Elab.Quotation
+
+namespace Lean
+namespace Elab
+
+namespace Term
+
+-- optional (":" >> numLit)
+private def getOptNum (stx : Syntax) : Option Nat :=
+if stx.isNone then none
+else (stx.getArg 1).isNatLit?
+
+private def mkParserSeq (ds : Array Syntax) : TermElabM Syntax :=
+if ds.size == 0 then
+  throwUnsupportedSyntax
+else if ds.size == 1 then
+  pure $ ds.get! 0
+else
+  ds.foldlFromM (fun r d => `(ParserDescr.andthen $r $d)) (ds.get! 0) 1
+
+partial def toParserDescr : Syntax → TermElabM Syntax
+| stx =>
+  let kind := stx.getKind;
+  if kind == nullKind then do
+     args ← stx.getArgs.mapM toParserDescr;
+     mkParserSeq args
+  else if kind == choiceKind then do
+    toParserDescr (stx.getArg 0)
+  else if kind == `Lean.Parser.Syntax.paren then
+    toParserDescr (stx.getArg 1)
+  else if kind == `Lean.Parser.Syntax.cat then do
+    let cat : Name := stx.getIdAt 0;
+    let rbp : Nat  := (getOptNum (stx.getArg 1)).getD 0;
+    env ← getEnv;
+    unless (Parser.isParserCategory env cat) $ throwError (stx.getArg 3) ("unknown category '" ++ cat ++ "'");
+    `(ParserDescr.parser $(quote cat) $(quote rbp))
+  else if kind == `Lean.Parser.Syntax.atom then do
+    match (stx.getArg 0).isStrLit? with
+    | some atom =>
+      let rbp : Option Nat  := getOptNum (stx.getArg 1);
+      `(ParserDescr.symbol $(quote atom) $(quote rbp))
+    | none => throwUnsupportedSyntax
+  else if kind == `Lean.Parser.Syntax.num then
+    `(ParserDescr.num)
+  else if kind == `Lean.Parser.Syntax.str then
+    `(ParserDescr.str)
+  else if kind == `Lean.Parser.Syntax.char then
+    `(ParserDescr.char)
+  else if kind == `Lean.Parser.Syntax.ident then
+    `(ParserDescr.ident)
+  else if kind == `Lean.Parser.Syntax.try then do
+    d ← toParserDescr $ stx.getArg 1;
+    `(ParserDescr.try $d)
+  else if kind == `Lean.Parser.Syntax.lookahead then do
+    d ← toParserDescr $ stx.getArg 1;
+    `(ParserDescr.lookahead $d)
+  else if kind == `Lean.Parser.Syntax.optional then do
+    d ← toParserDescr $ stx.getArg 1;
+    `(ParserDescr.optional $d)
+  else if kind == `Lean.Parser.Syntax.sepBy then do
+    d₁ ← toParserDescr $ stx.getArg 1;
+    d₂ ← toParserDescr $ stx.getArg 2;
+    `(ParserDescr.sepBy $d₁ $d₂)
+  else if kind == `Lean.Parser.Syntax.sepBy1 then do
+    d₁ ← toParserDescr $ stx.getArg 1;
+    d₂ ← toParserDescr $ stx.getArg 2;
+    `(ParserDescr.sepBy1 $d₁ $d₂)
+  else if kind == `Lean.Parser.Syntax.many then do
+    d ← toParserDescr $ stx.getArg 0;
+    `(ParserDescr.many $d)
+  else if kind == `Lean.Parser.Syntax.many1 then do
+    d ← toParserDescr $ stx.getArg 0;
+    `(ParserDescr.many1 $d)
+  else if kind == `Lean.Parser.Syntax.orelse then do
+    d₁ ← toParserDescr $ stx.getArg 0;
+    d₂ ← toParserDescr $ stx.getArg 2;
+    `(ParserDescr.orelse $d₁ $d₂)
+  else
+    throwError stx ("ERROR " ++ toString stx)
+    -- throwUnsupportedSyntax
+
+end Term
+
+namespace Command
+
+@[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab :=
+fun stx => do
+  let catName  := stx.getIdAt 1;
+  let attrName := catName.appendAfter "Parser";
+  env ← getEnv;
+  env ← liftIO stx $ Parser.registerParserCategory env attrName catName;
+  setEnv env
+
+@[builtinCommandElab syntax] def elabSyntax : CommandElab :=
+fun stx => do
+  env ← getEnv;
+  let cat := stx.getIdAt 3;
+  unless (Parser.isParserCategory env cat) $ throwError (stx.getArg 3) ("unknown category '" ++ cat ++ "'");
+  let (env, kind) := Parser.mkFreshKind env cat;
+  setEnv env;
+  let catParserId := mkIdentFrom stx (cat.appendAfter "Parser");
+  type ← `(Lean.ParserDescr);
+  val  ← runTermElabM none $ fun _ => Term.toParserDescr (stx.getArg 1);
+  d ← `(@[$catParserId:ident] private def $catParserId:ident : $type := ParserDescr.node $(quote kind) $val);
+  trace `Elab stx $ fun _ => d;
+  withMacroExpansion stx $ elabCommand d
+
+end Command
+end Elab
+end Lean
--- a/stage0/src/Init/Lean/Parser/Level.lean
+++ b/stage0/src/Init/Lean/Parser/Level.lean
@ -12,9 +12,6 @@ namespace Parser
@[init] def regBuiltinLevelParserAttr : IO Unit :=
 registerBuiltinParserAttribute `builtinLevelParser `level

-@[init] def regLevelParserAttribute : IO Unit :=
-registerBuiltinDynamicParserAttribute `levelParser `level
-
@[inline] def levelParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
 categoryParser `level rbp

--- a/stage0/src/Init/Lean/Parser/Parser.lean
+++ b/stage0/src/Init/Lean/Parser/Parser.lean
@ -1395,10 +1395,11 @@ inductive ParserExtensionEntry
 | parser   (catName : Name) (declName : Name) (k : ParserKind) (p : Parser k) : ParserExtensionEntry

 structure ParserExtensionState :=
-(tokens     : TokenTable := {})
-(kinds      : SyntaxNodeKindSet := {})
-(categories : ParserCategories := {})
-(newEntries : List ParserExtensionOleanEntry := [])
+(tokens      : TokenTable := {})
+(kinds       : SyntaxNodeKindSet := {})
+(categories  : ParserCategories := {})
+(newEntries  : List ParserExtensionOleanEntry := [])
+(nextKindIdx : Nat := 1)

 instance ParserExtensionState.inhabited : Inhabited ParserExtensionState := ⟨{}⟩

@ -1590,6 +1591,18 @@ registerPersistentEnvExtension {
@[init mkParserExtension]
 constant parserExtension : ParserExtension := arbitrary _

+partial def mkFreshKindAux (kinds : SyntaxNodeKindSet) (base : Name) : Nat → Name × Nat
+| currIdx =>
+  let candidate := base.appendIndexAfter currIdx;
+  if kinds.contains candidate then mkFreshKindAux (currIdx+1)
+  else (candidate, currIdx)
+
+def mkFreshKind (env : Environment) (part : Name) : Environment × Name :=
+let s := parserExtension.getState env;
+let (kind, idx) := mkFreshKindAux s.kinds (`_kind ++ env.mainModule ++ part) s.nextKindIdx;
+let env := parserExtension.setState env { nextKindIdx := idx+1, .. s };
+(env, kind)
+
 def isParserCategory (env : Environment) (catName : Name) : Bool :=
 (parserExtension.getState env).categories.contains catName

@ -1812,20 +1825,6 @@ mkAntiquot "fieldIdx" `fieldIdx <|>
 { fn   := fun _ => fieldIdxFn,
  info := mkAtomicInfo "fieldIdx" }

-/- Helper functions for defining simple parsers -/
-
-def unicodeInfixR (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
-pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser (lbp - 1)
-
-def infixR (sym : String) (lbp : Nat) : TrailingParser :=
-pushLeading >> symbol sym lbp >> termParser (lbp - 1)
-
-def unicodeInfixL (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
-pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser lbp
-
-def infixL (sym : String) (lbp : Nat) : TrailingParser :=
-pushLeading >> symbol sym lbp >> termParser lbp
-
 end Parser

 namespace Syntax
--- a/stage0/src/Init/Lean/Parser/Syntax.lean
+++ b/stage0/src/Init/Lean/Parser/Syntax.lean
@ -13,17 +13,14 @@ namespace Parser
 let leadingIdentAsSymbol := true;
 registerBuiltinParserAttribute `builtinSyntaxParser `syntax leadingIdentAsSymbol

-@[init] def regSyntaxParserAttribute : IO Unit :=
-registerBuiltinDynamicParserAttribute `syntaxParser `syntax
-
@[inline] def syntaxParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
 categoryParser `syntax rbp

 namespace Syntax

@[builtinSyntaxParser] def paren     := parser! "(" >> many1 syntaxParser >> ")"
-@[builtinSyntaxParser] def cat       := parser! ident >> optional (":" >> numLit)
-@[builtinSyntaxParser] def atom      := parser! strLit >> optional (":" >> numLit)
+@[builtinSyntaxParser] def cat       := parser! ident >> optional (try (":" >> numLit))
+@[builtinSyntaxParser] def atom      := parser! strLit >> optional (try (":" >> numLit))
@[builtinSyntaxParser] def num       := parser! nonReservedSymbol "num"
@[builtinSyntaxParser] def str       := parser! nonReservedSymbol "str"
@[builtinSyntaxParser] def char      := parser! nonReservedSymbol "char"
@ -36,7 +33,7 @@ namespace Syntax

@[builtinSyntaxParser] def many     := tparser! pushLeading >> symbolAux "*" none
@[builtinSyntaxParser] def many1    := tparser! pushLeading >> symbolAux "+" none
-@[builtinSyntaxParser] def orelse   := tparser! infixR " <|> " 2
+@[builtinSyntaxParser] def orelse   := tparser! pushLeading >> " <|> " >> syntaxParser 1

 end Syntax

--- a/stage0/src/Init/Lean/Parser/Tactic.lean
+++ b/stage0/src/Init/Lean/Parser/Tactic.lean
@ -30,7 +30,7 @@ namespace Tactic
@[builtinTacticParser] def «apply» := parser! nonReservedSymbol "apply " >> termParser
@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> tacticSeq >> "end"
@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> tacticSeq >> "}"
-@[builtinTacticParser] def orelse := tparser! infixR " <|> " 2
+@[builtinTacticParser] def orelse := tparser! pushLeading >> " <|> " >> tacticParser 1

 end Tactic

--- a/stage0/src/Init/Lean/Parser/Term.lean
+++ b/stage0/src/Init/Lean/Parser/Term.lean
@ -11,6 +11,20 @@ namespace Lean
 namespace Parser
 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)
+
+def infixR (sym : String) (lbp : Nat) : TrailingParser :=
+pushLeading >> symbol sym lbp >> termParser (lbp - 1)
+
+def unicodeInfixL (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
+pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser lbp
+
+def infixL (sym : String) (lbp : Nat) : TrailingParser :=
+pushLeading >> symbol sym lbp >> termParser lbp
+
 /- Built-in parsers -/
 -- NOTE: `checkNoWsBefore` should be used *before* `parser!` so that it is also applied to the generated
 -- antiquotation.
--- a/stage0/src/Init/LeanExt.lean
+++ b/stage0/src/Init/LeanExt.lean
@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.String.Basic
 import Init.Data.UInt
+import Init.Data.Hashable

 namespace Lean
 /-
@ -23,6 +24,29 @@ inductive Name
 | str : Name → String → USize → Name
 | num : Name → Nat → USize → Name

+instance Name.inhabited : Inhabited Name :=
+⟨Name.anonymous⟩
+
+def Name.hash : Name → USize
+| Name.anonymous => 1723
+| Name.str p s h => h
+| Name.num p v h => h
+
+instance Name.hashable : Hashable Name := ⟨Name.hash⟩
+
+@[export lean_name_hash] def Name.hashEx : Name → USize := Name.hash
+
+@[export lean_name_mk_string]
+def mkNameStr (p : Name) (s : String) : Name :=
+Name.str p s $ mixHash (hash p) (hash s)
+
+@[export lean_name_mk_numeral]
+def mkNameNum (p : Name) (v : Nat) : Name :=
+Name.num p v $ mixHash (hash p) (hash v)
+
+def mkNameSimple (s : String) : Name :=
+mkNameStr Name.anonymous s
+
 inductive ParserKind
 | leading | trailing

--- a/stage0/stdlib/CMakeLists.txt
+++ b/stage0/stdlib/CMakeLists.txt
--- a/stage0/stdlib/Init/Default.c
+++ b/stage0/stdlib/Init/Default.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Default
-// Imports: Init.Core Init.Control Init.Data.Basic Init.Coe Init.WF Init.Data Init.System Init.Util Init.Fix
+// Imports: Init.Core Init.Control Init.Data.Basic Init.Coe Init.WF Init.Data Init.System Init.Util Init.Fix Init.LeanExt
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -22,6 +22,7 @@ lean_object* initialize_Init_Data(lean_object*);
 lean_object* initialize_Init_System(lean_object*);
 lean_object* initialize_Init_Util(lean_object*);
 lean_object* initialize_Init_Fix(lean_object*);
+lean_object* initialize_Init_LeanExt(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Default(lean_object* w) {
 lean_object * res;
@ -54,6 +55,9 @@ lean_dec_ref(res);
 res = initialize_Init_Fix(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_LeanExt(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus
--- a/stage0/stdlib/Init/Lean/Data/Name.c
+++ b/stage0/stdlib/Init/Lean/Data/Name.c
@ -40,8 +40,6 @@ lean_object* l_Lean_Name_HasToString___closed__1;
 lean_object* l_Lean_mkNameSimple(lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
 uint8_t l_Lean_Name_isPrefixOf(lean_object*, lean_object*);
-lean_object* l_Lean_Name_inhabited;
-lean_object* l_Lean_Name_hashable___closed__1;
 lean_object* l_Lean_Name_lt___boxed(lean_object*, lean_object*);
 lean_object* l_RBNode_find___main___at_Lean_NameSet_contains___spec__1(lean_object*, lean_object*);
 lean_object* l_String_splitOn(lean_object*, lean_object*);
@ -53,7 +51,6 @@ lean_object* l_Lean_Name_lt___main___boxed(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1(lean_object*);
 lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*);
-lean_object* l_Lean_Name_hashable;
 lean_object* l_Lean_NameMap_insert___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_HasAppend___closed__1;
 lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
@ -69,8 +66,6 @@ lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
 lean_object* l_Lean_Name_components_x27(lean_object*);
 lean_object* l_Lean_NameMap_contains(lean_object*);
 lean_object* l_Lean_Name_toString(lean_object*);
-lean_object* l_Lean_Name_hashEx___boxed(lean_object*);
-size_t lean_name_hash(lean_object*);
 lean_object* l_RBNode_find___main___at_Lean_NameMap_contains___spec__1(lean_object*);
 uint8_t l_Lean_Name_isInternal(lean_object*);
 lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
@ -90,7 +85,6 @@ lean_object* l_Lean_Name_toStringWithSep___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_isInternal___main___boxed(lean_object*);
 lean_object* l_RBNode_insert___at_Lean_NameSet_insert___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkNameSet;
-size_t lean_usize_of_nat(lean_object*);
 lean_object* l_Lean_Name_quickLtAux___main___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_replacePrefix___main(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_stringToName___closed__1;
@ -121,7 +115,6 @@ lean_object* l_RBNode_setBlack___rarg(lean_object*);
 lean_object* l_Lean_Name_HasBeq___closed__1;
 lean_object* l_Lean_Name_append___main___boxed(lean_object*, lean_object*);
 lean_object* l_String_trim(lean_object*);
-size_t lean_usize_mix_hash(size_t, size_t);
 uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
 lean_object* l_Lean_Name_isPrefixOf___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_NameSet_insert(lean_object*, lean_object*);
@ -133,122 +126,14 @@ lean_object* l_Lean_mkNameMap(lean_object*);
 lean_object* l_RBNode_find___main___at_Lean_NameMap_find___spec__1___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
 lean_object* l_Lean_NameMap_find___rarg___boxed(lean_object*, lean_object*);
-lean_object* l_Lean_Name_hash___boxed(lean_object*);
 lean_object* l_Lean_Name_replacePrefix(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_components(lean_object*);
 lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
-size_t lean_string_hash(lean_object*);
 lean_object* l_RBNode_find___main___at_Lean_NameMap_find___spec__1___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_append___boxed(lean_object*, lean_object*);
 uint8_t lean_string_dec_lt(lean_object*, lean_object*);
 uint8_t lean_string_dec_eq(lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
-lean_object* _init_l_Lean_Name_inhabited() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_box(0);
-return x_1;
-}
-}
-size_t l_Lean_Name_hash(lean_object* x_1) {
-_start:
-{
-if (lean_obj_tag(x_1) == 0)
-{
-size_t x_2; 
-x_2 = 1723;
-return x_2;
-}
-else
-{
-size_t x_3; 
-x_3 = lean_ctor_get_usize(x_1, 2);
-return x_3;
-}
-}
-}
-lean_object* l_Lean_Name_hash___boxed(lean_object* x_1) {
-_start:
-{
-size_t x_2; lean_object* x_3; 
-x_2 = l_Lean_Name_hash(x_1);
-lean_dec(x_1);
-x_3 = lean_box_usize(x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Name_hashable___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Name_hash___boxed), 1, 0);
-return x_1;
-}
-}
-lean_object* _init_l_Lean_Name_hashable() {
-_start:
-{
-lean_object* x_1; 
-x_1 = l_Lean_Name_hashable___closed__1;
-return x_1;
-}
-}
-size_t lean_name_hash(lean_object* x_1) {
-_start:
-{
-size_t x_2; 
-x_2 = l_Lean_Name_hash(x_1);
-lean_dec(x_1);
-return x_2;
-}
-}
-lean_object* l_Lean_Name_hashEx___boxed(lean_object* x_1) {
-_start:
-{
-size_t x_2; lean_object* x_3; 
-x_2 = lean_name_hash(x_1);
-x_3 = lean_box_usize(x_2);
-return x_3;
-}
-}
-lean_object* lean_name_mk_string(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-size_t x_3; size_t x_4; size_t x_5; lean_object* x_6; 
-x_3 = l_Lean_Name_hash(x_1);
-x_4 = lean_string_hash(x_2);
-x_5 = lean_usize_mix_hash(x_3, x_4);
-x_6 = lean_alloc_ctor(1, 2, sizeof(size_t)*1);
-lean_ctor_set(x_6, 0, x_1);
-lean_ctor_set(x_6, 1, x_2);
-lean_ctor_set_usize(x_6, 2, x_5);
-return x_6;
-}
-}
-lean_object* lean_name_mk_numeral(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-size_t x_3; size_t x_4; size_t x_5; lean_object* x_6; 
-x_3 = l_Lean_Name_hash(x_1);
-x_4 = lean_usize_of_nat(x_2);
-x_5 = lean_usize_mix_hash(x_3, x_4);
-x_6 = lean_alloc_ctor(2, 2, sizeof(size_t)*1);
-lean_ctor_set(x_6, 0, x_1);
-lean_ctor_set(x_6, 1, x_2);
-lean_ctor_set_usize(x_6, 2, x_5);
-return x_6;
-}
-}
-lean_object* l_Lean_mkNameSimple(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; lean_object* x_3; 
-x_2 = lean_box(0);
-x_3 = lean_name_mk_string(x_2, x_1);
-return x_3;
-}
-}
 lean_object* _init_l_Lean_stringToName___closed__1() {
 _start:
 {
@ -9108,12 +8993,6 @@ lean_dec_ref(res);
 res = initialize_Init_Data_RBTree(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-l_Lean_Name_inhabited = _init_l_Lean_Name_inhabited();
-lean_mark_persistent(l_Lean_Name_inhabited);
-l_Lean_Name_hashable___closed__1 = _init_l_Lean_Name_hashable___closed__1();
-lean_mark_persistent(l_Lean_Name_hashable___closed__1);
-l_Lean_Name_hashable = _init_l_Lean_Name_hashable();
-lean_mark_persistent(l_Lean_Name_hashable);
 l_Lean_stringToName___closed__1 = _init_l_Lean_stringToName___closed__1();
 lean_mark_persistent(l_Lean_stringToName___closed__1);
 l_Lean_stringToName = _init_l_Lean_stringToName();
--- a/stage0/stdlib/Init/Lean/Elab.c
+++ b/stage0/stdlib/Init/Lean/Elab.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Elab
-// Imports: Init.Lean.Elab.Import Init.Lean.Elab.Exception Init.Lean.Elab.ElabStrategyAttrs Init.Lean.Elab.Command Init.Lean.Elab.Term Init.Lean.Elab.TermApp Init.Lean.Elab.TermBinders Init.Lean.Elab.Quotation Init.Lean.Elab.Frontend Init.Lean.Elab.BuiltinNotation Init.Lean.Elab.Declaration Init.Lean.Elab.Tactic
+// Imports: Init.Lean.Elab.Import Init.Lean.Elab.Exception Init.Lean.Elab.ElabStrategyAttrs Init.Lean.Elab.Command Init.Lean.Elab.Term Init.Lean.Elab.TermApp Init.Lean.Elab.TermBinders Init.Lean.Elab.Quotation Init.Lean.Elab.Frontend Init.Lean.Elab.BuiltinNotation Init.Lean.Elab.Declaration Init.Lean.Elab.Tactic Init.Lean.Elab.Syntax
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -25,6 +25,7 @@ lean_object* initialize_Init_Lean_Elab_Frontend(lean_object*);
 lean_object* initialize_Init_Lean_Elab_BuiltinNotation(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Declaration(lean_object*);
 lean_object* initialize_Init_Lean_Elab_Tactic(lean_object*);
+lean_object* initialize_Init_Lean_Elab_Syntax(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Lean_Elab(lean_object* w) {
 lean_object * res;
@ -66,6 +67,9 @@ lean_dec_ref(res);
 res = initialize_Init_Lean_Elab_Tactic(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Lean_Elab_Syntax(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus
--- a/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
+++ b/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
@ -54,6 +54,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOr___closed__3;
 lean_object* l_Lean_Elab_Term_elabseqLeft___closed__2;
 lean_object* l_Lean_Elab_Term_elabMod___closed__2;
 lean_object* l_Lean_Elab_Term_elabPow(lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Init_Lean_Elab_Quotation_15__toPreterm___main___lambda__3___closed__1;
 lean_object* l_Lean_Elab_Term_elabModN___closed__3;
 lean_object* l_Lean_Elab_Term_elabBOr___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabInfix(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -68,11 +69,11 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSubtype___closed__2;
 lean_object* l_Lean_Elab_Term_elabInfixOp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__18;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBNe(lean_object*);
-extern lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___elambda__3___closed__1;
 lean_object* l_Lean_Elab_Term_elabAnoymousCtor___closed__15;
 lean_object* l_Lean_Elab_Term_getDeclName_x3f(lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOrElse___closed__1;
 lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__14;
+extern lean_object* l___private_Init_Lean_Elab_Quotation_8__getHeadInfo___elambda__3___closed__1;
 lean_object* l_Lean_Elab_Term_elabBOr___closed__1;
 lean_object* l_Lean_Elab_Term_elabMul___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSub___closed__1;
@ -91,20 +92,19 @@ lean_object* l_Lean_Elab_Term_elabIf___lambda__1(lean_object*, lean_object*, lea
 extern lean_object* l_Lean_Parser_Term_show___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_elabSubtype___lambda__1___closed__9;
 lean_object* l_Lean_Elab_Term_elabMul___closed__2;
+extern lean_object* l___private_Init_Lean_Elab_Quotation_9__explodeHeadPat___lambda__1___closed__3;
 extern lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__2;
 extern lean_object* l_Array_empty___closed__1;
 lean_object* l_Lean_Elab_Term_elabPow___closed__3;
 lean_object* lean_environment_find(lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBAnd___closed__3;
 lean_object* l_Lean_Elab_Term_elabMod___closed__1;
-lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__34;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabIff___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMul___closed__3;
 lean_object* l_Lean_Elab_Term_elabIf___lambda__1___closed__6;
 lean_object* l_Lean_Elab_Term_elabHave___lambda__1(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___closed__2;
 extern lean_object* l_Lean_Parser_Term_mul___elambda__1___closed__1;
-extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabEquiv___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAdd(lean_object*);
 extern lean_object* l_Lean_Parser_Term_andM___elambda__1___closed__1;
@ -128,11 +128,9 @@ extern lean_object* l_Lean_Parser_Term_seqRight___elambda__1___closed__2;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAndThen(lean_object*);
 lean_object* l_Lean_Elab_Term_elabSubtype___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabCons___closed__1;
-extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabSubtype___lambda__1___closed__1;
 lean_object* lean_array_get_size(lean_object*);
-extern lean_object* l___private_Init_Lean_Elab_Quotation_8__explodeHeadPat___lambda__1___closed__3;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabEquiv___closed__2;
 lean_object* l_Lean_Elab_Term_elabModN(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMap(lean_object*);
@ -173,7 +171,6 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabseq___closed__1;
 lean_object* l___private_Init_Lean_Elab_Quotation_1__quoteName___main(lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabseqRight(lean_object*);
 extern lean_object* l___private_Init_Lean_Elab_Term_8__expandCDot___closed__4;
-extern lean_object* l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBAnd(lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHEq(lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMapConstRev(lean_object*);
@ -186,6 +183,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMapConst___closed__1;
 extern lean_object* l_Lean_Parser_Term_or___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_elabseq___closed__1;
 lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__19;
+extern lean_object* l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__31;
 extern lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__2;
 extern lean_object* l_Lean_Parser_Term_add___elambda__1___closed__1;
 extern lean_object* l_Lean_Parser_Term_add___elambda__1___closed__2;
@ -205,9 +203,11 @@ lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(lean_object*, lean_object*
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHave___closed__2;
 extern lean_object* l_Lean_Parser_Term_div___elambda__1___closed__2;
 lean_object* lean_array_fget(lean_object*, lean_object*);
+extern lean_object* l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__33;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabGT___closed__1;
 lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabseq___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Init_Lean_Elab_Quotation_15__toPreterm___main___lambda__3___closed__3;
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabModN(lean_object*);
 lean_object* l_Lean_Elab_Term_elabWhere___closed__1;
@ -217,7 +217,6 @@ lean_object* l_Lean_Elab_Term_elabseq___closed__2;
 extern lean_object* l_Lean_Parser_Term_band___elambda__1___closed__2;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabseqRight___closed__3;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHEq___closed__1;
-extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__36;
 extern lean_object* l_Lean_Parser_Term_id___elambda__1___closed__2;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSub(lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabGT___closed__2;
@ -240,7 +239,6 @@ extern lean_object* l_Lean_Parser_Term_div___elambda__1___closed__1;
 extern lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_elabShow___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSubtype___closed__3;
-lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__35;
 extern lean_object* l_Lean_Parser_Term_ge___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_elabseq___closed__3;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabseqLeft___closed__2;
@ -275,10 +273,12 @@ lean_object* l_Lean_Elab_Term_elabTParserMacro___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabShow___closed__3;
 lean_object* l_List_head_x21___at_Lean_Elab_Term_elabAnoymousCtor___spec__1(lean_object*);
 lean_object* l_Lean_Elab_Term_ElabFComp(lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Init_Lean_Elab_Quotation_4__quoteOption___rarg___lambda__2___closed__6;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabDiv___closed__3;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBNe___closed__3;
 lean_object* l_Lean_Elab_Term_elabProd___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__1;
+extern lean_object* l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 lean_object* l_Lean_Elab_Term_elabMapRev___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOrM___closed__2;
 lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__7;
@ -322,7 +322,6 @@ extern lean_object* l_Lean_Parser_Term_iff___elambda__1___closed__2;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAppend___closed__3;
 lean_object* l_Lean_Elab_Term_elabLE(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabDollar___closed__1;
-extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31;
 lean_object* l_Lean_Elab_Term_elabOr___closed__1;
 lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__3;
 lean_object* l_Lean_Elab_Term_elabMap___closed__3;
@ -367,8 +366,8 @@ lean_object* l_Lean_Elab_Term_elabMap___closed__1;
 lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__26;
 lean_object* l_Lean_Elab_Term_elabAnd___closed__2;
 extern lean_object* l_Lean_Parser_Term_mapConstRev___elambda__1___closed__2;
-extern lean_object* l___private_Init_Lean_Elab_Quotation_14__toPreterm___main___lambda__3___closed__1;
 lean_object* l_Lean_Elab_Term_elabIf___lambda__1___closed__8;
+extern lean_object* l___private_Init_Lean_Elab_Quotation_8__getHeadInfo___elambda__3___closed__10;
 lean_object* l_Lean_Elab_Term_elabMapConstRev___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabPow___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabDollarProj___closed__2;
@ -435,6 +434,7 @@ extern uint8_t l___private_Init_Lean_Elab_Term_7__hasCDot___main___closed__1;
 lean_object* l_Lean_Elab_Term_elabLE___closed__3;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabEq___closed__1;
 lean_object* l_Lean_Elab_Term_elabLT(lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__30;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBEq___closed__3;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabseqLeft___closed__3;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBOr(lean_object*);
@ -447,6 +447,7 @@ lean_object* l_Lean_Elab_Term_elabLE___closed__4;
 lean_object* l_Lean_Elab_Term_elabOrM___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabIff___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabCons___closed__3;
+extern lean_object* l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 extern lean_object* l_Lean_Parser_Term_paren___elambda__1___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabDollarProj___closed__3;
 lean_object* l_Lean_Elab_Term_elabSubtype___closed__1;
@ -483,6 +484,7 @@ lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOrM___closed__3;
 lean_object* l_Lean_Elab_Term_elabParserMacro___closed__1;
 lean_object* l_Lean_Elab_Term_ElabFComp___closed__3;
+extern lean_object* l___private_Init_Lean_Elab_Quotation_4__quoteOption___rarg___lambda__2___closed__4;
 lean_object* l_Lean_Elab_Term_elabAndThen___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabseqRight___closed__2;
 extern lean_object* l_Lean_Parser_Term_and___elambda__1___closed__2;
@ -493,7 +495,6 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabGT(lean_object*);
 extern lean_object* l_Lean_Parser_Term_mapRev___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Term_elabSubtype___lambda__1___closed__6;
 lean_object* l_Lean_Elab_Term_elabGT___closed__2;
-extern lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___elambda__3___closed__10;
 extern lean_object* l_Lean_mkOptionalNode___closed__1;
 lean_object* l_Lean_Expr_consumeMData___main(lean_object*);
 lean_object* l_Lean_Elab_Term_elabGT___closed__1;
@ -511,6 +512,7 @@ lean_object* l_Lean_Elab_Term_elabAnoymousCtor(lean_object*, lean_object*, lean_
 lean_object* l_Lean_Elab_Term_elabAndThen___closed__2;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabEquiv(lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabEq___closed__3;
+extern lean_object* l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabGE___closed__3;
 lean_object* l_Lean_Elab_Term_elabMapConst___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -542,7 +544,6 @@ lean_object* l_Lean_Elab_Term_elabIf___lambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_elabCons(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabMod(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAnoymousCtor___closed__3;
-extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__30;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOr___closed__1;
 extern lean_object* l_Lean_Parser_Term_map___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_elabAnoymousCtor___closed__10;
@ -570,7 +571,6 @@ extern lean_object* l_Lean_Parser_Term_bne___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Term_elabDollar(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabIf___lambda__1___closed__3;
 lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__25;
-extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__33;
 extern lean_object* l_Lean_Parser_Term_map___elambda__1___closed__1;
 lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Elab_Term_elabWhere___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabAndThen(lean_object*, lean_object*, lean_object*, lean_object*);
@ -598,7 +598,6 @@ lean_object* l_Lean_Elab_Term_elabSub___boxed(lean_object*, lean_object*, lean_o
 lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__2;
 lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__24;
 lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
-extern lean_object* l___private_Init_Lean_Elab_Quotation_14__toPreterm___main___lambda__3___closed__3;
 extern lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__2;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabNe___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabseqLeft(lean_object*);
@ -616,7 +615,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabLE___closed__2;
 extern lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__2;
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAndM___closed__2;
 lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__22;
-extern lean_object* l___private_Init_Lean_Elab_Quotation_14__toPreterm___main___lambda__1___closed__4;
+extern lean_object* l___private_Init_Lean_Elab_Quotation_15__toPreterm___main___lambda__1___closed__4;
 lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__9;
 lean_object* l_Lean_Elab_Term_elabAnoymousCtor___closed__7;
 lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__33;
@ -1029,7 +1028,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l___private_Init_Lean_Elab_Quotation_14__toPreterm___main___lambda__3___closed__1;
+x_2 = l___private_Init_Lean_Elab_Quotation_15__toPreterm___main___lambda__3___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@ -1217,7 +1216,7 @@ x_20 = lean_ctor_get(x_18, 0);
 x_21 = lean_box(0);
 x_22 = l_Lean_Elab_Term_elabIf___lambda__1___closed__1;
 x_23 = lean_name_mk_numeral(x_22, x_20);
-x_24 = l___private_Init_Lean_Elab_Quotation_14__toPreterm___main___lambda__3___closed__3;
+x_24 = l___private_Init_Lean_Elab_Quotation_15__toPreterm___main___lambda__3___closed__3;
 x_25 = l_Lean_Elab_Term_elabIf___lambda__1___closed__3;
 x_26 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_26, 0, x_21);
@ -1226,7 +1225,7 @@ lean_ctor_set(x_26, 2, x_23);
 lean_ctor_set(x_26, 3, x_25);
 x_27 = l_Array_empty___closed__1;
 x_28 = lean_array_push(x_27, x_26);
-x_29 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_29 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_30 = lean_array_push(x_28, x_29);
 x_31 = l_Lean_Parser_Term_id___elambda__1___closed__2;
 x_32 = lean_alloc_ctor(1, 2, 0);
@ -1262,7 +1261,7 @@ lean_dec(x_18);
 x_45 = lean_box(0);
 x_46 = l_Lean_Elab_Term_elabIf___lambda__1___closed__1;
 x_47 = lean_name_mk_numeral(x_46, x_43);
-x_48 = l___private_Init_Lean_Elab_Quotation_14__toPreterm___main___lambda__3___closed__3;
+x_48 = l___private_Init_Lean_Elab_Quotation_15__toPreterm___main___lambda__3___closed__3;
 x_49 = l_Lean_Elab_Term_elabIf___lambda__1___closed__3;
 x_50 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_50, 0, x_45);
@ -1271,7 +1270,7 @@ lean_ctor_set(x_50, 2, x_47);
 lean_ctor_set(x_50, 3, x_49);
 x_51 = l_Array_empty___closed__1;
 x_52 = lean_array_push(x_51, x_50);
-x_53 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_53 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_54 = lean_array_push(x_52, x_53);
 x_55 = l_Lean_Parser_Term_id___elambda__1___closed__2;
 x_56 = lean_alloc_ctor(1, 2, 0);
@ -1360,7 +1359,7 @@ lean_ctor_set(x_95, 2, x_92);
 lean_ctor_set(x_95, 3, x_94);
 x_96 = l_Array_empty___closed__1;
 x_97 = lean_array_push(x_96, x_95);
-x_98 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_98 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_99 = lean_array_push(x_97, x_98);
 x_100 = l_Lean_Parser_Term_id___elambda__1___closed__2;
 x_101 = lean_alloc_ctor(1, 2, 0);
@ -1392,9 +1391,9 @@ x_117 = lean_array_push(x_116, x_98);
 x_118 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_118, 0, x_69);
 lean_ctor_set(x_118, 1, x_117);
-x_119 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_119 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_120 = lean_array_push(x_119, x_118);
-x_121 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_121 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_122 = lean_array_push(x_120, x_121);
 x_123 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_124 = lean_alloc_ctor(1, 2, 0);
@ -1446,7 +1445,7 @@ lean_ctor_set(x_145, 2, x_142);
 lean_ctor_set(x_145, 3, x_144);
 x_146 = l_Array_empty___closed__1;
 x_147 = lean_array_push(x_146, x_145);
-x_148 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_148 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_149 = lean_array_push(x_147, x_148);
 x_150 = l_Lean_Parser_Term_id___elambda__1___closed__2;
 x_151 = lean_alloc_ctor(1, 2, 0);
@ -1478,9 +1477,9 @@ x_167 = lean_array_push(x_166, x_148);
 x_168 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_168, 0, x_69);
 lean_ctor_set(x_168, 1, x_167);
-x_169 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_169 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_170 = lean_array_push(x_169, x_168);
-x_171 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_171 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_172 = lean_array_push(x_170, x_171);
 x_173 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_174 = lean_alloc_ctor(1, 2, 0);
@ -1675,7 +1674,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Elab_Term_elabSubtype___lambda__1___closed__8;
-x_2 = l___private_Init_Lean_Elab_Quotation_8__explodeHeadPat___lambda__1___closed__3;
+x_2 = l___private_Init_Lean_Elab_Quotation_9__explodeHeadPat___lambda__1___closed__3;
 x_3 = lean_array_push(x_1, x_2);
 return x_3;
 }
@ -1816,7 +1815,7 @@ lean_ctor_set(x_25, 2, x_22);
 lean_ctor_set(x_25, 3, x_24);
 x_26 = l_Array_empty___closed__1;
 x_27 = lean_array_push(x_26, x_25);
-x_28 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_28 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_29 = lean_array_push(x_27, x_28);
 x_30 = l_Lean_Parser_Term_id___elambda__1___closed__2;
 x_31 = lean_alloc_ctor(1, 2, 0);
@ -1830,9 +1829,9 @@ x_36 = l_Lean_nullKind___closed__2;
 x_37 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_37, 0, x_36);
 lean_ctor_set(x_37, 1, x_35);
-x_38 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_38 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_39 = lean_array_push(x_38, x_37);
-x_40 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_40 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_41 = lean_array_push(x_39, x_40);
 x_42 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_43 = lean_alloc_ctor(1, 2, 0);
@ -1889,7 +1888,7 @@ lean_ctor_set(x_69, 2, x_66);
 lean_ctor_set(x_69, 3, x_68);
 x_70 = l_Array_empty___closed__1;
 x_71 = lean_array_push(x_70, x_69);
-x_72 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_72 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_73 = lean_array_push(x_71, x_72);
 x_74 = l_Lean_Parser_Term_id___elambda__1___closed__2;
 x_75 = lean_alloc_ctor(1, 2, 0);
@ -1903,9 +1902,9 @@ x_80 = l_Lean_nullKind___closed__2;
 x_81 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_81, 0, x_80);
 lean_ctor_set(x_81, 1, x_79);
-x_82 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_82 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_83 = lean_array_push(x_82, x_81);
-x_84 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_84 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_85 = lean_array_push(x_83, x_84);
 x_86 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_87 = lean_alloc_ctor(1, 2, 0);
@ -2041,7 +2040,7 @@ lean_ctor_set(x_134, 2, x_131);
 lean_ctor_set(x_134, 3, x_133);
 x_135 = l_Array_empty___closed__1;
 x_136 = lean_array_push(x_135, x_134);
-x_137 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_137 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_138 = lean_array_push(x_136, x_137);
 x_139 = l_Lean_Parser_Term_id___elambda__1___closed__2;
 x_140 = lean_alloc_ctor(1, 2, 0);
@ -2063,9 +2062,9 @@ x_149 = lean_array_push(x_142, x_148);
 x_150 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_150, 0, x_108);
 lean_ctor_set(x_150, 1, x_149);
-x_151 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_151 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_152 = lean_array_push(x_151, x_150);
-x_153 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_153 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_154 = lean_array_push(x_152, x_153);
 x_155 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_156 = lean_alloc_ctor(1, 2, 0);
@ -2122,7 +2121,7 @@ lean_ctor_set(x_182, 2, x_179);
 lean_ctor_set(x_182, 3, x_181);
 x_183 = l_Array_empty___closed__1;
 x_184 = lean_array_push(x_183, x_182);
-x_185 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_185 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_186 = lean_array_push(x_184, x_185);
 x_187 = l_Lean_Parser_Term_id___elambda__1___closed__2;
 x_188 = lean_alloc_ctor(1, 2, 0);
@ -2144,9 +2143,9 @@ x_197 = lean_array_push(x_190, x_196);
 x_198 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_198, 0, x_108);
 lean_ctor_set(x_198, 1, x_197);
-x_199 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_199 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_200 = lean_array_push(x_199, x_198);
-x_201 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_201 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_202 = lean_array_push(x_200, x_201);
 x_203 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_204 = lean_alloc_ctor(1, 2, 0);
@ -2842,9 +2841,9 @@ x_29 = lean_array_push(x_21, x_28);
 x_30 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_30, 0, x_27);
 lean_ctor_set(x_30, 1, x_29);
-x_31 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_31 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_32 = lean_array_push(x_31, x_30);
-x_33 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_33 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_34 = lean_array_push(x_32, x_33);
 x_35 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_36 = lean_alloc_ctor(1, 2, 0);
@ -2907,9 +2906,9 @@ x_67 = lean_array_push(x_59, x_66);
 x_68 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_68, 0, x_65);
 lean_ctor_set(x_68, 1, x_67);
-x_69 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_69 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_70 = lean_array_push(x_69, x_68);
-x_71 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_71 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_72 = lean_array_push(x_70, x_71);
 x_73 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_74 = lean_alloc_ctor(1, 2, 0);
@ -3173,9 +3172,9 @@ x_37 = lean_array_push(x_29, x_36);
 x_38 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_38, 0, x_35);
 lean_ctor_set(x_38, 1, x_37);
-x_39 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_39 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_40 = lean_array_push(x_39, x_38);
-x_41 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_41 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_42 = lean_array_push(x_40, x_41);
 x_43 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_44 = lean_alloc_ctor(1, 2, 0);
@ -3195,7 +3194,7 @@ x_53 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_53, 0, x_52);
 lean_ctor_set(x_53, 1, x_51);
 x_54 = lean_array_push(x_28, x_53);
-x_55 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_55 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_56 = lean_array_push(x_54, x_55);
 x_57 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_57, 0, x_35);
@ -3237,9 +3236,9 @@ x_75 = lean_array_push(x_67, x_74);
 x_76 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_76, 0, x_73);
 lean_ctor_set(x_76, 1, x_75);
-x_77 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_77 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_78 = lean_array_push(x_77, x_76);
-x_79 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_79 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_80 = lean_array_push(x_78, x_79);
 x_81 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_82 = lean_alloc_ctor(1, 2, 0);
@ -3259,7 +3258,7 @@ x_91 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_91, 0, x_90);
 lean_ctor_set(x_91, 1, x_89);
 x_92 = lean_array_push(x_66, x_91);
-x_93 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_93 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_94 = lean_array_push(x_92, x_93);
 x_95 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_95, 0, x_73);
@ -3344,9 +3343,9 @@ x_129 = lean_array_push(x_121, x_128);
 x_130 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_130, 0, x_127);
 lean_ctor_set(x_130, 1, x_129);
-x_131 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_131 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_132 = lean_array_push(x_131, x_130);
-x_133 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_133 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_134 = lean_array_push(x_132, x_133);
 x_135 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_136 = lean_alloc_ctor(1, 2, 0);
@ -3366,7 +3365,7 @@ x_145 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_145, 0, x_144);
 lean_ctor_set(x_145, 1, x_143);
 x_146 = lean_array_push(x_120, x_145);
-x_147 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_147 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_148 = lean_array_push(x_146, x_147);
 x_149 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_149, 0, x_127);
@ -3408,9 +3407,9 @@ x_167 = lean_array_push(x_159, x_166);
 x_168 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_168, 0, x_165);
 lean_ctor_set(x_168, 1, x_167);
-x_169 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_169 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_170 = lean_array_push(x_169, x_168);
-x_171 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_171 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_172 = lean_array_push(x_170, x_171);
 x_173 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_174 = lean_alloc_ctor(1, 2, 0);
@ -3430,7 +3429,7 @@ x_183 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_183, 0, x_182);
 lean_ctor_set(x_183, 1, x_181);
 x_184 = lean_array_push(x_158, x_183);
-x_185 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_185 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_186 = lean_array_push(x_184, x_185);
 x_187 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_187, 0, x_165);
@ -3556,9 +3555,9 @@ x_236 = lean_array_push(x_229, x_235);
 x_237 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_237, 0, x_204);
 lean_ctor_set(x_237, 1, x_236);
-x_238 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_238 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_239 = lean_array_push(x_238, x_237);
-x_240 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_240 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_241 = lean_array_push(x_239, x_240);
 x_242 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_243 = lean_alloc_ctor(1, 2, 0);
@ -3578,7 +3577,7 @@ x_252 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_252, 0, x_251);
 lean_ctor_set(x_252, 1, x_250);
 x_253 = lean_array_push(x_228, x_252);
-x_254 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_254 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_255 = lean_array_push(x_253, x_254);
 x_256 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_256, 0, x_204);
@ -3619,9 +3618,9 @@ x_273 = lean_array_push(x_266, x_272);
 x_274 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_274, 0, x_204);
 lean_ctor_set(x_274, 1, x_273);
-x_275 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_275 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_276 = lean_array_push(x_275, x_274);
-x_277 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_277 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_278 = lean_array_push(x_276, x_277);
 x_279 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_280 = lean_alloc_ctor(1, 2, 0);
@ -3641,7 +3640,7 @@ x_289 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_289, 0, x_288);
 lean_ctor_set(x_289, 1, x_287);
 x_290 = lean_array_push(x_265, x_289);
-x_291 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_291 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_292 = lean_array_push(x_290, x_291);
 x_293 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_293, 0, x_204);
@ -3726,9 +3725,9 @@ x_327 = lean_array_push(x_320, x_326);
 x_328 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_328, 0, x_204);
 lean_ctor_set(x_328, 1, x_327);
-x_329 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_329 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_330 = lean_array_push(x_329, x_328);
-x_331 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_331 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_332 = lean_array_push(x_330, x_331);
 x_333 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_334 = lean_alloc_ctor(1, 2, 0);
@ -3748,7 +3747,7 @@ x_343 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_343, 0, x_342);
 lean_ctor_set(x_343, 1, x_341);
 x_344 = lean_array_push(x_319, x_343);
-x_345 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_345 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_346 = lean_array_push(x_344, x_345);
 x_347 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_347, 0, x_204);
@ -3789,9 +3788,9 @@ x_364 = lean_array_push(x_357, x_363);
 x_365 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_365, 0, x_204);
 lean_ctor_set(x_365, 1, x_364);
-x_366 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_366 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_367 = lean_array_push(x_366, x_365);
-x_368 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_368 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_369 = lean_array_push(x_367, x_368);
 x_370 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_371 = lean_alloc_ctor(1, 2, 0);
@ -3811,7 +3810,7 @@ x_380 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_380, 0, x_379);
 lean_ctor_set(x_380, 1, x_378);
 x_381 = lean_array_push(x_356, x_380);
-x_382 = l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___closed__15;
+x_382 = l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
 x_383 = lean_array_push(x_381, x_382);
 x_384 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_384, 0, x_204);
@ -3923,11 +3922,11 @@ lean_dec(x_15);
 x_17 = l_Lean_Parser_Term_let___elambda__1___closed__1;
 lean_inc(x_2);
 x_18 = lean_name_mk_string(x_2, x_17);
-x_19 = l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___elambda__3___closed__1;
+x_19 = l___private_Init_Lean_Elab_Quotation_8__getHeadInfo___elambda__3___closed__1;
 lean_inc(x_3);
 x_20 = lean_array_push(x_3, x_19);
 x_21 = lean_array_push(x_20, x_14);
-x_22 = l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___elambda__3___closed__10;
+x_22 = l___private_Init_Lean_Elab_Quotation_8__getHeadInfo___elambda__3___closed__10;
 x_23 = lean_array_push(x_21, x_22);
 x_24 = lean_array_push(x_23, x_7);
 x_25 = lean_alloc_ctor(1, 2, 0);
@ -4386,27 +4385,19 @@ return x_3;
 lean_object* _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__29() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("some");
-return x_1;
+lean_object* x_1; lean_object* x_2; 
+x_1 = l___private_Init_Lean_Elab_Quotation_4__quoteOption___rarg___lambda__2___closed__4;
+x_2 = lean_string_utf8_byte_size(x_1);
+return x_2;
 }
 }
 lean_object* _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__30() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__29;
-x_2 = lean_string_utf8_byte_size(x_1);
-return x_2;
-}
-}
-lean_object* _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__31() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__29;
+x_1 = l___private_Init_Lean_Elab_Quotation_4__quoteOption___rarg___lambda__2___closed__4;
 x_2 = lean_unsigned_to_nat(0u);
-x_3 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__30;
+x_3 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__29;
 x_4 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@ -4414,13 +4405,25 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
+lean_object* _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__31() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l___private_Init_Lean_Elab_Quotation_4__quoteOption___rarg___lambda__2___closed__4;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
 lean_object* _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__32() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__29;
-x_3 = lean_name_mk_string(x_1, x_2);
+x_2 = l___private_Init_Lean_Elab_Quotation_4__quoteOption___rarg___lambda__2___closed__6;
+x_3 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_3, 0, x_2);
+lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
@ -4428,30 +4431,8 @@ lean_object* _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__33() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__33;
-x_2 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__29;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__34() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__33;
-x_3 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_3, 0, x_2);
-lean_ctor_set(x_3, 1, x_1);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__35() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = lean_box(0);
-x_2 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__34;
+x_2 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__32;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
@ -4633,10 +4614,10 @@ x_72 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_72, 0, x_44);
 lean_ctor_set(x_72, 1, x_71);
 x_73 = lean_array_push(x_36, x_72);
-x_74 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31;
+x_74 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__31;
 x_75 = lean_name_mk_numeral(x_74, x_52);
-x_76 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__30;
-x_77 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__36;
+x_76 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__30;
+x_77 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__33;
 x_78 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_78, 0, x_21);
 lean_ctor_set(x_78, 1, x_76);
@ -4657,9 +4638,9 @@ x_86 = l_Lean_nullKind___closed__2;
 x_87 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_87, 0, x_86);
 lean_ctor_set(x_87, 1, x_85);
-x_88 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_88 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_89 = lean_array_push(x_88, x_87);
-x_90 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_90 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_91 = lean_array_push(x_89, x_90);
 x_92 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_93 = lean_alloc_ctor(1, 2, 0);
@ -4722,10 +4703,10 @@ x_120 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_120, 0, x_44);
 lean_ctor_set(x_120, 1, x_119);
 x_121 = lean_array_push(x_36, x_120);
-x_122 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31;
+x_122 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__31;
 x_123 = lean_name_mk_numeral(x_122, x_99);
-x_124 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__30;
-x_125 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__36;
+x_124 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__30;
+x_125 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__33;
 x_126 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_126, 0, x_21);
 lean_ctor_set(x_126, 1, x_124);
@ -4746,9 +4727,9 @@ x_134 = l_Lean_nullKind___closed__2;
 x_135 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_135, 0, x_134);
 lean_ctor_set(x_135, 1, x_133);
-x_136 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_136 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_137 = lean_array_push(x_136, x_135);
-x_138 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_138 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_139 = lean_array_push(x_137, x_138);
 x_140 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_141 = lean_alloc_ctor(1, 2, 0);
@ -4816,10 +4797,10 @@ x_170 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_170, 0, x_44);
 lean_ctor_set(x_170, 1, x_169);
 x_171 = lean_array_push(x_36, x_170);
-x_172 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__32;
+x_172 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__31;
 x_173 = lean_name_mk_numeral(x_172, x_150);
-x_174 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__31;
-x_175 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__35;
+x_174 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__30;
+x_175 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__33;
 x_176 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_176, 0, x_21);
 lean_ctor_set(x_176, 1, x_174);
@ -4841,9 +4822,9 @@ x_185 = l_Lean_nullKind___closed__2;
 x_186 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_186, 0, x_185);
 lean_ctor_set(x_186, 1, x_184);
-x_187 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_187 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_188 = lean_array_push(x_187, x_186);
-x_189 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_189 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_190 = lean_array_push(x_188, x_189);
 x_191 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_192 = lean_alloc_ctor(1, 2, 0);
@ -4920,10 +4901,10 @@ x_227 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_227, 0, x_44);
 lean_ctor_set(x_227, 1, x_226);
 x_228 = lean_array_push(x_36, x_227);
-x_229 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__32;
+x_229 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__31;
 x_230 = lean_name_mk_numeral(x_229, x_206);
-x_231 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__31;
-x_232 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__35;
+x_231 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__30;
+x_232 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__33;
 x_233 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_233, 0, x_21);
 lean_ctor_set(x_233, 1, x_231);
@ -4945,9 +4926,9 @@ x_242 = l_Lean_nullKind___closed__2;
 x_243 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_243, 0, x_242);
 lean_ctor_set(x_243, 1, x_241);
-x_244 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
+x_244 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__53;
 x_245 = lean_array_push(x_244, x_243);
-x_246 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
+x_246 = l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__61;
 x_247 = lean_array_push(x_245, x_246);
 x_248 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
 x_249 = lean_alloc_ctor(1, 2, 0);
@ -6525,7 +6506,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l___private_Init_Lean_Elab_Quotation_14__toPreterm___main___lambda__1___closed__4;
+x_2 = l___private_Init_Lean_Elab_Quotation_15__toPreterm___main___lambda__1___closed__4;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@ -8377,10 +8358,6 @@ l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__32 = _init_l_Lean_Elab_Te
 lean_mark_persistent(l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__32);
 l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__33 = _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__33();
 lean_mark_persistent(l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__33);
-l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__34 = _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__34();
-lean_mark_persistent(l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__34);
-l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__35 = _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__35();
-lean_mark_persistent(l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__35);
 l_Lean_Elab_Term_elabParserMacro___closed__1 = _init_l_Lean_Elab_Term_elabParserMacro___closed__1();
 lean_mark_persistent(l_Lean_Elab_Term_elabParserMacro___closed__1);
 l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__1 = _init_l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__1();
--- a/stage0/stdlib/Init/Lean/Elab/Command.c
+++ b/stage0/stdlib/Init/Lean/Elab/Command.c
@ -21,7 +21,6 @@ extern lean_object* l_Lean_Name_toString___closed__1;
 lean_object* l_Lean_Elab_Command_registerBuiltinCommandElabAttr___closed__4;
 lean_object* l_Lean_Elab_Command_elabSection(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabNamespace(lean_object*);
-lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__2;
 lean_object* l_Lean_extractMacroScopes(lean_object*);
 lean_object* l_PersistentHashMap_contains___at_Lean_Elab_Command_addBuiltinCommandElab___spec__4___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_commandElabAttribute___closed__3;
@ -59,7 +58,6 @@ lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSection(lean_object
 lean_object* lean_array_uget(lean_object*, size_t);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabVariable(lean_object*);
 lean_object* lean_io_error_to_string(lean_object*);
-extern lean_object* l_Lean_Syntax_formatStxAux___main___closed__5;
 lean_object* l_Lean_Elab_Term_inferType(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Init_Lean_Elab_Util_7__regTraceClasses___closed__1;
 uint8_t l_Lean_Name_lt___main(lean_object*, lean_object*);
@ -106,7 +104,6 @@ lean_object* l_Lean_Elab_ElabFnTable_insert___rarg(lean_object*, lean_object*, l
 lean_object* l___private_Init_Lean_Elab_Command_8__elabCommandUsing(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_append___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabSetOption(lean_object*, lean_object*, lean_object*);
-lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1;
 lean_object* l_Lean_Elab_logAt___at_Lean_Elab_Command_logTrace___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_name_eq(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_registerBuiltinCommandElabAttr___closed__2;
@ -116,6 +113,7 @@ lean_object* l_Lean_Elab_Command_elabCommandAux___closed__5;
 lean_object* l_Lean_Elab_Command_compileDecl(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabUniverse(lean_object*);
 lean_object* l_Lean_Elab_Command_getCurrMacroScope___boxed(lean_object*, lean_object*);
+uint8_t l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_mkFreshKindAux___main___spec__3(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_reprint___main(lean_object*);
 lean_object* l_Lean_Elab_Command_elabCommandAux___closed__6;
 lean_object* l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Elab_Command_elabOpenSimple___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -145,7 +143,6 @@ lean_object* l_Lean_Elab_Command_setOption(lean_object*, lean_object*, lean_obje
 extern lean_object* l_String_splitAux___main___closed__1;
 lean_object* l_Lean_SMap_empty___at_Lean_Elab_Command_mkBuiltinCommandElabTable___spec__1___closed__2;
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabExport(lean_object*);
-lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2;
 lean_object* l_Lean_Elab_Command_commandElabAttribute___closed__2;
 lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Meta_isLevelDefEqAux___main___closed__5;
@ -162,7 +159,6 @@ extern lean_object* l_Lean_Meta_MetaHasEval___rarg___closed__4;
 extern lean_object* l_Lean_Parser_Command_mixfix___elambda__1___closed__2;
 lean_object* l_Lean_Name_getNumParts___main(lean_object*);
 lean_object* l_Lean_Elab_Command_elabOpen(lean_object*, lean_object*, lean_object*);
-lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__1;
 lean_object* l_Lean_Elab_mkMessageAt___at_Lean_Elab_Command_throwError___spec__3(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabSetOption___closed__3;
 extern lean_object* l_Lean_LocalContext_Inhabited___closed__1;
@ -175,7 +171,6 @@ lean_object* l_Lean_Elab_Command_elabMixfix___boxed(lean_object*, lean_object*);
 extern lean_object* l_Lean_AttributeImpl_inhabited___closed__2;
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabEnd___closed__9;
-lean_object* l_Lean_Elab_Command_elabDeclareSyntaxCat___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_throwUnsupportedSyntax___rarg(lean_object*);
 lean_object* l_IO_ofExcept___at_Lean_registerClassAttr___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_addBuiltinCommandElab(lean_object*, lean_object*, lean_object*, lean_object*);
@ -328,7 +323,6 @@ extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__7;
 lean_object* l_Lean_Elab_Command_elabOpenOnly(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Options_empty;
 extern lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__2;
-lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__3;
 lean_object* l_ReaderT_read___at_Lean_Elab_Command_CommandElabM_monadLog___spec__1(lean_object*, lean_object*);
 uint8_t l_coeDecidableEq(uint8_t);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabExport___closed__1;
@ -346,7 +340,6 @@ lean_object* l_PersistentHashMap_containsAux___main___at_Lean_Elab_Command_addBu
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabVariable___closed__2;
 extern lean_object* l_Lean_Parser_Command_open___elambda__1___closed__2;
 uint8_t l_Array_contains___at_Lean_findField_x3f___main___spec__1(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Command_elabSyntax___closed__3;
 lean_object* l_Lean_Elab_Command_CommandElabM_MonadQuotation___closed__1;
 lean_object* l_Lean_Elab_mkElabAttribute___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabEnd___closed__2;
@ -363,7 +356,6 @@ lean_object* l_PersistentHashMap_empty___at_Lean_Elab_Command_mkBuiltinCommandEl
 lean_object* l_mkHashMapImp___rarg(lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabOpen(lean_object*);
 lean_object* l_Lean_Elab_Command_elabEnd(lean_object*, lean_object*, lean_object*);
-lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax(lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_modifyScope___closed__1;
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabCheck(lean_object*);
@ -404,7 +396,6 @@ lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSynth___closed__1;
 lean_object* l___private_Init_Lean_Elab_Command_2__getState(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Command_universe___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Command_elabCommandAux___closed__2;
-lean_object* l_Lean_Parser_registerParserCategory(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabOpen___closed__2;
 extern lean_object* l_Bool_HasRepr___closed__1;
 lean_object* l_Lean_Meta_synthInstance(lean_object*, lean_object*, lean_object*);
@ -414,7 +405,6 @@ lean_object* l_Lean_Elab_Command_elabExport___closed__2;
 lean_object* l_AssocList_contains___main___at_Lean_Elab_Command_addBuiltinCommandElab___spec__3___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_withDeclId___spec__4(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabReserve(lean_object*, lean_object*);
-lean_object* l_Lean_Name_appendAfter(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Command_end___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_setOption___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_mkCommandElabAttribute___closed__1;
@ -452,21 +442,17 @@ lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Command_withDeclId___spec
 lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___closed__5;
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabUniverse___closed__2;
 lean_object* l___private_Init_Lean_Elab_Command_14__addScopes___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Command_elabSyntax___closed__1;
 lean_object* l_Lean_Elab_Command_withIncRecDepth(lean_object*);
 lean_object* lean_panic_fn(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_registerBuiltinCommandElabAttr___closed__3;
 lean_object* l___private_Init_Lean_Elab_Command_16__checkAnonymousScope___boxed(lean_object*);
 lean_object* l_Lean_Elab_log___at_Lean_Elab_Term_logTrace___spec__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
-uint8_t l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_isValidSyntaxNodeKind___spec__3(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabCheck___closed__2;
-lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat(lean_object*);
 extern lean_object* l_Lean_EnvExtension_setState___closed__1;
 lean_object* l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Elab_Command_elabOpenSimple___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getOptionalIdent_x3f(lean_object*);
 lean_object* l_Array_filterAux___main___at_Lean_Elab_Command_sortDeclLevelParams___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_mkCommandElabAttribute___closed__2;
-lean_object* l_Lean_Elab_Command_elabSyntax___closed__2;
 lean_object* l_Lean_Elab_Command_elabNamespace(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabReserve___rarg(lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabMixfix(lean_object*);
@ -481,7 +467,6 @@ lean_object* l_Lean_Elab_Command_logUnknownDecl___closed__1;
 lean_object* l_Lean_Syntax_getPos(lean_object*);
 lean_object* l_Lean_Elab_Command_State_inhabited;
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabMixfix___closed__2;
-lean_object* l_Lean_Elab_Command_elabSyntax(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabOpenHiding___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_getOpenDecls(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel___rarg___closed__4;
@ -534,11 +519,9 @@ lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabExport___closed__3;
 lean_object* l_Lean_Elab_Command_elabReserve___boxed(lean_object*, lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSynth(lean_object*);
 lean_object* l_Lean_Elab_Command_liftIOCore___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__3;
 lean_object* l_AssocList_find___main___at_Lean_Elab_Command_elabCommandAux___spec__6___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_logUnknownDecl___closed__2;
 lean_object* l_List_foldl___main___at_Lean_addMacroScopes___spec__1(lean_object*, lean_object*);
-extern lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Command_mkCommandElabAttribute(lean_object*);
 lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___closed__10;
 lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_withDeclId___spec__3(lean_object*, lean_object*, lean_object*);
@ -584,7 +567,6 @@ lean_object* l_List_foldlM___main___at___private_Init_Lean_Elab_Command_7__addMa
 lean_object* l_Lean_Elab_Command_mkMessageAux(lean_object*, lean_object*, lean_object*, uint8_t);
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Command_10__mkTermState___boxed(lean_object*);
-extern lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Command_commandElabAttribute___closed__5;
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabNamespace___closed__1;
 lean_object* l_Lean_Elab_Command_CommandElabM_MonadQuotation___closed__3;
@ -596,7 +578,6 @@ lean_object* l___private_Init_Lean_Elab_Command_11__getVarDecls___boxed(lean_obj
 lean_object* l_Lean_Elab_Command_declareBuiltinCommandElab___closed__2;
 extern lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__2;
 lean_object* l_Lean_Elab_syntaxNodeKindOfAttrParam(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Command_elabDeclareSyntaxCat(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_regBuiltinCommandParserAttr___closed__3;
 lean_object* l_HashMapImp_find_x3f___at_Lean_Elab_Command_elabCommandAux___spec__5(lean_object*, lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabNamespace___closed__2;
@ -3365,7 +3346,7 @@ x_17 = lean_ctor_get(x_1, 0);
 lean_inc(x_17);
 lean_dec(x_1);
 x_18 = lean_unsigned_to_nat(0u);
-x_19 = l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_isValidSyntaxNodeKind___spec__3(x_17, x_18, x_3);
+x_19 = l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_mkFreshKindAux___main___spec__3(x_17, x_18, x_3);
 lean_dec(x_17);
 return x_19;
 }
@ -18685,230 +18666,6 @@ x_5 = l_Lean_Elab_Command_addBuiltinCommandElab(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
-lean_object* l_Lean_Elab_Command_elabDeclareSyntaxCat(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; 
-x_4 = lean_unsigned_to_nat(1u);
-x_5 = l_Lean_Syntax_getIdAt(x_1, x_4);
-x_6 = l_Lean_Syntax_formatStxAux___main___closed__5;
-lean_inc(x_5);
-x_7 = l_Lean_Name_appendAfter(x_5, x_6);
-lean_inc(x_2);
-x_8 = l_Lean_Elab_Command_getEnv(x_2, x_3);
-if (lean_obj_tag(x_8) == 0)
-{
-lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; 
-x_9 = lean_ctor_get(x_8, 0);
-lean_inc(x_9);
-x_10 = lean_ctor_get(x_8, 1);
-lean_inc(x_10);
-lean_dec(x_8);
-x_11 = 0;
-x_12 = l_Lean_Parser_registerParserCategory(x_9, x_7, x_5, x_11, x_10);
-if (lean_obj_tag(x_12) == 0)
-{
-lean_object* x_13; lean_object* x_14; lean_object* x_15; 
-x_13 = lean_ctor_get(x_12, 0);
-lean_inc(x_13);
-x_14 = lean_ctor_get(x_12, 1);
-lean_inc(x_14);
-lean_dec(x_12);
-x_15 = l_Lean_Elab_Command_setEnv(x_13, x_2, x_14);
-return x_15;
-}
-else
-{
-uint8_t x_16; 
-x_16 = !lean_is_exclusive(x_12);
-if (x_16 == 0)
-{
-lean_object* x_17; lean_object* x_18; lean_object* x_19; 
-x_17 = lean_ctor_get(x_12, 0);
-x_18 = l___private_Init_Lean_Elab_Command_1__ioErrorToMessage(x_2, x_1, x_17);
-x_19 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_19, 0, x_18);
-lean_ctor_set(x_12, 0, x_19);
-return x_12;
-}
-else
-{
-lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; 
-x_20 = lean_ctor_get(x_12, 0);
-x_21 = lean_ctor_get(x_12, 1);
-lean_inc(x_21);
-lean_inc(x_20);
-lean_dec(x_12);
-x_22 = l___private_Init_Lean_Elab_Command_1__ioErrorToMessage(x_2, x_1, x_20);
-x_23 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_23, 0, x_22);
-x_24 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_24, 0, x_23);
-lean_ctor_set(x_24, 1, x_21);
-return x_24;
-}
-}
-}
-else
-{
-uint8_t x_25; 
-lean_dec(x_7);
-lean_dec(x_5);
-lean_dec(x_2);
-x_25 = !lean_is_exclusive(x_8);
-if (x_25 == 0)
-{
-return x_8;
-}
-else
-{
-lean_object* x_26; lean_object* x_27; lean_object* x_28; 
-x_26 = lean_ctor_get(x_8, 0);
-x_27 = lean_ctor_get(x_8, 1);
-lean_inc(x_27);
-lean_inc(x_26);
-lean_dec(x_8);
-x_28 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_28, 0, x_26);
-lean_ctor_set(x_28, 1, x_27);
-return x_28;
-}
-}
-}
-}
-lean_object* l_Lean_Elab_Command_elabDeclareSyntaxCat___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-lean_object* x_4; 
-x_4 = l_Lean_Elab_Command_elabDeclareSyntaxCat(x_1, x_2, x_3);
-lean_dec(x_1);
-return x_4;
-}
-}
-lean_object* _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string("elabDeclareSyntaxCat");
-return x_1;
-}
-}
-lean_object* _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Elab_Command_declareBuiltinCommandElab___closed__3;
-x_2 = l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__3() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabDeclareSyntaxCat___boxed), 3, 0);
-return x_1;
-}
-}
-lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
-x_2 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
-x_3 = l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2;
-x_4 = l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__3;
-x_5 = l_Lean_Elab_Command_addBuiltinCommandElab(x_2, x_3, x_4, x_1);
-return x_5;
-}
-}
-lean_object* _init_l_Lean_Elab_Command_elabSyntax___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string("not implemented yet ");
-return x_1;
-}
-}
-lean_object* _init_l_Lean_Elab_Command_elabSyntax___closed__2() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Elab_Command_elabSyntax___closed__1;
-x_2 = lean_alloc_ctor(2, 1, 0);
-lean_ctor_set(x_2, 0, x_1);
-return x_2;
-}
-}
-lean_object* _init_l_Lean_Elab_Command_elabSyntax___closed__3() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Elab_Command_elabSyntax___closed__2;
-x_2 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_2, 0, x_1);
-return x_2;
-}
-}
-lean_object* l_Lean_Elab_Command_elabSyntax(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_13; 
-x_4 = lean_box(0);
-x_5 = lean_unsigned_to_nat(0u);
-lean_inc(x_1);
-x_6 = l_Lean_Syntax_formatStxAux___main(x_4, x_5, x_1);
-x_7 = l_Lean_Options_empty;
-x_8 = l_Lean_Format_pretty(x_6, x_7);
-x_9 = lean_alloc_ctor(2, 1, 0);
-lean_ctor_set(x_9, 0, x_8);
-x_10 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_10, 0, x_9);
-x_11 = l_Lean_Elab_Command_elabSyntax___closed__3;
-x_12 = lean_alloc_ctor(8, 2, 0);
-lean_ctor_set(x_12, 0, x_11);
-lean_ctor_set(x_12, 1, x_10);
-x_13 = l_Lean_Elab_Command_throwError___rarg(x_1, x_12, x_2, x_3);
-return x_13;
-}
-}
-lean_object* _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string("elabSyntax");
-return x_1;
-}
-}
-lean_object* _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__2() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Elab_Command_declareBuiltinCommandElab___closed__3;
-x_2 = l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__1;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__3() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabSyntax), 3, 0);
-return x_1;
-}
-}
-lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
-x_2 = l_Lean_Parser_Command_syntax___elambda__1___closed__1;
-x_3 = l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__2;
-x_4 = l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__3;
-x_5 = l_Lean_Elab_Command_addBuiltinCommandElab(x_2, x_3, x_4, x_1);
-return x_5;
-}
-}
 lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_withDeclId___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@ -22701,30 +22458,6 @@ lean_mark_persistent(l___regBuiltinCommandElab_Lean_Elab_Command_elabSetOption__
 res = l___regBuiltinCommandElab_Lean_Elab_Command_elabSetOption(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1 = _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1();
-lean_mark_persistent(l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1);
-l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2 = _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2();
-lean_mark_persistent(l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__2);
-l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__3 = _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__3();
-lean_mark_persistent(l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__3);
-res = l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat(lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-l_Lean_Elab_Command_elabSyntax___closed__1 = _init_l_Lean_Elab_Command_elabSyntax___closed__1();
-lean_mark_persistent(l_Lean_Elab_Command_elabSyntax___closed__1);
-l_Lean_Elab_Command_elabSyntax___closed__2 = _init_l_Lean_Elab_Command_elabSyntax___closed__2();
-lean_mark_persistent(l_Lean_Elab_Command_elabSyntax___closed__2);
-l_Lean_Elab_Command_elabSyntax___closed__3 = _init_l_Lean_Elab_Command_elabSyntax___closed__3();
-lean_mark_persistent(l_Lean_Elab_Command_elabSyntax___closed__3);
-l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__1 = _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__1();
-lean_mark_persistent(l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__1);
-l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__2 = _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__2();
-lean_mark_persistent(l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__2);
-l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__3 = _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__3();
-lean_mark_persistent(l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__3);
-res = l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax(lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
 l_Lean_Elab_Command_withDeclId___closed__1 = _init_l_Lean_Elab_Command_withDeclId___closed__1();
 lean_mark_persistent(l_Lean_Elab_Command_withDeclId___closed__1);
 l_Lean_Elab_Command_withDeclId___closed__2 = _init_l_Lean_Elab_Command_withDeclId___closed__2();
--- a/stage0/stdlib/Init/Lean/Elab/Quotation.c
+++ b/stage0/stdlib/Init/Lean/Elab/Quotation.c
--- a/stage0/stdlib/Init/Lean/Elab/Syntax.c
+++ b/stage0/stdlib/Init/Lean/Elab/Syntax.c
--- a/stage0/stdlib/Init/Lean/Elab/Term.c
+++ b/stage0/stdlib/Init/Lean/Elab/Term.c
@ -150,6 +150,7 @@ lean_object* l_Lean_Elab_Term_withoutPostponing(lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__13;
 lean_object* l_Lean_Elab_Term_decLevel(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_8__expandCDot___closed__2;
+uint8_t l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_mkFreshKindAux___main___spec__3(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_reprint___main(lean_object*);
 lean_object* l_Lean_Elab_Term_elabParen___closed__3;
 lean_object* lean_local_ctx_find_from_user_name(lean_object*, lean_object*);
@ -610,7 +611,6 @@ lean_object* l_Lean_Elab_Term_decLevel_x3f___boxed(lean_object*, lean_object*, l
 lean_object* l_Lean_Elab_Term_ensureType___closed__1;
 lean_object* l_Lean_Elab_log___at_Lean_Elab_Term_logTrace___spec__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_getPos___at_Lean_Elab_Term_throwError___spec__2(lean_object*, lean_object*, lean_object*);
-uint8_t l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_isValidSyntaxNodeKind___spec__3(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_expandCDot_x3f___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Term_21__mkPairsAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabTerm___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -2856,7 +2856,7 @@ x_17 = lean_ctor_get(x_1, 0);
 lean_inc(x_17);
 lean_dec(x_1);
 x_18 = lean_unsigned_to_nat(0u);
-x_19 = l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_isValidSyntaxNodeKind___spec__3(x_17, x_18, x_3);
+x_19 = l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_mkFreshKindAux___main___spec__3(x_17, x_18, x_3);
 lean_dec(x_17);
 return x_19;
 }
--- a/stage0/stdlib/Init/Lean/Parser/Level.c
+++ b/stage0/stdlib/Init/Lean/Parser/Level.c
@ -45,7 +45,6 @@ lean_object* l_Lean_Parser_Level_max___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Level_num___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Level_max___closed__7;
 lean_object* l_Lean_Parser_regBuiltinLevelParserAttr___closed__4;
-lean_object* l_Lean_Parser_registerBuiltinDynamicParserAttribute(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_paren___closed__7;
 lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Level_hole___elambda__1(lean_object*, lean_object*, lean_object*);
@ -90,7 +89,6 @@ lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Level_max___closed__6;
 lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Level_imax;
-lean_object* l_Lean_Parser_regLevelParserAttribute___closed__1;
 extern lean_object* l_Char_HasRepr___closed__1;
 lean_object* l_Lean_Parser_Level_hole;
 extern lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__5;
@ -99,8 +97,6 @@ lean_object* l_Lean_Parser_levelParser(uint8_t, lean_object*);
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Level_max___elambda__1___spec__1(uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_num___elambda__1___closed__3;
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
-lean_object* l_Lean_Parser_regLevelParserAttribute___closed__2;
-lean_object* l_Lean_Parser_regLevelParserAttribute(lean_object*);
 lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__11;
 lean_object* l_Lean_Parser_Level_imax___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_ident___closed__1;
@ -228,34 +224,6 @@ x_5 = l_Lean_Parser_registerBuiltinParserAttribute(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
-lean_object* _init_l_Lean_Parser_regLevelParserAttribute___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string("levelParser");
-return x_1;
-}
-}
-lean_object* _init_l_Lean_Parser_regLevelParserAttribute___closed__2() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = lean_box(0);
-x_2 = l_Lean_Parser_regLevelParserAttribute___closed__1;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-lean_object* l_Lean_Parser_regLevelParserAttribute(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_2 = l_Lean_Parser_regLevelParserAttribute___closed__2;
-x_3 = l_Lean_Parser_regBuiltinLevelParserAttr___closed__4;
-x_4 = l_Lean_Parser_registerBuiltinDynamicParserAttribute(x_2, x_3, x_1);
-return x_4;
-}
-}
 lean_object* l_Lean_Parser_levelParser(uint8_t x_1, lean_object* x_2) {
 _start:
 {
@ -2331,13 +2299,6 @@ lean_mark_persistent(l_Lean_Parser_regBuiltinLevelParserAttr___closed__4);
 res = l_Lean_Parser_regBuiltinLevelParserAttr(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-l_Lean_Parser_regLevelParserAttribute___closed__1 = _init_l_Lean_Parser_regLevelParserAttribute___closed__1();
-lean_mark_persistent(l_Lean_Parser_regLevelParserAttribute___closed__1);
-l_Lean_Parser_regLevelParserAttribute___closed__2 = _init_l_Lean_Parser_regLevelParserAttribute___closed__2();
-lean_mark_persistent(l_Lean_Parser_regLevelParserAttribute___closed__2);
-res = l_Lean_Parser_regLevelParserAttribute(lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
 l_Lean_Parser_Level_paren___elambda__1___closed__1 = _init_l_Lean_Parser_Level_paren___elambda__1___closed__1();
 lean_mark_persistent(l_Lean_Parser_Level_paren___elambda__1___closed__1);
 l_Lean_Parser_Level_paren___elambda__1___closed__2 = _init_l_Lean_Parser_Level_paren___elambda__1___closed__2();
--- a/stage0/stdlib/Init/Lean/Parser/Parser.c
+++ b/stage0/stdlib/Init/Lean/Parser/Parser.c
--- a/stage0/stdlib/Init/Lean/Parser/Syntax.c
+++ b/stage0/stdlib/Init/Lean/Parser/Syntax.c
--- a/stage0/stdlib/Init/Lean/Parser/Tactic.c
+++ b/stage0/stdlib/Init/Lean/Parser/Tactic.c
@ -13,10 +13,10 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+lean_object* l_Lean_Parser_Tactic_orelse___closed__4;
 lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__4;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_intro(lean_object*);
-extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Tactic_orelse___closed__2;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__15;
 lean_object* l_Lean_Parser_Tactic_intros___closed__7;
@ -42,6 +42,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Tactic_nestedTacticBlock(lean_obje
 lean_object* l_Lean_Parser_Tactic_assumption___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__4;
 extern lean_object* l_Lean_Parser_Term_have___closed__3;
+lean_object* l_Lean_Parser_ParserState_pushSyntax(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly;
 extern lean_object* l_Lean_Parser_Term_subtype___closed__1;
 lean_object* l_Lean_Parser_tacticSeq___closed__2;
@ -49,6 +50,7 @@ lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_o
 lean_object* l_Lean_Parser_Tactic_apply___closed__4;
 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_registerBuiltinDynamicParserAttribute(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_regBuiltinTacticParserAttr(lean_object*);
@ -68,6 +70,7 @@ lean_object* l_Lean_Parser_Tactic_orelse___closed__3;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__5;
 lean_object* l_Lean_Parser_ParserState_mkErrorsAt(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Tactic_orelse___closed__5;
 lean_object* l_Lean_Parser_symbolFn___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_intros___closed__3;
 lean_object* l_Lean_Parser_Tactic_apply___closed__5;
@ -78,12 +81,14 @@ lean_object* l_Lean_Parser_regBuiltinTacticParserAttr___closed__2;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__13;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__11;
 lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__1;
+lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Tactic_assumption;
 lean_object* l_Lean_Parser_Tactic_intros___elambda__1(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Tactic_assumption___elambda__1___closed__4;
 lean_object* l_Lean_Parser_manyAux___main(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
+extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__3;
 lean_object* l_Lean_Parser_tacticSeq___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_nonReservedSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___closed__1;
@ -137,6 +142,7 @@ lean_object* l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache_
 lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__1;
 extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__9;
+lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Tactic_orelse;
 lean_object* l_Lean_Parser_categoryParserFn(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_tacticSeq(uint8_t);
@ -154,6 +160,7 @@ lean_object* l_Lean_Parser_regTacticParserAttribute(lean_object*);
 lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__6;
 lean_object* l_Lean_Parser_sepBy1Fn(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Parser_epsilonInfo;
 lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___closed__4;
 lean_object* l_Lean_Parser_Tactic_assumption___closed__3;
@ -187,12 +194,15 @@ lean_object* l_Lean_Parser_Tactic_intro___closed__3;
 lean_object* l_Lean_Parser_regBuiltinTacticParserAttr___closed__4;
 lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__4;
+lean_object* l_Lean_Parser_Tactic_orelse___closed__6;
 lean_object* l_Lean_Parser_Tactic_intro___closed__5;
 lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__7;
+lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Tactic_assumption___elambda__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__5;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_orelse(lean_object*);
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_categoryParser___elambda__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -2272,49 +2282,210 @@ x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
+lean_object* _init_l_Lean_Parser_Tactic_orelse___elambda__1___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Parser_Term_orelse___elambda__1___closed__3;
+x_2 = l_String_trim(x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_orelse___elambda__1___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Char_HasRepr___closed__1;
+x_2 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__2;
+x_3 = lean_string_append(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_orelse___elambda__1___closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__3;
+x_2 = l_Char_HasRepr___closed__1;
+x_3 = lean_string_append(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_orelse___elambda__1___closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__4;
+x_3 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_3, 0, x_2);
+lean_ctor_set(x_3, 1, x_1);
+return x_3;
+}
+}
 lean_object* l_Lean_Parser_Tactic_orelse___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; 
-x_4 = l_Lean_Parser_Term_orelse___elambda__1___closed__4;
-x_5 = lean_ctor_get(x_4, 1);
-lean_inc(x_5);
-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_apply_3(x_5, x_1, x_2, x_3);
-x_9 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
-x_10 = l_Lean_Parser_ParserState_mkNode(x_8, x_9, x_7);
-return x_10;
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_4 = lean_ctor_get(x_3, 0);
+lean_inc(x_4);
+x_5 = lean_array_get_size(x_4);
+lean_dec(x_4);
+lean_inc(x_3);
+x_6 = l_Lean_Parser_ParserState_pushSyntax(x_3, x_1);
+x_7 = lean_ctor_get(x_3, 3);
+lean_inc(x_7);
+if (lean_obj_tag(x_7) == 0)
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; 
+x_8 = lean_ctor_get(x_3, 1);
+lean_inc(x_8);
+lean_dec(x_3);
+lean_inc(x_2);
+x_9 = l_Lean_Parser_tokenFn(x_2, x_6);
+x_10 = lean_ctor_get(x_9, 3);
+lean_inc(x_10);
+if (lean_obj_tag(x_10) == 0)
+{
+lean_object* x_11; lean_object* x_12; 
+x_11 = lean_ctor_get(x_9, 0);
+lean_inc(x_11);
+x_12 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_11);
+lean_dec(x_11);
+if (lean_obj_tag(x_12) == 2)
+{
+lean_object* x_13; lean_object* x_14; uint8_t x_15; 
+x_13 = lean_ctor_get(x_12, 1);
+lean_inc(x_13);
+lean_dec(x_12);
+x_14 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__2;
+x_15 = lean_string_dec_eq(x_13, x_14);
+lean_dec(x_13);
+if (x_15 == 0)
+{
+lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+lean_dec(x_2);
+x_16 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__5;
+x_17 = l_Lean_Parser_ParserState_mkErrorsAt(x_9, x_16, x_8);
+x_18 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
+x_19 = l_Lean_Parser_ParserState_mkNode(x_17, x_18, x_5);
+return x_19;
+}
+else
+{
+lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+lean_dec(x_8);
+x_20 = l_Lean_Parser_regBuiltinTacticParserAttr___closed__4;
+x_21 = lean_unsigned_to_nat(1u);
+x_22 = l_Lean_Parser_categoryParserFn(x_20, x_21, x_2, x_9);
+x_23 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
+x_24 = l_Lean_Parser_ParserState_mkNode(x_22, x_23, x_5);
+return x_24;
+}
+}
+else
+{
+lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+lean_dec(x_12);
+lean_dec(x_2);
+x_25 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__5;
+x_26 = l_Lean_Parser_ParserState_mkErrorsAt(x_9, x_25, x_8);
+x_27 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
+x_28 = l_Lean_Parser_ParserState_mkNode(x_26, x_27, x_5);
+return x_28;
+}
+}
+else
+{
+lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; 
+lean_dec(x_10);
+lean_dec(x_2);
+x_29 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__5;
+x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_9, x_29, x_8);
+x_31 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
+x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_5);
+return x_32;
+}
+}
+else
+{
+lean_object* x_33; lean_object* x_34; 
+lean_dec(x_7);
+lean_dec(x_3);
+lean_dec(x_2);
+x_33 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
+x_34 = l_Lean_Parser_ParserState_mkNode(x_6, x_33, x_5);
+return x_34;
+}
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__1() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Parser_Term_orelse___elambda__1___closed__4;
-x_2 = lean_ctor_get(x_1, 0);
-lean_inc(x_2);
-x_3 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
-x_4 = l_Lean_Parser_nodeInfo(x_3, x_2);
-return x_4;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__2;
+x_3 = l_Lean_Parser_symbolInfo(x_2, x_1);
+return x_3;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__2() {
 _start:
 {
+uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = 1;
+x_2 = l_Lean_Parser_regBuiltinTacticParserAttr___closed__4;
+x_3 = lean_unsigned_to_nat(1u);
+x_4 = l_Lean_Parser_categoryParser(x_1, x_2, x_3);
+return x_4;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_Parser_Tactic_orelse___closed__2;
+x_2 = lean_ctor_get(x_1, 0);
+lean_inc(x_2);
+x_3 = l_Lean_Parser_Tactic_orelse___closed__1;
+x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
+return x_4;
+}
+}
+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___closed__1;
+x_2 = l_Lean_Parser_Tactic_orelse___closed__4;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__6() {
+_start:
+{
 lean_object* x_1; 
 x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_orelse___elambda__1), 3, 0);
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__3() {
+lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_orelse___closed__1;
-x_2 = l_Lean_Parser_Tactic_orelse___closed__2;
+x_1 = l_Lean_Parser_Tactic_orelse___closed__5;
+x_2 = l_Lean_Parser_Tactic_orelse___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);
@ -2325,7 +2496,7 @@ lean_object* _init_l_Lean_Parser_Tactic_orelse() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Tactic_orelse___closed__3;
+x_1 = l_Lean_Parser_Tactic_orelse___closed__7;
 return x_1;
 }
 }
@ -2938,12 +3109,28 @@ if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 l_Lean_Parser_Tactic_orelse___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_orelse___elambda__1___closed__1();
 lean_mark_persistent(l_Lean_Parser_Tactic_orelse___elambda__1___closed__1);
+l_Lean_Parser_Tactic_orelse___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_orelse___elambda__1___closed__2();
+lean_mark_persistent(l_Lean_Parser_Tactic_orelse___elambda__1___closed__2);
+l_Lean_Parser_Tactic_orelse___elambda__1___closed__3 = _init_l_Lean_Parser_Tactic_orelse___elambda__1___closed__3();
+lean_mark_persistent(l_Lean_Parser_Tactic_orelse___elambda__1___closed__3);
+l_Lean_Parser_Tactic_orelse___elambda__1___closed__4 = _init_l_Lean_Parser_Tactic_orelse___elambda__1___closed__4();
+lean_mark_persistent(l_Lean_Parser_Tactic_orelse___elambda__1___closed__4);
+l_Lean_Parser_Tactic_orelse___elambda__1___closed__5 = _init_l_Lean_Parser_Tactic_orelse___elambda__1___closed__5();
+lean_mark_persistent(l_Lean_Parser_Tactic_orelse___elambda__1___closed__5);
 l_Lean_Parser_Tactic_orelse___closed__1 = _init_l_Lean_Parser_Tactic_orelse___closed__1();
 lean_mark_persistent(l_Lean_Parser_Tactic_orelse___closed__1);
 l_Lean_Parser_Tactic_orelse___closed__2 = _init_l_Lean_Parser_Tactic_orelse___closed__2();
 lean_mark_persistent(l_Lean_Parser_Tactic_orelse___closed__2);
 l_Lean_Parser_Tactic_orelse___closed__3 = _init_l_Lean_Parser_Tactic_orelse___closed__3();
 lean_mark_persistent(l_Lean_Parser_Tactic_orelse___closed__3);
+l_Lean_Parser_Tactic_orelse___closed__4 = _init_l_Lean_Parser_Tactic_orelse___closed__4();
+lean_mark_persistent(l_Lean_Parser_Tactic_orelse___closed__4);
+l_Lean_Parser_Tactic_orelse___closed__5 = _init_l_Lean_Parser_Tactic_orelse___closed__5();
+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());
--- a/stage0/stdlib/Init/Lean/Parser/Term.c
+++ b/stage0/stdlib/Init/Lean/Parser/Term.c
@ -35,6 +35,7 @@ lean_object* l_Lean_Parser_Term_letIdDecl;
 lean_object* l_Lean_Parser_Term_heq___elambda__1___closed__4;
 extern lean_object* l_Lean_Parser_charLit___closed__1;
 lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___closed__5;
+lean_object* l_Lean_Parser_Term_infixL___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinParser_Lean_Parser_Term_iff(lean_object*);
 lean_object* l_Lean_mkAppStx(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___elambda__1___spec__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
@ -129,7 +130,6 @@ lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___closed__6;
 extern lean_object* l_Lean_Parser_Level_paren___closed__2;
 lean_object* l_Lean_Parser_Term_inaccessible___closed__1;
 lean_object* l_Lean_Parser_Term_not___closed__6;
-lean_object* l_Lean_Parser_unicodeInfixR(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__12;
 lean_object* l_Lean_Parser_Term_lt___elambda__1___closed__4;
@ -520,6 +520,7 @@ lean_object* l_Lean_Parser_Term_where___closed__4;
 lean_object* l_Lean_Parser_Term_prod___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_paren___closed__5;
 lean_object* l_Lean_Parser_Term_letPatDecl___elambda__1___closed__4;
+lean_object* l_Lean_Parser_Term_infixR___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_div___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_sort___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_arrayLit___closed__6;
@ -584,6 +585,7 @@ lean_object* l_Lean_Parser_Term_fun___closed__6;
 lean_object* l_Lean_Parser_Term_num___closed__2;
 lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Term_binderDefault;
+lean_object* l_Lean_Parser_unicodeSymbolFn___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Term_uminus___elambda__1___closed__1;
@ -687,7 +689,6 @@ lean_object* l_Lean_Parser_Term_structInst___closed__4;
 lean_object* l_Lean_Parser_Term_num___closed__4;
 lean_object* l_Lean_Parser_dollarSymbol(uint8_t);
 lean_object* l_Lean_Parser_Term_suffices___elambda__1(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Parser_infixR(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_fromTerm___closed__2;
 lean_object* l_Lean_Parser_Term_id___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_type___elambda__1___closed__5;
@ -1095,6 +1096,7 @@ lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_
 lean_object* l_Lean_Parser_Term_id___closed__3;
 lean_object* l_Lean_Parser_Term_let___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_sortApp___elambda__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Term_unicodeInfixL(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_hole___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Term_structInstSource___closed__6;
 lean_object* l_Lean_Parser_Term_namedArgument___closed__2;
@ -1242,6 +1244,7 @@ lean_object* l_Lean_Parser_Term_match__syntax___closed__1;
 lean_object* l_Lean_Parser_Term_instBinder___closed__2;
 extern lean_object* l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
 lean_object* l_Lean_Parser_Term_letDecl___closed__1;
+lean_object* l_Lean_Parser_Term_unicodeInfixL___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_doSeq___closed__5;
 lean_object* l_Lean_Parser_Term_emptyC___closed__4;
 lean_object* l_Lean_Parser_Term_band___closed__3;
@ -1279,6 +1282,7 @@ lean_object* l_Lean_Parser_Term_le___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_eq___closed__2;
 lean_object* l_Lean_Parser_Term_binderIdent;
 lean_object* l_Lean_Parser_Term_simpleBinder___elambda__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Term_infixR(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_seqLeft___closed__3;
 lean_object* l_Lean_Parser_Term_implicitBinder___elambda__1___closed__2;
 lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__4;
@ -1296,6 +1300,7 @@ lean_object* l_Lean_Parser_Term_have___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Term_namedPattern___closed__4;
 lean_object* l_Lean_Parser_Term_seq___elambda__1___closed__3;
+lean_object* l_Lean_Parser_Term_infixL___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_binderTactic___closed__2;
 lean_object* l_Lean_Parser_Term_if___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Term_div___closed__1;
@ -1397,6 +1402,7 @@ lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__12;
 lean_object* l_Lean_Syntax_isTermId_x3f(lean_object*);
 lean_object* l_Lean_Parser_Term_let___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Term_type___elambda__1___closed__4;
+lean_object* l_Lean_Parser_Term_infixL(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_anonymousCtor;
 lean_object* l_Lean_Parser_Term_dollarProj___closed__4;
 lean_object* l_Lean_Parser_Term_iff___closed__3;
@ -1434,7 +1440,6 @@ lean_object* l_Lean_Parser_Term_structInstSource___closed__1;
 lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Term_depArrow___closed__6;
 lean_object* l_Lean_Parser_Term_mapConst___elambda__1___closed__3;
-lean_object* l_Lean_Parser_unicodeInfixL(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_namedPattern___closed__1;
 lean_object* l_Lean_Parser_Term_doId___closed__7;
 lean_object* l_Lean_Parser_Term_explicitBinder___closed__2;
@ -1644,6 +1649,7 @@ lean_object* l_Lean_Parser_Term_fcomp___closed__3;
 lean_object* l_Lean_Parser_Term_doLet___closed__2;
 lean_object* l_Lean_Parser_Term_type___closed__5;
 lean_object* l_Lean_Parser_Term_match___elambda__1___closed__10;
+lean_object* l_Lean_Parser_Term_unicodeInfixR___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_andthen___closed__1;
 lean_object* l_Lean_Parser_Term_and___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___closed__6;
@ -1714,6 +1720,7 @@ lean_object* l_Lean_Parser_Term_dollarProj;
 lean_object* l_Lean_Parser_Term_dollarProj___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_proj___closed__6;
 lean_object* l_Lean_Parser_Term_type___closed__4;
+lean_object* l_Lean_Parser_Term_infixR___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_beq___closed__2;
 lean_object* l_Lean_Parser_Term_arrayLit___closed__2;
 lean_object* l_Lean_Parser_Term_ne___elambda__1___closed__4;
@ -1816,6 +1823,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_or(lean_object*);
 lean_object* l_Lean_Parser_Term_iff___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_antiquot___closed__1;
 lean_object* l_Lean_Parser_Term_doPat___closed__5;
+lean_object* l_Lean_Parser_categoryParser___elambda__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__4;
 lean_object* l_Lean_Parser_numLitFn___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_binderDefault___closed__3;
@ -1830,7 +1838,6 @@ lean_object* l_Lean_Parser_Term_bindOp___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_do___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_letDecl___closed__3;
 lean_object* l_Lean_Parser_Term_subtype___elambda__1___closed__3;
-lean_object* l_Lean_Parser_infixL(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_if___closed__7;
 lean_object* l_Lean_Parser_Term_match___closed__10;
 lean_object* l_Lean_Parser_Term_modN___elambda__1___closed__2;
@ -1861,8 +1868,10 @@ lean_object* l_Lean_Parser_Term_doExpr___closed__3;
 lean_object* l_Lean_Parser_Term_binderTactic___closed__3;
 lean_object* l_Lean_Parser_Term_doId___closed__6;
 lean_object* l_Lean_Parser_Term_leftArrow___elambda__1(lean_object*);
+lean_object* l_Lean_Parser_Term_unicodeInfixR___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__2;
+lean_object* l_Lean_Parser_Term_unicodeInfixL___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_subtype___closed__11;
 lean_object* l_Lean_Parser_unicodeSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_where___closed__10;
@ -1881,6 +1890,7 @@ lean_object* l_Lean_Parser_Term_bnot___elambda__1(lean_object*, lean_object*, le
 lean_object* l_Lean_Parser_Term_let;
 lean_object* l_Lean_Parser_Term_depArrow___closed__3;
 lean_object* l_Lean_Parser_Term_map;
+lean_object* l_Lean_Parser_Term_unicodeInfixR(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Term_forall___closed__6;
 lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__2;
@ -1918,6 +1928,304 @@ lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Term_letIdDecl___closed__6;
 lean_object* l_Lean_Parser_Term_app___closed__4;
 extern lean_object* l_Lean_Parser_mkAntiquot___closed__1;
+lean_object* l_Lean_Parser_Term_unicodeInfixR___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; 
+lean_inc(x_2);
+lean_inc(x_4);
+x_5 = l_Lean_Parser_ParserState_pushSyntax(x_4, x_2);
+x_6 = lean_ctor_get(x_4, 3);
+lean_inc(x_6);
+lean_dec(x_4);
+if (lean_obj_tag(x_6) == 0)
+{
+lean_object* x_7; 
+x_7 = lean_apply_3(x_1, x_2, x_3, x_5);
+return x_7;
+}
+else
+{
+lean_dec(x_6);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_5;
+}
+}
+}
+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_inc(x_3);
+x_4 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_4, 0, x_3);
+x_5 = l_String_trim(x_1);
+x_6 = l_String_trim(x_2);
+lean_inc(x_6);
+lean_inc(x_5);
+x_7 = l_Lean_Parser_unicodeSymbolInfo(x_5, x_6, x_4);
+x_8 = lean_alloc_closure((void*)(l_Lean_Parser_unicodeSymbolFn___rarg___boxed), 5, 2);
+lean_closure_set(x_8, 0, x_5);
+lean_closure_set(x_8, 1, x_6);
+x_9 = lean_unsigned_to_nat(1u);
+x_10 = lean_nat_sub(x_3, x_9);
+lean_dec(x_3);
+x_11 = 1;
+x_12 = l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
+lean_inc(x_10);
+x_13 = l_Lean_Parser_categoryParser(x_11, x_12, x_10);
+x_14 = lean_ctor_get(x_13, 0);
+lean_inc(x_14);
+lean_dec(x_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);
+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;
+}
+}
+lean_object* l_Lean_Parser_Term_unicodeInfixR___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_Parser_Term_unicodeInfixR(x_1, x_2, x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_4;
+}
+}
+lean_object* l_Lean_Parser_Term_infixR___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; 
+lean_inc(x_2);
+lean_inc(x_4);
+x_5 = l_Lean_Parser_ParserState_pushSyntax(x_4, x_2);
+x_6 = lean_ctor_get(x_4, 3);
+lean_inc(x_6);
+lean_dec(x_4);
+if (lean_obj_tag(x_6) == 0)
+{
+lean_object* x_7; 
+x_7 = lean_apply_3(x_1, x_2, x_3, x_5);
+return x_7;
+}
+else
+{
+lean_dec(x_6);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_5;
+}
+}
+}
+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_inc(x_2);
+x_3 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_3, 0, x_2);
+x_4 = l_String_trim(x_1);
+lean_inc(x_4);
+x_5 = l_Lean_Parser_symbolInfo(x_4, x_3);
+x_6 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
+lean_closure_set(x_6, 0, x_4);
+x_7 = lean_unsigned_to_nat(1u);
+x_8 = lean_nat_sub(x_2, x_7);
+lean_dec(x_2);
+x_9 = 1;
+x_10 = l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
+lean_inc(x_8);
+x_11 = l_Lean_Parser_categoryParser(x_9, x_10, x_8);
+x_12 = lean_ctor_get(x_11, 0);
+lean_inc(x_12);
+lean_dec(x_11);
+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);
+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;
+}
+}
+lean_object* l_Lean_Parser_Term_infixR___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
+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) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; 
+lean_inc(x_2);
+lean_inc(x_4);
+x_5 = l_Lean_Parser_ParserState_pushSyntax(x_4, x_2);
+x_6 = lean_ctor_get(x_4, 3);
+lean_inc(x_6);
+lean_dec(x_4);
+if (lean_obj_tag(x_6) == 0)
+{
+lean_object* x_7; 
+x_7 = lean_apply_3(x_1, x_2, x_3, x_5);
+return x_7;
+}
+else
+{
+lean_dec(x_6);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_5;
+}
+}
+}
+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_inc(x_3);
+x_4 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_4, 0, x_3);
+x_5 = l_String_trim(x_1);
+x_6 = l_String_trim(x_2);
+lean_inc(x_6);
+lean_inc(x_5);
+x_7 = l_Lean_Parser_unicodeSymbolInfo(x_5, x_6, x_4);
+x_8 = lean_alloc_closure((void*)(l_Lean_Parser_unicodeSymbolFn___rarg___boxed), 5, 2);
+lean_closure_set(x_8, 0, x_5);
+lean_closure_set(x_8, 1, x_6);
+x_9 = 1;
+x_10 = l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
+lean_inc(x_3);
+x_11 = l_Lean_Parser_categoryParser(x_9, x_10, x_3);
+x_12 = lean_ctor_get(x_11, 0);
+lean_inc(x_12);
+lean_dec(x_11);
+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);
+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;
+}
+}
+lean_object* l_Lean_Parser_Term_unicodeInfixL___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_Parser_Term_unicodeInfixL(x_1, x_2, x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_4;
+}
+}
+lean_object* l_Lean_Parser_Term_infixL___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; 
+lean_inc(x_2);
+lean_inc(x_4);
+x_5 = l_Lean_Parser_ParserState_pushSyntax(x_4, x_2);
+x_6 = lean_ctor_get(x_4, 3);
+lean_inc(x_6);
+lean_dec(x_4);
+if (lean_obj_tag(x_6) == 0)
+{
+lean_object* x_7; 
+x_7 = lean_apply_3(x_1, x_2, x_3, x_5);
+return x_7;
+}
+else
+{
+lean_dec(x_6);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_5;
+}
+}
+}
+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_inc(x_2);
+x_3 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_3, 0, x_2);
+x_4 = l_String_trim(x_1);
+lean_inc(x_4);
+x_5 = l_Lean_Parser_symbolInfo(x_4, x_3);
+x_6 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
+lean_closure_set(x_6, 0, x_4);
+x_7 = 1;
+x_8 = l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
+lean_inc(x_2);
+x_9 = l_Lean_Parser_categoryParser(x_7, x_8, x_2);
+x_10 = lean_ctor_get(x_9, 0);
+lean_inc(x_10);
+lean_dec(x_9);
+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);
+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;
+}
+}
+lean_object* l_Lean_Parser_Term_infixL___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
 lean_object* _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__1() {
 _start:
 {
@ -30381,7 +30689,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
 x_1 = l_Lean_Parser_Term_depArrow___elambda__1___closed__6;
 x_2 = l_Lean_Parser_Term_depArrow___elambda__1___closed__8;
 x_3 = lean_unsigned_to_nat(25u);
-x_4 = l_Lean_Parser_unicodeInfixR(x_1, x_2, x_3);
+x_4 = l_Lean_Parser_Term_unicodeInfixR(x_1, x_2, x_3);
 return x_4;
 }
 }
@ -31951,7 +32259,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_fcomp___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(90u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -32056,7 +32364,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_prod___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(35u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -32161,7 +32469,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_add___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(65u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -32266,7 +32574,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_sub___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(65u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -32371,7 +32679,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_mul___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(70u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -32476,7 +32784,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_div___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(70u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -32581,7 +32889,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_mod___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(70u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -32686,7 +32994,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_modN___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(70u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -32791,7 +33099,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_pow___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(80u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -32905,7 +33213,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
 x_1 = l_Lean_Parser_Term_le___elambda__1___closed__3;
 x_2 = l_Lean_Parser_Term_le___elambda__1___closed__4;
 x_3 = lean_unsigned_to_nat(50u);
-x_4 = l_Lean_Parser_unicodeInfixL(x_1, x_2, x_3);
+x_4 = l_Lean_Parser_Term_unicodeInfixL(x_1, x_2, x_3);
 return x_4;
 }
 }
@ -33019,7 +33327,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
 x_1 = l_Lean_Parser_Term_ge___elambda__1___closed__3;
 x_2 = l_Lean_Parser_Term_ge___elambda__1___closed__4;
 x_3 = lean_unsigned_to_nat(50u);
-x_4 = l_Lean_Parser_unicodeInfixL(x_1, x_2, x_3);
+x_4 = l_Lean_Parser_Term_unicodeInfixL(x_1, x_2, x_3);
 return x_4;
 }
 }
@ -33124,7 +33432,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_lt___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(50u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -33229,7 +33537,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_gt___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(50u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -33334,7 +33642,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_eq___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(50u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -33439,7 +33747,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_ne___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(50u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -33544,7 +33852,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_beq___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(50u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -33649,7 +33957,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_bne___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(50u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -33763,7 +34071,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
 x_1 = l_Lean_Parser_Term_heq___elambda__1___closed__3;
 x_2 = l_Lean_Parser_Term_heq___elambda__1___closed__4;
 x_3 = lean_unsigned_to_nat(50u);
-x_4 = l_Lean_Parser_unicodeInfixL(x_1, x_2, x_3);
+x_4 = l_Lean_Parser_Term_unicodeInfixL(x_1, x_2, x_3);
 return x_4;
 }
 }
@ -33868,7 +34176,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_equiv___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(50u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -33973,7 +34281,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_subst___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(75u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -34087,7 +34395,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
 x_1 = l_Lean_Parser_Term_and___elambda__1___closed__3;
 x_2 = l_Lean_Parser_Term_and___elambda__1___closed__4;
 x_3 = lean_unsigned_to_nat(35u);
-x_4 = l_Lean_Parser_unicodeInfixR(x_1, x_2, x_3);
+x_4 = l_Lean_Parser_Term_unicodeInfixR(x_1, x_2, x_3);
 return x_4;
 }
 }
@ -34201,7 +34509,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
 x_1 = l_Lean_Parser_Term_or___elambda__1___closed__3;
 x_2 = l_Lean_Parser_Term_or___elambda__1___closed__4;
 x_3 = lean_unsigned_to_nat(30u);
-x_4 = l_Lean_Parser_unicodeInfixR(x_1, x_2, x_3);
+x_4 = l_Lean_Parser_Term_unicodeInfixR(x_1, x_2, x_3);
 return x_4;
 }
 }
@ -34315,7 +34623,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
 x_1 = l_Lean_Parser_Term_iff___elambda__1___closed__3;
 x_2 = l_Lean_Parser_Term_iff___elambda__1___closed__4;
 x_3 = lean_unsigned_to_nat(20u);
-x_4 = l_Lean_Parser_unicodeInfixL(x_1, x_2, x_3);
+x_4 = l_Lean_Parser_Term_unicodeInfixL(x_1, x_2, x_3);
 return x_4;
 }
 }
@ -34420,7 +34728,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_band___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(35u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -34525,7 +34833,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_bor___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(30u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -34630,7 +34938,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_append___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(65u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -34735,7 +35043,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_cons___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(67u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -34840,7 +35148,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_orelse___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(2u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -34945,7 +35253,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_orM___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(30u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -35050,7 +35358,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_andM___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(35u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -35155,7 +35463,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_andthen___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(60u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -35260,7 +35568,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_bindOp___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(55u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -35365,7 +35673,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_mapRev___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(100u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -35470,7 +35778,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_seq___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(60u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -35575,7 +35883,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_seqLeft___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(60u);
-x_3 = l_Lean_Parser_infixL(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }
@ -35680,7 +35988,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_seqRight___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(60u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -35785,7 +36093,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_map___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(100u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -35890,7 +36198,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_mapConst___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(100u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
@ -35995,7 +36303,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_mapConstRev___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(100u);
-x_3 = l_Lean_Parser_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
 return x_3;
 }
 }
--- a/stage0/stdlib/Init/LeanExt.c
+++ b/stage0/stdlib/Init/LeanExt.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.LeanExt
-// Imports: Init.Data.String.Basic Init.Data.UInt
+// Imports: Init.Data.String.Basic Init.Data.UInt Init.Data.Hashable
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -19,19 +19,27 @@ lean_object* l_Lean_ParserDescr_optional(uint8_t, lean_object*);
 lean_object* l_Lean_ParserDescr_lookahead(uint8_t, lean_object*);
 lean_object* l_Lean_ParserDescr_many(uint8_t, lean_object*);
 lean_object* l_Lean_ParserDescr_ident(uint8_t);
+lean_object* l_Lean_mkNameSimple(lean_object*);
 lean_object* l_Lean_ParserDescr_andthen___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_char(uint8_t);
+lean_object* l_Lean_Name_inhabited;
 extern lean_object* l_String_splitAux___main___closed__1;
+lean_object* l_Lean_Name_hashable___closed__1;
 lean_object* l_Lean_ParserDescr_try(uint8_t, lean_object*);
+lean_object* l_Lean_Name_hashable;
 lean_object* l_Lean_ParserDescr_str(uint8_t);
 lean_object* l_Lean_ParserDescrCore_inhabited(uint8_t);
 lean_object* l_Lean_ParserDescr_many1(uint8_t, lean_object*);
 lean_object* l_Lean_ParserDescr_many___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_num___boxed(lean_object*);
 lean_object* l_Lean_ParserDescr_many1___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_Name_hashEx___boxed(lean_object*);
+size_t lean_name_hash(lean_object*);
+size_t l_Lean_Name_hash(lean_object*);
 lean_object* l_Lean_ParserDescr_parser(lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_lookahead___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_sepBy(uint8_t, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_andthen(uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_symbol___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_node(uint8_t, lean_object*, lean_object*);
@ -39,17 +47,128 @@ lean_object* l_Lean_ParserDescr_try___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_ident___boxed(lean_object*);
 lean_object* l_Lean_ParserDescr_str___boxed(lean_object*);
 lean_object* l_Lean_ParserDescr_node___boxed(lean_object*, lean_object*, lean_object*);
+size_t lean_usize_of_nat(lean_object*);
 lean_object* l_Lean_ParserDescr_nonReservedSymbol___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescrCore_inhabited___boxed(lean_object*);
 lean_object* l_Lean_ParserDescr_sepBy1(uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_char___boxed(lean_object*);
 lean_object* l_Lean_ParserDescr_orelse___boxed(lean_object*, lean_object*, lean_object*);
+size_t lean_usize_mix_hash(size_t, size_t);
 lean_object* l_Lean_ParserDescr_sepBy___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_num(uint8_t);
 lean_object* l_Lean_ParserDescr_symbol(uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_optional___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_ParserDescr_nonReservedSymbol(lean_object*, uint8_t);
+lean_object* l_Lean_Name_hash___boxed(lean_object*);
+lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
+size_t lean_string_hash(lean_object*);
 lean_object* l_Lean_ParserDescr_sepBy1___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* _init_l_Lean_Name_inhabited() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_box(0);
+return x_1;
+}
+}
+size_t l_Lean_Name_hash(lean_object* x_1) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+size_t x_2; 
+x_2 = 1723;
+return x_2;
+}
+else
+{
+size_t x_3; 
+x_3 = lean_ctor_get_usize(x_1, 2);
+return x_3;
+}
+}
+}
+lean_object* l_Lean_Name_hash___boxed(lean_object* x_1) {
+_start:
+{
+size_t x_2; lean_object* x_3; 
+x_2 = l_Lean_Name_hash(x_1);
+lean_dec(x_1);
+x_3 = lean_box_usize(x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Name_hashable___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Name_hash___boxed), 1, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Name_hashable() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_Name_hashable___closed__1;
+return x_1;
+}
+}
+size_t lean_name_hash(lean_object* x_1) {
+_start:
+{
+size_t x_2; 
+x_2 = l_Lean_Name_hash(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
+lean_object* l_Lean_Name_hashEx___boxed(lean_object* x_1) {
+_start:
+{
+size_t x_2; lean_object* x_3; 
+x_2 = lean_name_hash(x_1);
+x_3 = lean_box_usize(x_2);
+return x_3;
+}
+}
+lean_object* lean_name_mk_string(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+size_t x_3; size_t x_4; size_t x_5; lean_object* x_6; 
+x_3 = l_Lean_Name_hash(x_1);
+x_4 = lean_string_hash(x_2);
+x_5 = lean_usize_mix_hash(x_3, x_4);
+x_6 = lean_alloc_ctor(1, 2, sizeof(size_t)*1);
+lean_ctor_set(x_6, 0, x_1);
+lean_ctor_set(x_6, 1, x_2);
+lean_ctor_set_usize(x_6, 2, x_5);
+return x_6;
+}
+}
+lean_object* lean_name_mk_numeral(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+size_t x_3; size_t x_4; size_t x_5; lean_object* x_6; 
+x_3 = l_Lean_Name_hash(x_1);
+x_4 = lean_usize_of_nat(x_2);
+x_5 = lean_usize_mix_hash(x_3, x_4);
+x_6 = lean_alloc_ctor(2, 2, sizeof(size_t)*1);
+lean_ctor_set(x_6, 0, x_1);
+lean_ctor_set(x_6, 1, x_2);
+lean_ctor_set_usize(x_6, 2, x_5);
+return x_6;
+}
+}
+lean_object* l_Lean_mkNameSimple(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; 
+x_2 = lean_box(0);
+x_3 = lean_name_mk_string(x_2, x_1);
+return x_3;
+}
+}
 lean_object* l_Lean_ParserDescrCore_inhabited(uint8_t x_1) {
 _start:
 {
@ -415,6 +534,7 @@ return x_3;
 }
 lean_object* initialize_Init_Data_String_Basic(lean_object*);
 lean_object* initialize_Init_Data_UInt(lean_object*);
+lean_object* initialize_Init_Data_Hashable(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_LeanExt(lean_object* w) {
 lean_object * res;
@ -426,6 +546,15 @@ lean_dec_ref(res);
 res = initialize_Init_Data_UInt(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Data_Hashable(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_Lean_Name_inhabited = _init_l_Lean_Name_inhabited();
+lean_mark_persistent(l_Lean_Name_inhabited);
+l_Lean_Name_hashable___closed__1 = _init_l_Lean_Name_hashable___closed__1();
+lean_mark_persistent(l_Lean_Name_hashable___closed__1);
+l_Lean_Name_hashable = _init_l_Lean_Name_hashable();
+lean_mark_persistent(l_Lean_Name_hashable);
 l_Lean_ParserDescr_pushLeading = _init_l_Lean_ParserDescr_pushLeading();
 lean_mark_persistent(l_Lean_ParserDescr_pushLeading);
 return lean_mk_io_result(lean_box(0));