chore: update stage0

2020-11-29 16:24:37 -08:00 · 2020-11-29 16:24:37 -08:00 · 62639da58c
commit 62639da58c
parent 390eea3750
38 changed files with 14987 additions and 11275 deletions
--- a/stage0/src/Init/NotationExtra.lean
+++ b/stage0/src/Init/NotationExtra.lean
@ -69,7 +69,7 @@ private def mkHintBody (cs : Array Syntax) (p : Syntax) : MacroM Syntax := do
  return body

 macro_rules
-  | `(unif_hint $bs* where $cs* |- $p) => do
+  | `(unif_hint $bs:explicitBinder* where $cs* |- $p) => do
    let body ← mkHintBody cs p
    `(@[unificationHint] def hint $bs:explicitBinder* : Sort _ := $body)
  | `(unif_hint $n:ident $bs* where $cs* |- $p) => do
--- a/stage0/src/Init/Prelude.lean
+++ b/stage0/src/Init/Prelude.lean
@ -340,6 +340,9 @@ inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

+instance : Inhabited Nat where
+  default := Nat.zero
+
 /- For numeric literals notation -/
 class OfNat (α : Type u) where
  ofNat : Nat → α
@ -350,8 +353,25 @@ export OfNat (ofNat)
 instance : OfNat Nat where
  ofNat x := x

-instance : Inhabited Nat where
-  default := 0
+class One (α : Type u) where
+  one : α
+
+instance [OfNat α] : One α where
+  one := ofNat Nat.zero.succ
+
+class Zero (α : Type u) where
+  zero : α
+
+instance [OfNat α] : Zero α where
+  zero := ofNat Nat.zero
+
+@[defaultInstance]
+instance : One Nat where
+  one := Nat.zero.succ
+
+@[defaultInstance]
+instance : Zero Nat where
+  zero := Nat.zero

 class HasLessEq (α : Type u) where LessEq : α → α → Prop
 class HasLess   (α : Type u) where Less : α → α → Prop
--- a/stage0/src/Lean/Delaborator.lean
+++ b/stage0/src/Lean/Delaborator.lean
@ -603,7 +603,21 @@ def delabLit : Delab := do
@[builtinDelab app.OfNat.ofNat]
 def delabOfNat : Delab := whenPPOption getPPCoercions do
  let e@(Expr.app _ (Expr.lit (Literal.natVal n) _) _) ← getExpr | failure
-  pure $ quote n
+  return quote n
+
+-- `One.one` ~> `1`
+@[builtinDelab app.One.one]
+def delabOne : Delab := whenPPOption getPPCoercions do
+  let e ← getExpr
+  guard <| e.getAppNumArgs == 2
+  return quote (1:Nat)
+
+-- `Zero.zero` ~> `0`
+@[builtinDelab app.Zero.zero]
+def delabZero : Delab := whenPPOption getPPCoercions do
+  let e ← getExpr
+  guard <| e.getAppNumArgs == 2
+  return quote (0:Nat)

 /--
 Delaborate a projection primitive. These do not usually occur in
--- a/stage0/src/Lean/Elab/Inductive.lean
+++ b/stage0/src/Lean/Elab/Inductive.lean
@ -18,7 +18,10 @@ open Meta
 builtin_initialize
  registerTraceClass `Elab.inductive

-def checkValidInductiveModifier (modifiers : Modifiers) : CommandElabM Unit := do
+section
+variables {m : Type → Type} [Monad m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m]
+
+def checkValidInductiveModifier (modifiers : Modifiers) : m Unit := do
  if modifiers.isNoncomputable then
    throwError "invalid use of 'noncomputable' in inductive declaration"
  if modifiers.isPartial then
@ -26,7 +29,7 @@ def checkValidInductiveModifier (modifiers : Modifiers) : CommandElabM Unit := d
  unless modifiers.attrs.size == 0 || (modifiers.attrs.size == 1 && modifiers.attrs[0].name == `class) do
    throwError "invalid use of attributes in inductive declaration"

-def checkValidCtorModifier (modifiers : Modifiers) : CommandElabM Unit := do
+def checkValidCtorModifier (modifiers : Modifiers) : m Unit := do
  if modifiers.isNoncomputable then
    throwError "invalid use of 'noncomputable' in constructor declaration"
  if modifiers.isPartial then
@ -36,6 +39,8 @@ def checkValidCtorModifier (modifiers : Modifiers) : CommandElabM Unit := do
  if modifiers.attrs.size != 0 then
    throwError "invalid use of attributes in constructor declaration"

+end
+
 structure CtorView where
  ref       : Syntax
  modifiers : Modifiers
@ -448,7 +453,7 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
  checkLevelNames views
  let allUserLevelNames := view0.levelNames
  let isUnsafe          := view0.modifiers.isUnsafe
-  withRef view0.ref $ Term.withLevelNames allUserLevelNames do
+  withRef view0.ref <| Term.withLevelNames allUserLevelNames do
    let rs ← elabHeader views
    withInductiveLocalDecls rs fun params indFVars => do
      let numExplicitParams := params.size
--- a/stage0/src/Lean/Elab/Structure.lean
+++ b/stage0/src/Lean/Elab/Structure.lean
@ -97,7 +97,7 @@ The structure constructor syntax is
 parser! try (declModifiers >> ident >> optional inferMod >> " :: ")
 ```
 -/
-private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM StructCtorView :=
+private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM StructCtorView :=
  let useDefault :=
    pure { ref := structStx, modifiers := {}, inferMod := false, name := defaultCtorName, declName := structDeclName ++ defaultCtorName }
  if structStx[5].isNone then
@ -121,7 +121,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
      let declName ← applyVisibility ctorModifiers.visibility declName
      pure { ref := ctor, name := name, modifiers := ctorModifiers, inferMod := inferMod, declName := declName }

-def checkValidFieldModifier (modifiers : Modifiers) : CommandElabM Unit := do
+def checkValidFieldModifier (modifiers : Modifiers) : TermElabM Unit := do
  if modifiers.isNoncomputable then
    throwError "invalid use of 'noncomputable' in field declaration"
  if modifiers.isPartial then
@ -142,7 +142,7 @@ def structSimpleBinder   := parser! atomic (declModifiers true >> many1 ident) >
 def structFields         := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
 ```
 -/
-private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM (Array StructFieldView) :=
+private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM (Array StructFieldView) :=
  let fieldBinders := if structStx[5].isNone then #[] else structStx[5][2][0].getArgs
  fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do
    let mut fieldBinder := fieldBinder
@ -470,7 +470,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
      trace[Elab.structure]! "type: {type}"
      let usedLevelNames ← collectLevelParamsInStructure type scopeVars view.params fieldInfos
      match sortDeclLevelParams view.scopeLevelNames view.allUserLevelNames usedLevelNames with
-      | Except.error msg      => throwError msg
+      | Except.error msg      => withRef view.ref <| throwError msg
      | Except.ok levelParams =>
        let params := scopeVars ++ view.params
        let ctor ← mkCtor view levelParams params fieldInfos
@ -528,24 +528,31 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
  let parents   := if exts.isNone then #[] else exts[0][1].getSepArgs
  let optType   := stx[4]
  let type ← if optType.isNone then `(Sort _) else pure optType[0][1]
-  let scopeLevelNames ← getLevelNames
-  let ⟨name, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers
-  let ctor ← expandCtor stx modifiers declName
-  let fields ← expandFields stx modifiers declName
-  runTermElabM declName $ fun scopeVars => Term.withLevelNames allUserLevelNames $ Term.elabBinders params fun params => elabStructureView {
-    ref               := stx,
-    modifiers         := modifiers,
-    scopeLevelNames   := scopeLevelNames,
-    allUserLevelNames := allUserLevelNames,
-    declName          := declName,
-    isClass           := isClass,
-    scopeVars         := scopeVars,
-    params            := params,
-    parents           := parents,
-    type              := type,
-    ctor              := ctor,
-    fields            := fields
-  }
+  runTermElabM none fun scopeVars => do
+    let scopeLevelNames ← Term.getLevelNames
+    let ⟨name, declName, allUserLevelNames⟩ ← Elab.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
+    Term.withDeclName declName do
+      let ctor ← expandCtor stx modifiers declName
+      let fields ← expandFields stx modifiers declName
+      Term.withLevelNames allUserLevelNames <| Term.withAutoBoundImplicitLocal <|
+        Term.elabBinders params (catchAutoBoundImplicit := true) fun params => do
+          let params ← Term.addAutoBoundImplicits params
+          let allUserLevelNames ← Term.getLevelNames
+          Term.withAutoBoundImplicitLocal (flag := false) do
+            elabStructureView {
+              ref               := stx,
+              modifiers         := modifiers,
+              scopeLevelNames   := scopeLevelNames,
+              allUserLevelNames := allUserLevelNames,
+              declName          := declName,
+              isClass           := isClass,
+              scopeVars         := scopeVars,
+              params            := params,
+              parents           := parents,
+              type              := type,
+              ctor              := ctor,
+              fields            := fields
+            }

 builtin_initialize registerTraceClass `Elab.structure

--- a/stage0/src/Lean/Elab/Syntax.lean
+++ b/stage0/src/Lean/Elab/Syntax.lean
@ -332,6 +332,11 @@ def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
  | `(infixl:$prec $op => $f)  =>  let prec1 : Syntax := quote (prec.toNat+1); `(notation:$prec lhs $op:strLit rhs:$prec1 => $f lhs rhs)
  | `(prefix:$prec $op => $f)  => `(notation:$prec $op:strLit arg:$prec => $f arg)
  | `(postfix:$prec $op => $f) => `(notation:$prec arg $op:strLit => $f arg)
+  | `(infix:$prec [$prio] $op => $f)   => `(infixl:$prec [$prio] $op => $f)
+  | `(infixr:$prec [$prio] $op => $f)  => `(notation:$prec [$prio] lhs $op:strLit rhs:$prec => $f lhs rhs)
+  | `(infixl:$prec [$prio] $op => $f)  =>  let prec1 : Syntax := quote (prec.toNat+1); `(notation:$prec [$prio] lhs $op:strLit rhs:$prec1 => $f lhs rhs)
+  | `(prefix:$prec [$prio] $op => $f)  => `(notation:$prec [$prio] $op:strLit arg:$prec => $f arg)
+  | `(postfix:$prec [$prio] $op => $f) => `(notation:$prec [$prio] arg $op:strLit => $f arg)
  | _ => Macro.throwUnsupported

 /- Wrap all occurrences of the given `ident` nodes in antiquotations -/
@ -372,7 +377,7 @@ def expandNotationItemIntoPattern (stx : Syntax) : MacroM Syntax :=
  else
    Macro.throwUnsupported

-private def expandNotationAux (ref : Syntax) (currNamespace : Name) (prec? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : MacroM Syntax := do
+private def expandNotationAux (ref : Syntax) (currNamespace : Name) (prec? : Option Syntax) (prio : Nat) (items : Array Syntax) (rhs : Syntax) : MacroM Syntax := do
  let kind ← mkFreshKind `term
  -- build parser
  let syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem
@ -386,15 +391,17 @@ private def expandNotationAux (ref : Syntax) (currNamespace : Name) (prec? : Opt
     So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
  let pat := Syntax.node (currNamespace ++ kind) patArgs
  match prec? with
-  | none      => `(syntax [$(mkIdentFrom ref kind):ident] $syntaxParts* : $cat macro_rules | `($pat) => `($rhs))
-  | some prec => `(syntax:$prec [$(mkIdentFrom ref kind):ident] $syntaxParts* : $cat macro_rules | `($pat) => `($rhs))
+  | none      => `(syntax [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat macro_rules | `($pat) => `($rhs))
+  | some prec => `(syntax:$prec [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat macro_rules | `($pat) => `($rhs))

@[builtinCommandElab «notation»] def expandNotation : CommandElab :=
  adaptExpander fun stx => do
    let currNamespace ← getCurrNamespace
    match_syntax stx with
-    | `(notation:$prec $items* => $rhs)        => liftMacroM $ expandNotationAux stx currNamespace prec items rhs
-    | `(notation $items:notationItem* => $rhs) => liftMacroM $ expandNotationAux stx currNamespace none items rhs
+    | `(notation:$prec $items* => $rhs)                => liftMacroM <| expandNotationAux stx currNamespace prec 0 items rhs
+    | `(notation $items:notationItem* => $rhs)         => liftMacroM <| expandNotationAux stx currNamespace none 0 items rhs
+    | `(notation:$prec [$prio] $items* => $rhs)        => liftMacroM <| expandNotationAux stx currNamespace prec (prio.isNatLit?.getD 0) items rhs
+    | `(notation [$prio] $items:notationItem* => $rhs) => liftMacroM <| expandNotationAux stx currNamespace none (prio.isNatLit?.getD 0) items rhs
    | _ => throwUnsupportedSyntax

 /- Convert `macro` argument into a `syntax` command item -/
--- a/stage0/src/Lean/Elab/Term.lean
+++ b/stage0/src/Lean/Elab/Term.lean
@ -1255,7 +1255,7 @@ def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitL

@[builtinTermElab numLit] def elabNumLit : TermElab := fun stx expectedType? => do
  let val ← match stx.isNatLit? with
-    | some val => pure (mkNatLit val)
+    | some val => pure val
    | none     => throwIllFormedSyntax
  let typeMVar ← mkFreshTypeMVar MetavarKind.synthetic
  match expectedType? with
@ -1263,8 +1263,15 @@ def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitL
  | _                 => pure ()
  let u ← getLevel typeMVar
  let u ← decLevel u
-  let mvar ← mkInstMVar (mkApp (Lean.mkConst `OfNat [u]) typeMVar)
-  pure $ mkApp3 (Lean.mkConst `OfNat.ofNat [u]) typeMVar mvar val
+  if val == 0 then
+    let mvar ← mkInstMVar (mkApp (Lean.mkConst `Zero [u]) typeMVar)
+    return mkApp2 (Lean.mkConst `Zero.zero [u]) typeMVar mvar
+  else if val == 1 then
+    let mvar ← mkInstMVar (mkApp (Lean.mkConst `One [u]) typeMVar)
+    return mkApp2 (Lean.mkConst `One.one [u]) typeMVar mvar
+  else
+    let mvar ← mkInstMVar (mkApp (Lean.mkConst `OfNat [u]) typeMVar)
+    return mkApp3 (Lean.mkConst `OfNat.ofNat [u]) typeMVar mvar (mkNatLit val)

@[builtinTermElab charLit] def elabCharLit : TermElab := fun stx _ => do
  match stx.isCharLit? with
--- a/stage0/src/Lean/Meta/Offset.lean
+++ b/stage0/src/Lean/Meta/Offset.lean
@ -58,6 +58,10 @@ where
        return v₁ * v₂
      else if c == `OfNat.ofNat && nargs == 3 then
        evalNat (e.getArg! 2)
+      else if c == `One.one && nargs == 2 then
+        return 1
+      else if c == `Zero.zero && nargs == 2 then
+        return 0
      else
        failure
    | _ => failure
--- a/stage0/src/Lean/Meta/UnificationHint.lean
+++ b/stage0/src/Lean/Meta/UnificationHint.lean
@ -87,6 +87,7 @@ builtin_initialize
  }

 def tryUnificationHints (t s : Expr) : MetaM Bool := do
+  trace[Meta.isDefEq.hint]! "{t} =?= {s}"
  unless (← read).config.unificationHints do
    return false
  if t.isMVar then
--- a/stage0/src/Lean/Parser/Syntax.lean
+++ b/stage0/src/Lean/Parser/Syntax.lean
@ -50,21 +50,13 @@ def «infixl»   := parser! "infixl"
 def «infixr»   := parser! "infixr"
 def «postfix»  := parser! "postfix"
 def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «postfix»
-@[builtinCommandParser] def «mixfix»   := parser!
-  (checkOutsideQuot >> mixfixKind >> optPrecedence >> ppSpace >> strLit >> darrow >> termParser)
-  <|>
-  (checkInsideQuot >> mixfixKind >> optPrecedence >> optPrio >> ppSpace >> strLit >> darrow >> termParser)
-
+@[builtinCommandParser] def «mixfix»   := parser! mixfixKind >> optPrecedence >> optPrio >> ppSpace >> strLit >> darrow >> termParser
 -- NOTE: We use `suppressInsideQuot` in the following parsers because quotations inside them are evaluated in the same stage and
 -- thus should be ignored when we use `checkInsideQuot` to prepare the next stage for a builtin syntax change
 def identPrec  := parser! ident >> optPrecedence
 def optKind : Parser := optional ("[" >> ident >> "]")
 def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Parser.Command.notationItem) (strLit <|> identPrec)
-@[builtinCommandParser] def «notation»    := parser!
-  (checkOutsideQuot >> "notation" >> optPrecedence >> many notationItem >> darrow >> termParser)
-  <|>
-  (checkInsideQuot >> "notation" >> optPrecedence >> optPrio >> many notationItem >> darrow >> termParser)
-
+@[builtinCommandParser] def «notation»    := parser! "notation" >> optPrecedence >> optPrio >> many notationItem >> darrow >> termParser
@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (parser! "macro_rules" >> optKind >> Term.matchAlts)
 def parserKind     := parser! ident
 def parserPrio     := parser! numLit
--- a/stage0/src/library/constants.cpp
+++ b/stage0/src/library/constants.cpp
@ -108,108 +108,211 @@ name const * g_uint64 = nullptr;
 name const * g_usize = nullptr;
 void initialize_constants() {
    g_absurd = new name{"absurd"};
+    mark_persistent(g_absurd->raw());
    g_and = new name{"And"};
+    mark_persistent(g_and->raw());
    g_and_left = new name{"And", "left"};
+    mark_persistent(g_and_left->raw());
    g_and_right = new name{"And", "right"};
+    mark_persistent(g_and_right->raw());
    g_and_intro = new name{"And", "intro"};
+    mark_persistent(g_and_intro->raw());
    g_and_rec = new name{"And", "rec"};
+    mark_persistent(g_and_rec->raw());
    g_and_cases_on = new name{"And", "casesOn"};
+    mark_persistent(g_and_cases_on->raw());
    g_array = new name{"Array"};
+    mark_persistent(g_array->raw());
    g_array_sz = new name{"Array", "sz"};
+    mark_persistent(g_array_sz->raw());
    g_array_data = new name{"Array", "data"};
+    mark_persistent(g_array_data->raw());
    g_auto_param = new name{"autoParam"};
+    mark_persistent(g_auto_param->raw());
    g_bit0 = new name{"bit0"};
+    mark_persistent(g_bit0->raw());
    g_bit1 = new name{"bit1"};
+    mark_persistent(g_bit1->raw());
    g_has_of_nat_of_nat = new name{"HasOfNat", "ofNat"};
+    mark_persistent(g_has_of_nat_of_nat->raw());
    g_byte_array = new name{"ByteArray"};
+    mark_persistent(g_byte_array->raw());
    g_bool = new name{"Bool"};
+    mark_persistent(g_bool->raw());
    g_bool_false = new name{"Bool", "false"};
+    mark_persistent(g_bool_false->raw());
    g_bool_true = new name{"Bool", "true"};
+    mark_persistent(g_bool_true->raw());
    g_bool_cases_on = new name{"Bool", "casesOn"};
+    mark_persistent(g_bool_cases_on->raw());
    g_cast = new name{"cast"};
+    mark_persistent(g_cast->raw());
    g_char = new name{"Char"};
+    mark_persistent(g_char->raw());
    g_congr_arg = new name{"congrArg"};
+    mark_persistent(g_congr_arg->raw());
    g_decidable = new name{"Decidable"};
+    mark_persistent(g_decidable->raw());
    g_decidable_is_true = new name{"Decidable", "isTrue"};
+    mark_persistent(g_decidable_is_true->raw());
    g_decidable_is_false = new name{"Decidable", "isFalse"};
+    mark_persistent(g_decidable_is_false->raw());
    g_decidable_decide = new name{"Decidable", "decide"};
+    mark_persistent(g_decidable_decide->raw());
    g_empty = new name{"Empty"};
+    mark_persistent(g_empty->raw());
    g_empty_rec = new name{"Empty", "rec"};
+    mark_persistent(g_empty_rec->raw());
    g_empty_cases_on = new name{"Empty", "casesOn"};
+    mark_persistent(g_empty_cases_on->raw());
    g_exists = new name{"Exists"};
+    mark_persistent(g_exists->raw());
    g_eq = new name{"Eq"};
+    mark_persistent(g_eq->raw());
    g_eq_cases_on = new name{"Eq", "casesOn"};
+    mark_persistent(g_eq_cases_on->raw());
    g_eq_rec_on = new name{"Eq", "recOn"};
+    mark_persistent(g_eq_rec_on->raw());
    g_eq_rec = new name{"Eq", "rec"};
+    mark_persistent(g_eq_rec->raw());
    g_eq_ndrec = new name{"Eq", "ndrec"};
+    mark_persistent(g_eq_ndrec->raw());
    g_eq_refl = new name{"Eq", "refl"};
+    mark_persistent(g_eq_refl->raw());
    g_eq_subst = new name{"Eq", "subst"};
+    mark_persistent(g_eq_subst->raw());
    g_eq_symm = new name{"Eq", "symm"};
+    mark_persistent(g_eq_symm->raw());
    g_eq_trans = new name{"Eq", "trans"};
+    mark_persistent(g_eq_trans->raw());
    g_float = new name{"Float"};
+    mark_persistent(g_float->raw());
    g_float_array = new name{"FloatArray"};
+    mark_persistent(g_float_array->raw());
    g_false = new name{"False"};
+    mark_persistent(g_false->raw());
    g_false_rec = new name{"False", "rec"};
+    mark_persistent(g_false_rec->raw());
    g_false_cases_on = new name{"False", "casesOn"};
+    mark_persistent(g_false_cases_on->raw());
    g_has_add_add = new name{"HasAdd", "add"};
+    mark_persistent(g_has_add_add->raw());
    g_has_neg_neg = new name{"HasNeg", "neg"};
+    mark_persistent(g_has_neg_neg->raw());
    g_has_one_one = new name{"HasOne", "one"};
+    mark_persistent(g_has_one_one->raw());
    g_has_zero_zero = new name{"HasZero", "zero"};
+    mark_persistent(g_has_zero_zero->raw());
    g_heq = new name{"HEq"};
+    mark_persistent(g_heq->raw());
    g_heq_refl = new name{"HEq", "refl"};
+    mark_persistent(g_heq_refl->raw());
    g_iff = new name{"Iff"};
+    mark_persistent(g_iff->raw());
    g_iff_refl = new name{"Iff", "refl"};
+    mark_persistent(g_iff_refl->raw());
    g_int = new name{"Int"};
+    mark_persistent(g_int->raw());
    g_int_nat_abs = new name{"Int", "natAbs"};
+    mark_persistent(g_int_nat_abs->raw());
    g_int_dec_lt = new name{"Int", "decLt"};
+    mark_persistent(g_int_dec_lt->raw());
    g_int_of_nat = new name{"Int", "ofNat"};
+    mark_persistent(g_int_of_nat->raw());
    g_inline = new name{"inline"};
+    mark_persistent(g_inline->raw());
    g_io = new name{"IO"};
+    mark_persistent(g_io->raw());
    g_ite = new name{"ite"};
+    mark_persistent(g_ite->raw());
    g_lc_proof = new name{"lcProof"};
+    mark_persistent(g_lc_proof->raw());
    g_lc_unreachable = new name{"lcUnreachable"};
+    mark_persistent(g_lc_unreachable->raw());
    g_list = new name{"List"};
+    mark_persistent(g_list->raw());
    g_mut_quot = new name{"MutQuot"};
+    mark_persistent(g_mut_quot->raw());
    g_nat = new name{"Nat"};
+    mark_persistent(g_nat->raw());
    g_nat_succ = new name{"Nat", "succ"};
+    mark_persistent(g_nat_succ->raw());
    g_nat_zero = new name{"Nat", "zero"};
+    mark_persistent(g_nat_zero->raw());
    g_nat_has_zero = new name{"Nat", "HasZero"};
+    mark_persistent(g_nat_has_zero->raw());
    g_nat_has_one = new name{"Nat", "HasOne"};
+    mark_persistent(g_nat_has_one->raw());
    g_nat_has_add = new name{"Nat", "HasAdd"};
+    mark_persistent(g_nat_has_add->raw());
    g_nat_add = new name{"Nat", "add"};
+    mark_persistent(g_nat_add->raw());
    g_nat_dec_eq = new name{"Nat", "decEq"};
+    mark_persistent(g_nat_dec_eq->raw());
    g_nat_sub = new name{"Nat", "sub"};
+    mark_persistent(g_nat_sub->raw());
    g_ne = new name{"ne"};
+    mark_persistent(g_ne->raw());
    g_not = new name{"Not"};
+    mark_persistent(g_not->raw());
    g_opt_param = new name{"optParam"};
+    mark_persistent(g_opt_param->raw());
    g_or = new name{"Or"};
+    mark_persistent(g_or->raw());
    g_panic = new name{"panic"};
+    mark_persistent(g_panic->raw());
    g_punit = new name{"PUnit"};
+    mark_persistent(g_punit->raw());
    g_punit_unit = new name{"PUnit", "unit"};
+    mark_persistent(g_punit_unit->raw());
    g_pprod = new name{"PProd"};
+    mark_persistent(g_pprod->raw());
    g_pprod_mk = new name{"PProd", "mk"};
+    mark_persistent(g_pprod_mk->raw());
    g_pprod_fst = new name{"PProd", "fst"};
+    mark_persistent(g_pprod_fst->raw());
    g_pprod_snd = new name{"PProd", "snd"};
+    mark_persistent(g_pprod_snd->raw());
    g_propext = new name{"propext"};
+    mark_persistent(g_propext->raw());
    g_quot_mk = new name{"Quot", "mk"};
+    mark_persistent(g_quot_mk->raw());
    g_quot_lift = new name{"Quot", "lift"};
+    mark_persistent(g_quot_lift->raw());
    g_sorry_ax = new name{"sorryAx"};
+    mark_persistent(g_sorry_ax->raw());
    g_string = new name{"String"};
+    mark_persistent(g_string->raw());
    g_string_data = new name{"String", "data"};
+    mark_persistent(g_string_data->raw());
    g_subsingleton_elim = new name{"Subsingleton", "elim"};
+    mark_persistent(g_subsingleton_elim->raw());
    g_task = new name{"Task"};
+    mark_persistent(g_task->raw());
    g_thunk = new name{"Thunk"};
+    mark_persistent(g_thunk->raw());
    g_thunk_mk = new name{"Thunk", "mk"};
+    mark_persistent(g_thunk_mk->raw());
    g_thunk_get = new name{"Thunk", "get"};
+    mark_persistent(g_thunk_get->raw());
    g_true = new name{"True"};
+    mark_persistent(g_true->raw());
    g_true_intro = new name{"True", "intro"};
+    mark_persistent(g_true_intro->raw());
    g_unit = new name{"Unit"};
+    mark_persistent(g_unit->raw());
    g_unit_unit = new name{"Unit", "unit"};
+    mark_persistent(g_unit_unit->raw());
    g_uint8 = new name{"UInt8"};
+    mark_persistent(g_uint8->raw());
    g_uint16 = new name{"UInt16"};
+    mark_persistent(g_uint16->raw());
    g_uint32 = new name{"UInt32"};
+    mark_persistent(g_uint32->raw());
    g_uint64 = new name{"UInt64"};
+    mark_persistent(g_uint64->raw());
    g_usize = new name{"USize"};
+    mark_persistent(g_usize->raw());
 }
 void finalize_constants() {
    delete g_absurd;
--- a/stage0/src/runtime/alloc.cpp
+++ b/stage0/src/runtime/alloc.cpp
@ -267,10 +267,11 @@ void heap::export_objs() {
 void heap::alloc_segment() {
    if (heap * h = g_heap_manager->pop_orphan()) {
        lean_assert(h->m_curr_segment);
+        /* import pending objects, before moving `h`'s segment to *this* heap. */
+        h->import_objs();
        segment * s = h->m_curr_segment;
        h->m_curr_segment = s->m_next;
        s->move_to_heap(this);
-        h->import_objs();
        if (h->m_curr_segment != nullptr) {
            g_heap_manager->push_orphan(h);
        } else {
@ -369,7 +370,10 @@ extern "C" void * lean_alloc_small(unsigned sz, unsigned slot_idx) {
    if (LEAN_UNLIKELY(r == nullptr)) {
        if (g_heap->m_page_free_list[slot_idx] == nullptr) {
            g_heap->import_objs();
-            p = alloc_page(g_heap, sz);
+            lean_assert(g_heap->m_curr_page[slot_idx] == p);
+            /* g_heap->import_objs() may add objects to p->m_header.m_free_list */
+            if (p->m_header.m_free_list == nullptr)
+                p = alloc_page(g_heap, sz);
        } else {
            p = page_list_pop(g_heap->m_page_free_list[slot_idx]);
            p->m_header.m_in_page_free_list = false;
--- a/stage0/src/runtime/object.cpp
+++ b/stage0/src/runtime/object.cpp
@ -305,6 +305,7 @@ extern "C" b_obj_res lean_thunk_get_core(b_obj_arg t) {
        object * r = lean_apply_1(c, lean_box(0));
        lean_assert(r != nullptr); /* Closure must return a valid lean object */
        lean_assert(lean_to_thunk(t)->m_value == nullptr);
+        mark_mt(r);
        lean_to_thunk(t)->m_value = r;
        return r;
    } else {
--- a/stage0/stdlib/Init/NotationExtra.c
+++ b/stage0/stdlib/Init/NotationExtra.c
--- a/stage0/stdlib/Init/Prelude.c
+++ b/stage0/stdlib/Init/Prelude.c
@ -89,6 +89,7 @@ lean_object* l_instDecidableEqUInt8___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_withRef___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_arbitrary___rarg___boxed(lean_object*);
 lean_object* l_ReaderT_bind___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_instZeroNat;
 lean_object* l_ReaderT_run(lean_object*, lean_object*, lean_object*);
 lean_object* l_instMonadStateOf___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_maxRecDepthErrorMessage;
@ -102,6 +103,7 @@ lean_object* l_instSubNat;
 lean_object* l_ReaderT_instMonadFunctorReaderT___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_foldl___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_run(lean_object*, lean_object*, lean_object*);
+lean_object* l_instOne(lean_object*);
 lean_object* l_UInt8_size;
 lean_object* l_Lean_Syntax_getKind_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_instHasLessEqUInt32;
@ -256,6 +258,7 @@ lean_object* l_cast___rarg___boxed(lean_object*);
 lean_object* l_Lean_Macro_mkMacroEnv___boxed(lean_object*);
 lean_object* l_inferInstance___rarg(lean_object*);
 lean_object* l_Lean_addMacroScope_match__1(lean_object*);
+lean_object* l_instZero(lean_object*);
 lean_object* l_getThe___rarg(lean_object*);
 lean_object* l___private_Init_Prelude_0__Lean_extractMacroScopesAux(lean_object*, lean_object*);
 uint8_t l_Lean_Name_hasMacroScopes(lean_object*);
@ -292,6 +295,7 @@ lean_object* l_Lean_interpolatedStrLitKind___closed__1;
 lean_object* l_EStateM_adaptExcept_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MacroScopesView_review_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_ite(lean_object*, lean_object*);
+lean_object* l_instZero___rarg(lean_object*);
 lean_object* l_Lean_numLitKind;
 lean_object* l_List_set_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_tryCatch_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -379,6 +383,7 @@ lean_object* l_EStateM_map_match__1___rarg(lean_object*, lean_object*, lean_obje
 lean_object* l_ReaderT_bind___at_Lean_Macro_instMonadRefMacroM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_instInhabitedUInt8___closed__1;
 lean_object* l_instMonadFunctorT___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_instOneNat;
 lean_object* l_Lean_Macro_expandMacro_x3f___rarg(lean_object*);
 lean_object* l_Lean_Macro_expandMacroNotAvailable_x3f___closed__1;
 uint16_t l_instInhabitedUInt16___closed__1;
@ -691,6 +696,7 @@ lean_object* l_and_match__1(lean_object*);
 lean_object* l_Lean_Macro_expandMacro_x3fImp(lean_object*, lean_object*, lean_object*);
 lean_object* l_and_match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*);
 lean_object* l_EStateM_instInhabitedResult(lean_object*, lean_object*, lean_object*);
+lean_object* l_instOne___rarg(lean_object*);
 lean_object* l_Lean_Syntax_setArgs_match__1(lean_object*);
 lean_object* l_List_hasDecEq_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_getOp___rarg(lean_object*, lean_object*, lean_object*);
@ -2058,6 +2064,14 @@ x_4 = lean_box(x_3);
 return x_4;
 }
 }
+static lean_object* _init_l_instInhabitedNat() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_unsigned_to_nat(0u);
+return x_1;
+}
+}
 lean_object* l_instOfNatNat(lean_object* x_1) {
 _start:
 {
@ -2074,7 +2088,49 @@ lean_dec(x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_instInhabitedNat() {
+lean_object* l_instOne___rarg(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; 
+x_2 = lean_unsigned_to_nat(1u);
+x_3 = lean_apply_1(x_1, x_2);
+return x_3;
+}
+}
+lean_object* l_instOne(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_instOne___rarg), 1, 0);
+return x_2;
+}
+}
+lean_object* l_instZero___rarg(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; 
+x_2 = lean_unsigned_to_nat(0u);
+x_3 = lean_apply_1(x_1, x_2);
+return x_3;
+}
+}
+lean_object* l_instZero(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_instZero___rarg), 1, 0);
+return x_2;
+}
+}
+static lean_object* _init_l_instOneNat() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_unsigned_to_nat(1u);
+return x_1;
+}
+}
+static lean_object* _init_l_instZeroNat() {
 _start:
 {
 lean_object* x_1; 
@ -11448,6 +11504,10 @@ l_instInhabitedPointedType = _init_l_instInhabitedPointedType();
 lean_mark_persistent(l_instInhabitedPointedType);
 l_instInhabitedNat = _init_l_instInhabitedNat();
 lean_mark_persistent(l_instInhabitedNat);
+l_instOneNat = _init_l_instOneNat();
+lean_mark_persistent(l_instOneNat);
+l_instZeroNat = _init_l_instZeroNat();
+lean_mark_persistent(l_instZeroNat);
 l_instAddNat___closed__1 = _init_l_instAddNat___closed__1();
 lean_mark_persistent(l_instAddNat___closed__1);
 l_instAddNat = _init_l_instAddNat();
--- a/stage0/stdlib/Lean/Delaborator.c
+++ b/stage0/stdlib/Lean/Delaborator.c
@ -25,6 +25,7 @@ lean_object* l_Lean_Delaborator_delabseqRight___closed__1;
 extern lean_object* l_Lean_Name_toString___closed__1;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_8830____closed__4;
 lean_object* l_Lean_Delaborator_delabDoElems___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Delaborator_delabZero___closed__1;
 lean_object* l_Lean_Delaborator_delabConst___lambda__1___closed__3;
 lean_object* l_Lean_Delaborator_delabDoElems___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_delabEq(lean_object*);
@ -37,8 +38,10 @@ lean_object* l_Lean_Delaborator_withProj(lean_object*);
 lean_object* l_Lean_Delaborator_delabBind(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Level_quote___closed__6;
 extern lean_object* l_Lean_Meta_Match_Pattern_toExpr_visit___closed__2;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__27;
 size_t l_USize_add(size_t, size_t);
 extern lean_object* l_Lean_fieldIdxKind;
+lean_object* l___regBuiltin_Lean_Delaborator_delabZero(lean_object*);
 lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_delabBind___closed__2;
 lean_object* l_Lean_Delaborator_delabFComp___lambda__1___closed__2;
@ -72,12 +75,14 @@ extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3331____closed_
 lean_object* l_Lean_Delaborator_delabseqRight___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabProd___closed__1;
 lean_object* l_Lean_Delaborator_annotatePos(lean_object*, lean_object*);
+lean_object* l___regBuiltin_Lean_Delaborator_delabZero___closed__3;
 lean_object* l_Lean_Delaborator_delabMVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withLetDecl___at_Lean_Delaborator_delabLetE___spec__1(lean_object*);
 lean_object* l_Lean_Delaborator_delabAdd___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_addParenHeuristic___closed__2;
 lean_object* l___private_Lean_Delaborator_0__Lean_Delaborator_shouldGroupWithNext_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabLE___lambda__1___closed__4;
+lean_object* l___regBuiltin_Lean_Delaborator_delabZero___closed__1;
 extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_11506____closed__7;
 lean_object* l___regBuiltin_Lean_Delaborator_delabConsList___closed__1;
 extern lean_object* l_Lean_withIncRecDepth___rarg___lambda__2___closed__2;
@ -110,6 +115,7 @@ lean_object* l_Lean_Delaborator_AppMatchState_moreArgs___default;
 lean_object* l_Array_zipWithAux___at_Lean_Delaborator_delabAppMatch___spec__4___closed__1;
 lean_object* l_Lean_Delaborator_delabAnd___closed__1;
 lean_object* l___private_Lean_Delaborator_0__Lean_Delaborator_shouldGroupWithNext_match__1(lean_object*);
+lean_object* l___regBuiltin_Lean_Delaborator_delabZero___closed__2;
 lean_object* l_Lean_Meta_inferType___at___private_Lean_Delaborator_0__Lean_Delaborator_delabPatterns___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabMod___lambda__1___closed__2;
 lean_object* l_Lean_Delaborator_delabAppImplicit_match__1(lean_object*);
@ -199,7 +205,6 @@ lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalDeclImp___rarg(le
 lean_object* l_Lean_Delaborator_delabAppMatch___lambda__3___closed__2;
 extern lean_object* l_myMacro____x40_Init_Core___hyg_715____closed__4;
 lean_object* l_Lean_getPPNotation___boxed(lean_object*);
-extern lean_object* l___kind_term____x40_Init_NotationExtra___hyg_3345____closed__2;
 lean_object* l_Lean_Delaborator_delabEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Level_quote___lambda__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t l_USize_sub(size_t, size_t);
@ -273,6 +278,7 @@ uint8_t l_Lean_Delaborator_hasIdent(lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabCoe___closed__1;
 lean_object* l_Lean_Delaborator_withMDataExpr___rarg___closed__2;
 lean_object* l_Lean_Delaborator_delabEquiv___closed__1;
+extern lean_object* l___kind_term____x40_Init_NotationExtra___hyg_2577____closed__2;
 extern lean_object* l___kind_term____x40_Init_Notation___hyg_2514____closed__1;
 lean_object* l_Lean_Delaborator_delabLit_match__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabCons___closed__1;
@ -327,6 +333,7 @@ extern lean_object* l_myMacro____x40_Init_Control_Basic___hyg_75____closed__6;
 lean_object* l_Lean_Delaborator_liftMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Level_getOffsetAux(lean_object*, lean_object*);
 extern lean_object* l___kind_stx____x40_Init_Notation___hyg_7296____closed__8;
+extern lean_object* l_Lean_Meta_evalNat_visit___closed__10;
 lean_object* l_Lean_Delaborator_delabListToArray___lambda__1___closed__1;
 lean_object* l_Lean_Delaborator_delabAnd___lambda__1___closed__1;
 lean_object* l_Lean_Level_quote_match__1(lean_object*);
@ -342,12 +349,12 @@ lean_object* l_Lean_Delaborator_annotateCurPos___boxed(lean_object*, lean_object
 lean_object* l___regBuiltin_Lean_Delaborator_delabCons___closed__2;
 lean_object* l___regBuiltin_Lean_Delaborator_delabAdd___closed__3;
 lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1019____spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Delaborator_delabZero___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t l_USize_shiftRight(size_t, size_t);
 lean_object* l_Lean_Delaborator_delabDoElems_match__1(lean_object*);
 lean_object* l_Lean_Level_quote___lambda__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_getPPFullNames___boxed(lean_object*);
 lean_object* l_Lean_Delaborator_delabLam_match__1(lean_object*);
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__39;
 lean_object* l_Lean_Delaborator_delabBNot___lambda__1___closed__3;
 lean_object* l___regBuiltin_Lean_Delaborator_delabEquiv___closed__1;
 lean_object* l_Lean_Delaborator_getPPOption_match__1(lean_object*);
@ -357,6 +364,7 @@ lean_object* l_Lean_Delaborator_delabBind___lambda__1(uint8_t, lean_object*, lea
 lean_object* l_Lean_Delaborator_delabAppMatch_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_delabLetE___closed__1;
 lean_object* l_Lean_Delaborator_delabAdd___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 lean_object* l___regBuiltin_Lean_Delaborator_delabOfNat(lean_object*);
 lean_object* l_Lean_Delaborator_delabDoElems___lambda__4___closed__4;
 lean_object* l___regBuiltin_Lean_Delaborator_delabBEq___closed__1;
@ -455,11 +463,13 @@ lean_object* l_Lean_Delaborator_delabDoElems___lambda__1(lean_object*, lean_obje
 uint8_t l_Lean_getPPFullNames(lean_object*);
 lean_object* l_Lean_Delaborator_delabAppend___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Level_instQuoteLevel___closed__1;
+lean_object* l_Lean_Delaborator_delabOne___lambda__1___closed__2;
 lean_object* l_Lean_Delaborator_delabAppImplicit___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_2714____closed__4;
 lean_object* l_Lean_Delaborator_delabNot___lambda__1___closed__4;
 lean_object* l___private_Lean_Delaborator_0__Lean_Delaborator_skippingBinders_match__1(lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_7791____closed__7;
+lean_object* l_Lean_Delaborator_delabOne___lambda__1___closed__1;
 lean_object* l___regBuiltin_Lean_Delaborator_delabAppend(lean_object*);
 lean_object* l_Lean_Meta_inferType___at___private_Lean_Delaborator_0__Lean_Delaborator_delabPatterns___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabMData___closed__1;
@ -495,6 +505,7 @@ extern lean_object* l___kind_term____x40_Init_Notation___hyg_1681____closed__1;
 lean_object* l_Lean_Delaborator_delabConst___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_delabListToArray___closed__2;
 lean_object* l_Lean_Delaborator_delabDoElems(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Delaborator_delabOne___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabForall___lambda__1___closed__4;
 extern lean_object* l___kind_term____x40_Init_Data_Array_Basic___hyg_3284____closed__7;
 lean_object* l_Lean_Delaborator_delabAppExplicit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -665,7 +676,6 @@ size_t l_Lean_Name_hash(lean_object*);
 lean_object* l_Lean_Delaborator_delab___closed__4;
 extern lean_object* l___kind_term____x40_Init_Notation___hyg_4329____closed__1;
 uint8_t l_Array_anyMUnsafe_any___at_Lean_Delaborator_delabForall___spec__3(lean_object*, lean_object*, size_t, size_t);
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
 lean_object* l___regBuiltin_Lean_Delaborator_delabDo___closed__1;
 lean_object* l_Lean_Delaborator_delabAdd(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_repr(lean_object*);
@ -673,6 +683,7 @@ extern lean_object* l___kind_term____x40_Init_Notation___hyg_5505____closed__1;
 lean_object* l___private_Lean_Delaborator_0__Lean_Delaborator_delabBinders_match__2___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabAdd___closed__1;
 lean_object* l_Lean_Delaborator_delabMul(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Delaborator_delabZero___closed__2;
 lean_object* l_Lean_Delaborator_delabNamedPattern(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_LocalDecl_binderInfo(lean_object*);
 lean_object* l_Lean_Delaborator_delabOr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -714,6 +725,7 @@ lean_object* l_Lean_Delaborator_delabIff(lean_object*, lean_object*, lean_object
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_8830____closed__18;
 uint8_t l_Lean_getPPStructureInstanceType(lean_object*);
 lean_object* l_Lean_Delaborator_delabAppMatch___lambda__3___closed__10;
+lean_object* l_Lean_Delaborator_delabOne___closed__2;
 lean_object* l_Lean_getStructureFields(lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_getParamKinds_match__1___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Expr_ctorName___closed__3;
@ -737,12 +749,13 @@ lean_object* l_Lean_Delaborator_instInhabitedDelabM___closed__1;
 lean_object* l___regBuiltin_Lean_Delaborator_delabMul(lean_object*);
 lean_object* l_Lean_Delaborator_AppMatchState_rhss___default;
 lean_object* l_Lean_Delaborator_delabForall___closed__1;
+lean_object* l_Lean_Delaborator_delabOne___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_protectedExt;
 lean_object* l_Lean_Delaborator_delabPrefixOp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Expr_isCharLit___closed__3;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_38____closed__5;
 lean_object* l_Lean_Delaborator_failure___rarg___closed__1;
-lean_object* l_Lean_initFn____x40_Lean_Delaborator___hyg_11463_(lean_object*);
+lean_object* l_Lean_initFn____x40_Lean_Delaborator___hyg_11519_(lean_object*);
 lean_object* l_Lean_initFn____x40_Lean_Delaborator___hyg_574_(lean_object*);
 lean_object* l_Lean_Delaborator_withAppFn_match__1(lean_object*);
 lean_object* l_Lean_Delaborator_delabProd___lambda__1___closed__1;
@ -792,10 +805,12 @@ extern lean_object* l_Lean_mkSimpleThunk___closed__1;
 lean_object* l_Lean_Delaborator_delabLam___lambda__3___closed__4;
 lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Init_NotationExtra_0__Lean_mkHintBody___closed__2;
+lean_object* l___regBuiltin_Lean_Delaborator_delabOne(lean_object*);
 extern lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
 uint8_t l_Lean_Expr_isConst(lean_object*);
 lean_object* l___private_Lean_Delaborator_0__Lean_Delaborator_delabBinders_match__2(lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_5204____closed__4;
+lean_object* l___regBuiltin_Lean_Delaborator_delabOne___closed__2;
 extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_576____closed__8;
 lean_object* l___regBuiltin_Lean_Delaborator_delabMapRev___closed__1;
 lean_object* l_Lean_Delaborator_initFn____x40_Lean_Delaborator___hyg_626____closed__2;
@ -952,6 +967,7 @@ lean_object* l_Lean_Delaborator_instAlternativeDelabM___closed__3;
 lean_object* l_Lean_Delaborator_delabGT___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Delaborator_0__Lean_Delaborator_unresolveOpenDecls(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabSort___closed__2;
+lean_object* l_Lean_Delaborator_delabOne(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Syntax_mkApp___closed__1;
 lean_object* l_Lean_Meta_getMatcherInfo_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_fmt___at_Lean_ppExpr___spec__4(lean_object*);
@ -990,6 +1006,7 @@ lean_object* l_Lean_Delaborator_getPPOption_match__1___rarg(lean_object*, lean_o
 lean_object* l_Lean_Delaborator_mkDelabAttribute___closed__2;
 lean_object* l_Lean_Delaborator_delabLetE(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getLocalDecl___at_Lean_Meta_getFVarLocalDecl___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Meta_evalNat_visit___closed__8;
 extern lean_object* l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__1;
 lean_object* l_Lean_Delaborator_delabDo___lambda__1___closed__5;
 lean_object* l_Lean_Expr_bindingName_x21(lean_object*);
@ -1036,7 +1053,6 @@ lean_object* l_Lean_Meta_throwUnknownFVar___rarg(lean_object*, lean_object*, lea
 lean_object* l_Lean_Delaborator_instAlternativeDelabM;
 lean_object* l_Lean_Delaborator_delabAppImplicit___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___kind_term____x40_Init_Notation___hyg_2184____closed__1;
-extern lean_object* l_Lean_Meta_evalNat_visit___closed__1;
 lean_object* l_Lean_Delaborator_delabBVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_BinderInfo_isExplicit(uint8_t);
 lean_object* l_Lean_Delaborator_instMonadQuotationDelabM___closed__4;
@ -1065,6 +1081,7 @@ lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_instantiateForallAux(lean_
 lean_object* l_Lean_Delaborator_delabAppExplicit___lambda__2___closed__2;
 lean_object* lean_panic_fn(lean_object*, lean_object*);
 lean_object* l_Lean_getPPUniverses___closed__2;
+lean_object* l_Lean_Delaborator_delabZero(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabLT___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg___closed__1;
 extern lean_object* l_Lean_getSanitizeNames___closed__1;
@ -1225,6 +1242,7 @@ lean_object* l___regBuiltin_Lean_Delaborator_delabEquiv___closed__2;
 lean_object* l___regBuiltin_Lean_Delaborator_delabAppend___closed__3;
 lean_object* l___regBuiltin_Lean_Delaborator_delabSort___closed__1;
 lean_object* l___regBuiltin_Lean_Delaborator_delabMVar___closed__1;
+extern lean_object* l_Lean_Meta_evalNat_visit___closed__2;
 lean_object* l_Lean_Delaborator_delabAttribute;
 uint8_t l_Lean_TagDeclarationExtension_isTagged(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabConst___closed__2;
@ -1270,6 +1288,7 @@ lean_object* l_List_forIn_loop___at_Lean_Delaborator_delabMData___spec__3___lamb
 lean_object* l_Lean_Delaborator_delabBNot___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_delabProj(lean_object*);
 lean_object* l_Lean_Delaborator_delabBNot___lambda__1___closed__4;
+lean_object* l_Lean_Delaborator_delabZero___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_syntax_ident(lean_object*);
 lean_object* l_Lean_Delaborator_delabSort___closed__1;
 lean_object* l___regBuiltin_Lean_Delaborator_delabLetE(lean_object*);
@ -1305,6 +1324,7 @@ lean_object* l_Lean_Delaborator_delabAppExplicit_match__3___rarg(lean_object*, l
 lean_object* l_Lean_Delaborator_descend___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_getAppFn(lean_object*);
 lean_object* l_Lean_Delaborator_delabLit___closed__1;
+lean_object* l___regBuiltin_Lean_Delaborator_delabOne___closed__1;
 lean_object* l_Lean_Delaborator_delabFVar___closed__1;
 extern lean_object* l_Lean_Meta_CheckAssignment_checkFVar___closed__1;
 lean_object* l_Lean_Delaborator_mkDelabAttribute___closed__11;
@ -1321,9 +1341,11 @@ lean_object* l_Lean_Delaborator_delabBEq___lambda__1(uint8_t, lean_object*, lean
 lean_object* l_Lean_Delaborator_delabEquiv___lambda__1___closed__1;
 lean_object* l_Lean_Delaborator_delabLam___lambda__3___closed__3;
 lean_object* l___regBuiltin_Lean_Delaborator_delabseqRight___closed__3;
+extern lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Environment_displayStats___spec__8___lambda__1___closed__1;
 lean_object* l_Lean_Delaborator_delabAppend___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabGE___lambda__1___closed__4;
 lean_object* l_Lean_Delaborator_delabMapRev___lambda__1___closed__2;
+lean_object* l_Lean_Delaborator_delabZero___lambda__1___closed__1;
 lean_object* l_Lean_Delaborator_delabDoElems_delabAndRet___closed__1;
 lean_object* l_Lean_Delaborator_delabOrElse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
@ -1349,6 +1371,7 @@ lean_object* l_Lean_Delaborator_delabAppMatch___lambda__3___boxed(lean_object*,
 lean_object* l_Lean_Delaborator_delabSub___closed__1;
 lean_object* lean_usize_to_nat(size_t);
 lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLetDeclImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Delaborator_delabOne___closed__1;
 lean_object* l_Lean_Delaborator_delabAppImplicit___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_withAppFn_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabAndThen___lambda__1___closed__2;
@ -1411,6 +1434,7 @@ lean_object* l_Lean_Level_quote___closed__4;
 lean_object* l_Lean_Delaborator_delabDoElems___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabConst_match__1___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_4032____closed__1;
+extern lean_object* l_Lean_Meta_evalNat_match__1___rarg___closed__1;
 extern lean_object* l___regBuiltin_Lean_Elab_Term_elabSyntheticHole___closed__1;
 lean_object* l_Lean_Delaborator_delabDoElems___lambda__1___closed__3;
 lean_object* l_Lean_Delaborator_delabConst___closed__3;
@ -1430,6 +1454,7 @@ extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Subarray___hyg_1011__
 lean_object* l_Lean_getPPPrivateNames___boxed(lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_delabModN(lean_object*);
 lean_object* l_Lean_Delaborator_delabSub___lambda__1___closed__1;
+lean_object* l___regBuiltin_Lean_Delaborator_delabOne___closed__3;
 lean_object* l_Lean_Delaborator_delabNil___closed__1;
 lean_object* l_Lean_Delaborator_delabMapRev___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabAppMatch___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1443,6 +1468,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_1378____closed__4;
 lean_object* l_Lean_throwError___at_Lean_Delaborator_delabAppMatch___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_getExprKind_match__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_getPPStructureProjections___boxed(lean_object*);
+extern lean_object* l_Lean_Meta_evalNat_visit___closed__5;
 lean_object* l___regBuiltin_Lean_Delaborator_delabNot___closed__2;
 lean_object* l___regBuiltin_Lean_Delaborator_delabOfNat___closed__2;
 lean_object* l_Lean_Delaborator_getExprKind_match__2___rarg(lean_object*, lean_object*, lean_object*);
@ -1886,7 +1912,7 @@ lean_object* l_Lean_Level_quote___lambda__9(lean_object* x_1, lean_object* x_2,
 _start:
 {
 lean_object* x_4; lean_object* x_5; 
-x_4 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__39;
+x_4 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__35;
 x_5 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_5, 0, x_4);
 lean_ctor_set(x_5, 1, x_3);
@ -3904,7 +3930,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__31;
+x_2 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__27;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@ -12121,9 +12147,9 @@ x_29 = l_Lean_nullKind___closed__2;
 x_30 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_30, 0, x_29);
 lean_ctor_set(x_30, 1, x_28);
-x_31 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__35;
+x_31 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__31;
 x_32 = lean_array_push(x_31, x_30);
-x_33 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
+x_33 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 x_34 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_34, 0, x_33);
 lean_ctor_set(x_34, 1, x_32);
@ -12171,9 +12197,9 @@ x_50 = l_Lean_nullKind___closed__2;
 x_51 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_51, 0, x_50);
 lean_ctor_set(x_51, 1, x_49);
-x_52 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__35;
+x_52 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__31;
 x_53 = lean_array_push(x_52, x_51);
-x_54 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
+x_54 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 x_55 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_55, 0, x_54);
 lean_ctor_set(x_55, 1, x_53);
@ -12230,9 +12256,9 @@ x_74 = l_Lean_nullKind___closed__2;
 x_75 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_75, 0, x_74);
 lean_ctor_set(x_75, 1, x_73);
-x_76 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__35;
+x_76 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__31;
 x_77 = lean_array_push(x_76, x_75);
-x_78 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
+x_78 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 x_79 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_79, 0, x_78);
 lean_ctor_set(x_79, 1, x_77);
@ -12280,9 +12306,9 @@ x_95 = l_Lean_nullKind___closed__2;
 x_96 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_96, 0, x_95);
 lean_ctor_set(x_96, 1, x_94);
-x_97 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__35;
+x_97 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__31;
 x_98 = lean_array_push(x_97, x_96);
-x_99 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
+x_99 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 x_100 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_100, 0, x_99);
 lean_ctor_set(x_100, 1, x_98);
@ -25735,7 +25761,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Delaborator_getExprKind___closed__5;
-x_2 = l_Lean_Meta_evalNat_visit___closed__1;
+x_2 = l_Lean_Meta_evalNat_visit___closed__5;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@ -25769,6 +25795,289 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
+static lean_object* _init_l_Lean_Delaborator_delabOne___lambda__1___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = lean_unsigned_to_nat(1u);
+x_2 = l_Nat_repr(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Delaborator_delabOne___lambda__1___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_numLitKind;
+x_2 = l_Lean_Delaborator_delabOne___lambda__1___closed__1;
+x_3 = l_Lean_instInhabitedSourceInfo___closed__1;
+x_4 = l_Lean_Syntax_mkLit(x_1, x_2, x_3);
+return x_4;
+}
+}
+lean_object* l_Lean_Delaborator_delabOne___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; 
+x_8 = lean_unsigned_to_nat(0u);
+x_9 = l_Lean_Expr_getAppNumArgsAux(x_1, x_8);
+x_10 = lean_unsigned_to_nat(2u);
+x_11 = lean_nat_dec_eq(x_9, x_10);
+lean_dec(x_9);
+if (x_11 == 0)
+{
+lean_object* x_12; uint8_t x_13; 
+x_12 = l_Lean_Delaborator_failure___rarg(x_7);
+x_13 = !lean_is_exclusive(x_12);
+if (x_13 == 0)
+{
+return x_12;
+}
+else
+{
+lean_object* x_14; lean_object* x_15; lean_object* x_16; 
+x_14 = lean_ctor_get(x_12, 0);
+x_15 = lean_ctor_get(x_12, 1);
+lean_inc(x_15);
+lean_inc(x_14);
+lean_dec(x_12);
+x_16 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_16, 0, x_14);
+lean_ctor_set(x_16, 1, x_15);
+return x_16;
+}
+}
+else
+{
+lean_object* x_17; lean_object* x_18; 
+x_17 = l_Lean_Delaborator_delabOne___lambda__1___closed__2;
+x_18 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_18, 0, x_17);
+lean_ctor_set(x_18, 1, x_7);
+return x_18;
+}
+}
+}
+static lean_object* _init_l_Lean_Delaborator_delabOne___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Delaborator_delabOne___lambda__1___boxed), 7, 0);
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_Delaborator_delabOne___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Delaborator_delabAppExplicit___closed__1;
+x_2 = l_Lean_Delaborator_delabOne___closed__1;
+x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Delaborator_delabAppExplicit___spec__2___rarg), 8, 2);
+lean_closure_set(x_3, 0, x_1);
+lean_closure_set(x_3, 1, x_2);
+return x_3;
+}
+}
+lean_object* l_Lean_Delaborator_delabOne(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_7 = l_Lean_Delaborator_delabOfNat___closed__3;
+x_8 = l_Lean_Delaborator_delabOne___closed__2;
+x_9 = l_Lean_Delaborator_whenPPOption(x_7, x_8, x_1, x_2, x_3, x_4, x_5, x_6);
+return x_9;
+}
+}
+lean_object* l_Lean_Delaborator_delabOne___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; 
+x_8 = l_Lean_Delaborator_delabOne___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_8;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOne___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Delaborator_getExprKind___closed__5;
+x_2 = l_Lean_Meta_evalNat_visit___closed__8;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOne___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l___regBuiltin_Lean_Delaborator_delabOne___closed__1;
+x_2 = l_Lean_Meta_evalNat_visit___closed__10;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOne___closed__3() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Delaborator_delabOne), 6, 0);
+return x_1;
+}
+}
+lean_object* l___regBuiltin_Lean_Delaborator_delabOne(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_Delaborator_delabAttribute;
+x_3 = l___regBuiltin_Lean_Delaborator_delabOne___closed__2;
+x_4 = l___regBuiltin_Lean_Delaborator_delabOne___closed__3;
+x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
+static lean_object* _init_l_Lean_Delaborator_delabZero___lambda__1___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_numLitKind;
+x_2 = l_Array_foldlMUnsafe_fold___at_Lean_Environment_displayStats___spec__8___lambda__1___closed__1;
+x_3 = l_Lean_instInhabitedSourceInfo___closed__1;
+x_4 = l_Lean_Syntax_mkLit(x_1, x_2, x_3);
+return x_4;
+}
+}
+lean_object* l_Lean_Delaborator_delabZero___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; 
+x_8 = lean_unsigned_to_nat(0u);
+x_9 = l_Lean_Expr_getAppNumArgsAux(x_1, x_8);
+x_10 = lean_unsigned_to_nat(2u);
+x_11 = lean_nat_dec_eq(x_9, x_10);
+lean_dec(x_9);
+if (x_11 == 0)
+{
+lean_object* x_12; uint8_t x_13; 
+x_12 = l_Lean_Delaborator_failure___rarg(x_7);
+x_13 = !lean_is_exclusive(x_12);
+if (x_13 == 0)
+{
+return x_12;
+}
+else
+{
+lean_object* x_14; lean_object* x_15; lean_object* x_16; 
+x_14 = lean_ctor_get(x_12, 0);
+x_15 = lean_ctor_get(x_12, 1);
+lean_inc(x_15);
+lean_inc(x_14);
+lean_dec(x_12);
+x_16 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_16, 0, x_14);
+lean_ctor_set(x_16, 1, x_15);
+return x_16;
+}
+}
+else
+{
+lean_object* x_17; lean_object* x_18; 
+x_17 = l_Lean_Delaborator_delabZero___lambda__1___closed__1;
+x_18 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_18, 0, x_17);
+lean_ctor_set(x_18, 1, x_7);
+return x_18;
+}
+}
+}
+static lean_object* _init_l_Lean_Delaborator_delabZero___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Delaborator_delabZero___lambda__1___boxed), 7, 0);
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_Delaborator_delabZero___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Delaborator_delabAppExplicit___closed__1;
+x_2 = l_Lean_Delaborator_delabZero___closed__1;
+x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Delaborator_delabAppExplicit___spec__2___rarg), 8, 2);
+lean_closure_set(x_3, 0, x_1);
+lean_closure_set(x_3, 1, x_2);
+return x_3;
+}
+}
+lean_object* l_Lean_Delaborator_delabZero(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_7 = l_Lean_Delaborator_delabOfNat___closed__3;
+x_8 = l_Lean_Delaborator_delabZero___closed__2;
+x_9 = l_Lean_Delaborator_whenPPOption(x_7, x_8, x_1, x_2, x_3, x_4, x_5, x_6);
+return x_9;
+}
+}
+lean_object* l_Lean_Delaborator_delabZero___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; 
+x_8 = l_Lean_Delaborator_delabZero___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_8;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabZero___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Delaborator_getExprKind___closed__5;
+x_2 = l_Lean_Meta_evalNat_visit___closed__2;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabZero___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l___regBuiltin_Lean_Delaborator_delabZero___closed__1;
+x_2 = l_Lean_Meta_evalNat_match__1___rarg___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabZero___closed__3() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Delaborator_delabZero), 6, 0);
+return x_1;
+}
+}
+lean_object* l___regBuiltin_Lean_Delaborator_delabZero(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_Delaborator_delabAttribute;
+x_3 = l___regBuiltin_Lean_Delaborator_delabZero___closed__2;
+x_4 = l___regBuiltin_Lean_Delaborator_delabZero___closed__3;
+x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
 lean_object* l_Lean_Delaborator_delabProj_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@ -25819,7 +26128,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_Delaborator_withAppFn___rarg___closed__2;
 x_2 = l_Lean_Delaborator_delabProj___closed__1;
-x_3 = lean_unsigned_to_nat(615u);
+x_3 = lean_unsigned_to_nat(629u);
 x_4 = lean_unsigned_to_nat(38u);
 x_5 = l_Lean_Syntax_strLitToAtom___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -28990,7 +29299,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_instInhabitedSourceInfo___closed__1;
-x_2 = l___kind_term____x40_Init_NotationExtra___hyg_3345____closed__2;
+x_2 = l___kind_term____x40_Init_NotationExtra___hyg_2577____closed__2;
 x_3 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@ -34873,7 +35182,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_Delaborator_withAppFn___rarg___closed__2;
 x_2 = l_Lean_Delaborator_delabDoElems___closed__1;
-x_3 = lean_unsigned_to_nat(819u);
+x_3 = lean_unsigned_to_nat(833u);
 x_4 = lean_unsigned_to_nat(40u);
 x_5 = l_Lean_Syntax_strLitToAtom___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -35543,7 +35852,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_Delaborator_withAppFn___rarg___closed__2;
 x_2 = l_Lean_delab___closed__1;
-x_3 = lean_unsigned_to_nat(849u);
+x_3 = lean_unsigned_to_nat(863u);
 x_4 = lean_unsigned_to_nat(14u);
 x_5 = l_Lean_Syntax_strLitToAtom___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -35799,7 +36108,7 @@ goto block_39;
 }
 }
 }
-lean_object* l_Lean_initFn____x40_Lean_Delaborator___hyg_11463_(lean_object* x_1) {
+lean_object* l_Lean_initFn____x40_Lean_Delaborator___hyg_11519_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
@ -36328,6 +36637,38 @@ lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3);
 res = l___regBuiltin_Lean_Delaborator_delabOfNat(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l_Lean_Delaborator_delabOne___lambda__1___closed__1 = _init_l_Lean_Delaborator_delabOne___lambda__1___closed__1();
+lean_mark_persistent(l_Lean_Delaborator_delabOne___lambda__1___closed__1);
+l_Lean_Delaborator_delabOne___lambda__1___closed__2 = _init_l_Lean_Delaborator_delabOne___lambda__1___closed__2();
+lean_mark_persistent(l_Lean_Delaborator_delabOne___lambda__1___closed__2);
+l_Lean_Delaborator_delabOne___closed__1 = _init_l_Lean_Delaborator_delabOne___closed__1();
+lean_mark_persistent(l_Lean_Delaborator_delabOne___closed__1);
+l_Lean_Delaborator_delabOne___closed__2 = _init_l_Lean_Delaborator_delabOne___closed__2();
+lean_mark_persistent(l_Lean_Delaborator_delabOne___closed__2);
+l___regBuiltin_Lean_Delaborator_delabOne___closed__1 = _init_l___regBuiltin_Lean_Delaborator_delabOne___closed__1();
+lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabOne___closed__1);
+l___regBuiltin_Lean_Delaborator_delabOne___closed__2 = _init_l___regBuiltin_Lean_Delaborator_delabOne___closed__2();
+lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabOne___closed__2);
+l___regBuiltin_Lean_Delaborator_delabOne___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabOne___closed__3();
+lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabOne___closed__3);
+res = l___regBuiltin_Lean_Delaborator_delabOne(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_Lean_Delaborator_delabZero___lambda__1___closed__1 = _init_l_Lean_Delaborator_delabZero___lambda__1___closed__1();
+lean_mark_persistent(l_Lean_Delaborator_delabZero___lambda__1___closed__1);
+l_Lean_Delaborator_delabZero___closed__1 = _init_l_Lean_Delaborator_delabZero___closed__1();
+lean_mark_persistent(l_Lean_Delaborator_delabZero___closed__1);
+l_Lean_Delaborator_delabZero___closed__2 = _init_l_Lean_Delaborator_delabZero___closed__2();
+lean_mark_persistent(l_Lean_Delaborator_delabZero___closed__2);
+l___regBuiltin_Lean_Delaborator_delabZero___closed__1 = _init_l___regBuiltin_Lean_Delaborator_delabZero___closed__1();
+lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabZero___closed__1);
+l___regBuiltin_Lean_Delaborator_delabZero___closed__2 = _init_l___regBuiltin_Lean_Delaborator_delabZero___closed__2();
+lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabZero___closed__2);
+l___regBuiltin_Lean_Delaborator_delabZero___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabZero___closed__3();
+lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabZero___closed__3);
+res = l___regBuiltin_Lean_Delaborator_delabZero(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 l_Lean_Delaborator_delabProj___closed__1 = _init_l_Lean_Delaborator_delabProj___closed__1();
 lean_mark_persistent(l_Lean_Delaborator_delabProj___closed__1);
 l_Lean_Delaborator_delabProj___closed__2 = _init_l_Lean_Delaborator_delabProj___closed__2();
@ -37087,7 +37428,7 @@ l_Lean_delab___closed__6 = _init_l_Lean_delab___closed__6();
 lean_mark_persistent(l_Lean_delab___closed__6);
 l_Lean_delab___closed__7 = _init_l_Lean_delab___closed__7();
 lean_mark_persistent(l_Lean_delab___closed__7);
-res = l_Lean_initFn____x40_Lean_Delaborator___hyg_11463_(lean_io_mk_world());
+res = l_Lean_initFn____x40_Lean_Delaborator___hyg_11519_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
--- a/stage0/stdlib/Lean/Elab/Binders.c
+++ b/stage0/stdlib/Lean/Elab/Binders.c
@ -81,6 +81,7 @@ lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandOptIdent___cl
 lean_object* l_Lean_Meta_withoutPostponingUniverseConstraintsImp___at_Lean_Elab_Term_elabBinders___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandFunBinders___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Array_empty___closed__1;
+extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2849____closed__10;
 lean_object* l_Lean_Elab_Term_declareTacticSyntax___closed__1;
 extern lean_object* l_Lean_Parser_Tactic_let___closed__2;
 lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___closed__12;
@ -400,7 +401,6 @@ lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__1___closed__2;
 extern lean_object* l_Lean_Parser_Tactic___kind_tactic____x40_Init_Notation___hyg_11224____closed__4;
 lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_expandFunBinders_loop___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkExplicitBinder(lean_object*, lean_object*);
-extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_3617____closed__10;
 extern lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_checkTypesAndAssign___closed__8;
 lean_object* l_Lean_Elab_Term_adaptExpander(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_setPostponed___at_Lean_Elab_Term_elabBinders___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -17588,7 +17588,7 @@ x_69 = l_Lean_nullKind___closed__2;
 x_70 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_70, 0, x_69);
 lean_ctor_set(x_70, 1, x_68);
-x_71 = l_myMacro____x40_Init_NotationExtra___hyg_3617____closed__10;
+x_71 = l_myMacro____x40_Init_NotationExtra___hyg_2849____closed__10;
 x_72 = lean_array_push(x_71, x_70);
 x_73 = l_Lean_Parser_Tactic_intro___closed__4;
 x_74 = lean_alloc_ctor(1, 2, 0);
@ -17623,7 +17623,7 @@ x_87 = l_Lean_nullKind___closed__2;
 x_88 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_88, 0, x_87);
 lean_ctor_set(x_88, 1, x_86);
-x_89 = l_myMacro____x40_Init_NotationExtra___hyg_3617____closed__10;
+x_89 = l_myMacro____x40_Init_NotationExtra___hyg_2849____closed__10;
 x_90 = lean_array_push(x_89, x_88);
 x_91 = l_Lean_Parser_Tactic_intro___closed__4;
 x_92 = lean_alloc_ctor(1, 2, 0);
@ -17756,7 +17756,7 @@ x_143 = l_Lean_nullKind___closed__2;
 x_144 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_144, 0, x_143);
 lean_ctor_set(x_144, 1, x_142);
-x_145 = l_myMacro____x40_Init_NotationExtra___hyg_3617____closed__10;
+x_145 = l_myMacro____x40_Init_NotationExtra___hyg_2849____closed__10;
 x_146 = lean_array_push(x_145, x_144);
 x_147 = l_Lean_Parser_Tactic_intro___closed__4;
 x_148 = lean_alloc_ctor(1, 2, 0);
--- a/stage0/stdlib/Lean/Elab/Declaration.c
+++ b/stage0/stdlib/Lean/Elab/Declaration.c
--- a/stage0/stdlib/Lean/Elab/DefView.c
+++ b/stage0/stdlib/Lean/Elab/DefView.c
@ -40,6 +40,7 @@ lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___closed__2;
 lean_object* l_Lean_Elab_Command_MkInstanceName_collect(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandOptIdent___closed__1;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__45;
 lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___regBuiltin_Lean_Elab_Term_elabDepArrow___closed__2;
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
@ -67,6 +68,7 @@ extern lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_272____c
 extern lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_272____closed__2;
 lean_object* l_Lean_Elab_Command_MkInstanceName_mkFreshInstanceName___rarg___boxed(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_DefView_0__Lean_Elab_Command_MkInstanceName_kindReplacements___closed__2;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 lean_object* lean_string_utf8_byte_size(lean_object*);
 lean_object* l_Lean_Elab_DefKind_isDefOrAbbrevOrOpaque_match__1(lean_object*);
 lean_object* l_Lean_Elab_Command_mkDefViewOfConstant(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -75,7 +77,6 @@ uint8_t l_Lean_Elab_DefKind_isExample(uint8_t);
 lean_object* l_Lean_Elab_Command_mkDefView___closed__3;
 uint8_t l_USize_decLt(size_t, size_t);
 extern lean_object* l_Lean_Compiler_initFn____x40_Lean_Compiler_InlineAttrs___hyg_54____closed__4;
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_MkInstanceName_collect___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_mkDefViewOfAbbrev___closed__2;
@ -109,7 +110,6 @@ uint8_t l_Char_isLower(uint32_t);
 lean_object* l_Lean_Elab_Command_isDefLike___boxed(lean_object*);
 lean_object* l_Std_RBNode_insert___at___private_Lean_Elab_DefView_0__Lean_Elab_Command_MkInstanceName_kindReplacements___spec__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBMap_ofList___at___private_Lean_Elab_DefView_0__Lean_Elab_Command_MkInstanceName_kindReplacements___spec__1(lean_object*);
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
 lean_object* l_Lean_Elab_Command_MkInstanceName_collect_match__1___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__20;
 lean_object* lean_st_mk_ref(lean_object*, lean_object*);
@ -128,7 +128,6 @@ extern lean_object* l_Lean_Elab_Term_elabForall___closed__2;
 uint32_t lean_string_utf8_get(lean_object*, lean_object*);
 extern lean_object* l___regBuiltin_Lean_Elab_Term_elabProp___closed__2;
 lean_object* l___private_Lean_Elab_DefView_0__Lean_Elab_Command_MkInstanceName_kindReplacements___closed__16;
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__49;
 lean_object* l_Lean_Elab_Command_MkInstanceName_append___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_MkInstanceName_main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Elab_Command_isDefLike(lean_object*);
@ -157,6 +156,7 @@ lean_object* l_Lean_Elab_Command_mkDefViewOfInstance_match__2(lean_object*);
 extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_839____closed__1;
 lean_object* l_Lean_Elab_Command_getCurrMacroScope(lean_object*, lean_object*, lean_object*);
 uint8_t l_Std_RBNode_isRed___rarg(lean_object*);
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__29;
 lean_object* l_Lean_Name_append(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_mkDefViewOfConstant_match__1(lean_object*);
 lean_object* l_Lean_Syntax_getKind(lean_object*);
@ -3239,8 +3239,8 @@ static lean_object* _init_l___private_Lean_Elab_DefView_0__Lean_Elab_Command_MkI
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
-x_2 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
+x_2 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__29;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@ -4808,7 +4808,7 @@ x_27 = l_Lean_mkAtomFrom(x_2, x_26);
 x_28 = l_Lean_Syntax_mkApp___closed__1;
 x_29 = lean_array_push(x_28, x_27);
 x_30 = lean_array_push(x_29, x_25);
-x_31 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__49;
+x_31 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__45;
 x_32 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_32, 0, x_31);
 lean_ctor_set(x_32, 1, x_30);
--- a/stage0/stdlib/Lean/Elab/Inductive.c
+++ b/stage0/stdlib/Lean/Elab/Inductive.c
--- a/stage0/stdlib/Lean/Elab/Level.c
+++ b/stage0/stdlib/Lean/Elab/Level.c
@ -43,7 +43,9 @@ lean_object* l_Lean_Elab_Level_mkFreshLevelMVar___boxed(lean_object*, lean_objec
 lean_object* l_Lean_Elab_Level_instMonadRefLevelElabM___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 uint8_t l_USize_decLt(size_t, size_t);
 lean_object* l_Lean_Elab_Level_instMonadNameGeneratorLevelElabM___lambda__3___boxed(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 lean_object* lean_nat_add(lean_object*, lean_object*);
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__34;
 lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Level_elabLevel___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Level_elabLevel___closed__6;
 lean_object* l_ReaderT_bind___at_Lean_Elab_Level_instMonadRefLevelElabM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -84,7 +86,6 @@ lean_object* l_Lean_Elab_Level_elabLevel___closed__5;
 lean_object* l_Lean_Syntax_getArgs(lean_object*);
 lean_object* l___private_Lean_Elab_Level_0__Lean_Elab_Level_isValidAutoBoundLevelName_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getKind(lean_object*);
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
 lean_object* l_Subarray_forInUnsafe_loop___at_Lean_Elab_Level_elabLevel___spec__3(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkFreshId___at_Lean_Elab_Level_mkFreshLevelMVar___spec__1___boxed(lean_object*);
 lean_object* l_Lean_Elab_Level_elabLevel___closed__3;
@ -105,7 +106,6 @@ lean_object* l_Lean_Level_ofNat(lean_object*);
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Level_elabLevel___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkLevelParam(lean_object*);
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__38;
 lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
 lean_object* l_Lean_Elab_Level_instMonadNameGeneratorLevelElabM___closed__4;
 lean_object* l_Lean_Elab_Level_instMonadRefLevelElabM___closed__3;
@ -1000,7 +1000,7 @@ static lean_object* _init_l_Lean_Elab_Level_elabLevel___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 x_2 = l_myMacro____x40_Init_Notation___hyg_5739____closed__7;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@ -1010,7 +1010,7 @@ static lean_object* _init_l_Lean_Elab_Level_elabLevel___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 x_2 = l_Lean_Level_LevelToFormat_Result_format___closed__2;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@ -1020,7 +1020,7 @@ static lean_object* _init_l_Lean_Elab_Level_elabLevel___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 x_2 = l_Lean_Level_LevelToFormat_Result_format___closed__4;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@ -1038,7 +1038,7 @@ static lean_object* _init_l_Lean_Elab_Level_elabLevel___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 x_2 = l_Lean_Elab_Level_elabLevel___closed__4;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@ -1130,7 +1130,7 @@ x_14 = lean_name_eq(x_4, x_13);
 if (x_14 == 0)
 {
 lean_object* x_15; uint8_t x_16; 
-x_15 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__38;
+x_15 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__34;
 x_16 = lean_name_eq(x_4, x_15);
 if (x_16 == 0)
 {
@ -1690,7 +1690,7 @@ x_157 = lean_name_eq(x_4, x_156);
 if (x_157 == 0)
 {
 lean_object* x_158; uint8_t x_159; 
-x_158 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__38;
+x_158 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__34;
 x_159 = lean_name_eq(x_4, x_158);
 if (x_159 == 0)
 {
--- a/stage0/stdlib/Lean/Elab/MutualDef.c
+++ b/stage0/stdlib/Lean/Elab/MutualDef.c
@ -74,6 +74,7 @@ lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_check___lambda__6
 lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___spec__2(size_t, size_t, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_FixPoint_markModified___rarg(lean_object*);
 lean_object* l_Lean_CollectFVars_main(lean_object*, lean_object*);
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__45;
 lean_object* l_Lean_Elab_Term_elabMutualDef___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
 uint8_t l_Lean_Elab_Term_MutualClosure_FixPoint_State_modified___default;
@ -353,7 +354,6 @@ lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_withFunLocalDecls
 lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_FixPoint_fixpoint_match__1(lean_object*);
 lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_check_match__1(lean_object*);
 uint8_t l_Array_anyMUnsafe_any___at_Lean_Elab_Term_MutualClosure_getModifiersForLetRecs___spec__2(lean_object*, size_t, size_t);
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__49;
 lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__4___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_reverse___rarg(lean_object*);
 extern lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
@ -5444,7 +5444,7 @@ lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_declValToTerm(lea
 _start:
 {
 lean_object* x_4; uint8_t x_5; 
-x_4 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__49;
+x_4 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__45;
 lean_inc(x_1);
 x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
 if (x_5 == 0)
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural.c
@ -85,6 +85,7 @@ lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalDeclImp___rarg(le
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_hasBadIndexDep_x3f_match__2(lean_object*);
 lean_object* l_Lean_addTrace___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_mkBRecOn___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_throwToBelowFailed___rarg___closed__3;
+extern lean_object* l_Lean_Meta_evalNat_visit___closed__12;
 extern lean_object* l_Array_empty___closed__1;
 lean_object* lean_environment_find(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkForallFVars___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_replaceRecApps_loop___spec__15___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -521,7 +522,6 @@ lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structu
 uint8_t lean_string_dec_eq(lean_object*, lean_object*);
 uint8_t l_Lean_LocalDecl_isLet(lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
-extern lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1;
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_findRecArg_loop___rarg___lambda__1(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_getFixedPrefix_match__1___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
@ -7236,7 +7236,7 @@ lean_closure_set(x_18, 0, x_14);
 lean_closure_set(x_18, 1, x_1);
 lean_closure_set(x_18, 2, x_4);
 lean_closure_set(x_18, 3, x_5);
-x_19 = l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1;
+x_19 = l_Lean_Meta_evalNat_visit___closed__12;
 x_20 = l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___spec__1___rarg(x_16, x_19, x_18, x_7, x_8, x_9, x_10, x_17);
 return x_20;
 }
@ -12084,7 +12084,7 @@ lean_closure_set(x_36, 3, x_2);
 lean_closure_set(x_36, 4, x_6);
 lean_closure_set(x_36, 5, x_1);
 lean_closure_set(x_36, 6, x_28);
-x_37 = l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1;
+x_37 = l_Lean_Meta_evalNat_visit___closed__12;
 x_38 = l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_mkBRecOn___spec__4___rarg(x_32, x_37, x_36, x_11, x_12, x_13, x_14, x_15, x_35);
 return x_38;
 }
@ -12114,7 +12114,7 @@ lean_closure_set(x_46, 3, x_2);
 lean_closure_set(x_46, 4, x_6);
 lean_closure_set(x_46, 5, x_1);
 lean_closure_set(x_46, 6, x_28);
-x_47 = l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1;
+x_47 = l_Lean_Meta_evalNat_visit___closed__12;
 x_48 = l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_mkBRecOn___spec__4___rarg(x_32, x_47, x_46, x_11, x_12, x_13, x_14, x_15, x_45);
 return x_48;
 }
--- a/stage0/stdlib/Lean/Elab/Quotation.c
+++ b/stage0/stdlib/Lean/Elab/Quotation.c
@ -145,6 +145,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_2714____closed__3;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__2___closed__8;
 lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSyntax___closed__3;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_8830____closed__2;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__11;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__2;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__2___closed__4;
@ -361,7 +362,6 @@ lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_explode
 lean_object* l_Lean_Syntax_getArgs(lean_object*);
 lean_object* l_Lean_Syntax_getKind(lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_38____closed__2;
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_explodeHeadPat(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_2714____closed__7;
 lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___elambda__3___closed__2;
@ -4321,7 +4321,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabLevelQuot_
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 x_2 = l_Lean_Syntax_isQuot_match__1___rarg___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
--- a/stage0/stdlib/Lean/Elab/Structure.c
+++ b/stage0/stdlib/Lean/Elab/Structure.c
--- a/stage0/stdlib/Lean/Elab/Syntax.c
+++ b/stage0/stdlib/Lean/Elab/Syntax.c
--- a/stage0/stdlib/Lean/Elab/Tactic/Basic.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/Basic.c
@ -94,6 +94,7 @@ lean_object* l_Lean_Elab_Tactic_evalTacticSeq1Indented___boxed(lean_object*, lea
 extern lean_object* l_Lean_Parser_Tactic_matchAlt___closed__2;
 extern lean_object* l_Array_empty___closed__1;
 lean_object* l___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_findTag_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2849____closed__10;
 extern lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___closed__4;
 uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Tactic_failIfSuccess___closed__2;
@ -448,7 +449,6 @@ lean_object* l_Lean_Elab_Tactic_focus___rarg___lambda__1___boxed(lean_object*, l
 lean_object* l_Lean_Elab_Tactic_tagUntaggedGoals_match__2(lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalFailIfSuccess(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalIntros_match__1(lean_object*);
-extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_3617____closed__10;
 lean_object* l_Lean_Elab_Tactic_TacticM_run___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Tactic_case___closed__2;
 lean_object* l_Lean_Elab_Tactic_evalChoiceAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -10703,7 +10703,7 @@ x_34 = l_Lean_nullKind___closed__2;
 x_35 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_35, 0, x_34);
 lean_ctor_set(x_35, 1, x_33);
-x_36 = l_myMacro____x40_Init_NotationExtra___hyg_3617____closed__10;
+x_36 = l_myMacro____x40_Init_NotationExtra___hyg_2849____closed__10;
 x_37 = lean_array_push(x_36, x_35);
 x_38 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_38, 0, x_11);
@ -10893,7 +10893,7 @@ x_96 = lean_array_push(x_95, x_94);
 x_97 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_97, 0, x_71);
 lean_ctor_set(x_97, 1, x_96);
-x_98 = l_myMacro____x40_Init_NotationExtra___hyg_3617____closed__10;
+x_98 = l_myMacro____x40_Init_NotationExtra___hyg_2849____closed__10;
 lean_inc(x_97);
 x_99 = lean_array_push(x_98, x_97);
 x_100 = lean_alloc_ctor(1, 2, 0);
--- a/stage0/stdlib/Lean/Elab/Term.c
+++ b/stage0/stdlib/Lean/Elab/Term.c
@ -122,7 +122,6 @@ lean_object* l_Lean_Elab_Term_throwErrorIfErrors___closed__1;
 lean_object* l_Lean_Elab_Term_isValidAutoBoundImplicitName_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Format_pretty(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_liftAttrM(lean_object*);
-lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7516____closed__1;
 lean_object* l_Lean_Elab_Term_throwErrorIfErrors___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_getDeclName_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__2;
@ -143,11 +142,13 @@ lean_object* l_Lean_Meta_getMVarsAtDeclImp(lean_object*, lean_object*, lean_obje
 lean_object* l_Lean_Elab_Term_registerCustomErrorIfMVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__8;
 lean_object* l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__1;
+lean_object* l_Lean_Elab_Term_elabNumLit___lambda__1___closed__1;
 lean_object* l_Lean_Elab_Term_isMonadApp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_elabTypeOf(lean_object*);
 lean_object* l_Lean_Elab_Term_elabQuotedName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_Elab_Term_0__Lean_Elab_Term_tryPureCoe_x3f___spec__3___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_State_letRecsToLift___default;
+extern lean_object* l_Lean_Meta_evalNat_visit___closed__11;
 lean_object* l_Lean_MacroScopesView_format(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_isLetRecAuxMVar___closed__3;
 lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -267,6 +268,7 @@ lean_object* l_Lean_Elab_Term_elabSyntheticHole_match__2(lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeInst(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_foldlM___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__6___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withMVarContext___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__5(lean_object*);
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 lean_object* l_Lean_Meta_mkFreshTypeMVar___at_Lean_Elab_Term_elabNumLit___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_resolveName___closed__6;
 lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoeSort___closed__1;
@ -381,6 +383,7 @@ lean_object* l_List_foldlM___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___sp
 lean_object* l_Lean_Elab_Term_resolveLocalName_loop(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getLocalDecl___at_Lean_Elab_Term_addAutoBoundImplicits___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_levelMVarToParam(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Meta_evalNat_visit___closed__9;
 lean_object* l_Lean_Elab_Term_instInhabitedTermElabM___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MessageData_toString(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabByTactic(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -394,6 +397,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_useImplicitLambda_x3f_
 lean_object* l_Lean_Elab_Term_getMessageLog(lean_object*);
 lean_object* l_Std_AssocList_find_x3f___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__6(lean_object*, lean_object*);
 extern lean_object* l_Lean_initFn____x40_Lean_Data_Options___hyg_476____closed__3;
+lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkFreshLevelMVar___at___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabNumLit___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_ref_take(lean_object*, lean_object*);
@ -440,6 +444,7 @@ lean_object* l_Lean_Elab_Term_withMacroExpansion___rarg(lean_object*, lean_objec
 lean_object* l_Lean_Elab_Term_elabByTactic___closed__2;
 lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__3;
 lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___closed__14;
+lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7578____closed__1;
 lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_useImplicitLambda_x3f___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_mkConst___closed__2;
 extern lean_object* l_Lean_instQuoteProd___rarg___closed__1;
@ -513,7 +518,6 @@ lean_object* l_Lean_Elab_Term_instMonadLogTermElabM___closed__5;
 size_t l_Lean_Name_hash(lean_object*);
 lean_object* l_Lean_withNestedTraces___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_registerSyntheticMVarWithCurrRef___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
 lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__4;
 lean_object* l_Nat_repr(lean_object*);
 lean_object* l_Lean_Elab_Term_elabEnsureExpectedType_match__1(lean_object*);
@ -713,6 +717,7 @@ lean_object* l_Lean_Elab_Term_isLetRecAuxMVar___closed__2;
 lean_object* l___regBuiltin_Lean_Elab_Term_elabCharLit___closed__1;
 extern lean_object* l_Lean_Syntax_mkApp___closed__1;
 lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__4;
+extern lean_object* l_Lean_Meta_evalNat_visit___closed__6;
 lean_object* l_Lean_Elab_Term_elabEnsureExpectedType_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux_match__2(lean_object*);
 lean_object* l_Lean_Elab_Term_liftMetaM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -857,6 +862,7 @@ lean_object* l_Lean_Elab_Term_adaptExpander(lean_object*, lean_object*, lean_obj
 lean_object* l_Lean_Elab_Term_tryPostponeIfMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getPos(lean_object*);
 lean_object* l_Lean_Elab_logAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_exceptionToSorry___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_shouldAddAsStar___closed__1;
 lean_object* l_Lean_Elab_Term_getMessageLog___boxed(lean_object*);
 lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__1;
 lean_object* l_Lean_Elab_Term_isLocalIdent_x3f_match__1(lean_object*);
@ -914,7 +920,6 @@ lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits_
 extern lean_object* l_Lean_Meta_Context_config___default___closed__1;
 lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_Term_0__Lean_Elab_Term_isLambdaWithImplicit___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_liftCoreM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_Meta_evalNat_visit___closed__2;
 lean_object* l_Lean_mkAuxName___at_Lean_Elab_Term_mkAuxName___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_array(lean_object*, lean_object*);
 extern size_t l_Std_PersistentHashMap_insertAux___rarg___closed__2;
@ -979,7 +984,7 @@ lean_object* l_IO_println___at_Lean_instEval___spec__1(lean_object*, lean_object
 lean_object* l_Lean_Elab_Term_logUnassignedUsingErrorInfos_match__2___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_throwErrorIfErrors(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7516_(lean_object*);
+lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7578_(lean_object*);
 lean_object* l_Lean_Elab_Term_elabByTactic_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_addAutoBoundImplicits(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_withAutoBoundImplicitLocal___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1019,6 +1024,7 @@ lean_object* l_Lean_MetavarContext_getDecl(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_instMonadLogTermElabM___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_throwAutoBoundImplicitLocal___rarg___closed__2;
 lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore_match__2___rarg(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Meta_evalNat_visit___closed__7;
 uint8_t l_Std_PersistentArray_anyM___at_Lean_MessageLog_hasErrors___spec__1(lean_object*);
 lean_object* l_Lean_Meta_mkFreshLevelMVar___at_Lean_Elab_Term_ensureType___spec__2___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_HashMapImp_find_x3f___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__5___boxed(lean_object*, lean_object*);
@ -1099,6 +1105,7 @@ lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___lambda__1___boxed(l
 lean_object* l_Lean_getAttributeImpl(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkAppOptM___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Meta_throwLetTypeMismatchMessage___rarg___closed__8;
+lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_saveAllState___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_synthesizeInstMVarCore___spec__3___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_MVarErrorInfo_logError___closed__8;
@ -29834,7 +29841,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_Elab_Term_termElabAttribute;
-x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
+x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 x_4 = l___regBuiltin_Lean_Elab_Term_elabSort___closed__1;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
@ -33228,6 +33235,25 @@ x_10 = l_Lean_Meta_isExprDefEqImp(x_1, x_2, x_5, x_6, x_7, x_8, x_9);
 return x_10;
 }
 }
+lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; lean_object* x_9; 
+x_8 = l_Lean_Elab_throwIllFormedSyntax___rarg___closed__3;
+x_9 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(x_8, x_1, x_2, x_3, x_4, x_5, x_6, x_7);
+return x_9;
+}
+}
+static lean_object* _init_l_Lean_Elab_Term_elabNumLit___lambda__1___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Meta_evalNat_visit___closed__3;
+x_2 = l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_shouldAddAsStar___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
 lean_object* l_Lean_Elab_Term_elabNumLit___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
 _start:
 {
@ -33249,82 +33275,236 @@ lean_dec(x_11);
 x_14 = l_Lean_Meta_decLevel___at_Lean_Elab_Term_elabNumLit___spec__2(x_12, x_4, x_5, x_6, x_7, x_8, x_9, x_13);
 if (lean_obj_tag(x_14) == 0)
 {
-lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; 
 x_15 = lean_ctor_get(x_14, 0);
 lean_inc(x_15);
 x_16 = lean_ctor_get(x_14, 1);
 lean_inc(x_16);
 lean_dec(x_14);
-x_17 = lean_box(0);
-x_18 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_18, 0, x_15);
-lean_ctor_set(x_18, 1, x_17);
-x_19 = l_Lean_Meta_evalNat_visit___closed__2;
-lean_inc(x_18);
-x_20 = l_Lean_mkConst(x_19, x_18);
+x_17 = lean_unsigned_to_nat(0u);
+x_18 = lean_nat_dec_eq(x_2, x_17);
+if (x_18 == 0)
+{
+lean_object* x_19; uint8_t x_20; 
+x_19 = lean_unsigned_to_nat(1u);
+x_20 = lean_nat_dec_eq(x_2, x_19);
+if (x_20 == 0)
+{
+lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
+x_21 = lean_box(0);
+x_22 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_22, 0, x_15);
+lean_ctor_set(x_22, 1, x_21);
+x_23 = l_Lean_Meta_evalNat_visit___closed__6;
+lean_inc(x_22);
+x_24 = l_Lean_mkConst(x_23, x_22);
 lean_inc(x_1);
-x_21 = l_Lean_mkApp(x_20, x_1);
-x_22 = l_Lean_Elab_Term_mkInstMVar(x_21, x_4, x_5, x_6, x_7, x_8, x_9, x_16);
-if (lean_obj_tag(x_22) == 0)
+x_25 = l_Lean_mkApp(x_24, x_1);
+x_26 = l_Lean_Elab_Term_mkInstMVar(x_25, x_4, x_5, x_6, x_7, x_8, x_9, x_16);
+if (lean_obj_tag(x_26) == 0)
 {
-uint8_t x_23; 
-x_23 = !lean_is_exclusive(x_22);
-if (x_23 == 0)
+uint8_t x_27; 
+x_27 = !lean_is_exclusive(x_26);
+if (x_27 == 0)
 {
-lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; 
-x_24 = lean_ctor_get(x_22, 0);
-x_25 = l_Lean_Meta_evalNat_visit___closed__3;
-x_26 = l_Lean_mkConst(x_25, x_18);
-x_27 = l_Lean_mkApp3(x_26, x_1, x_24, x_2);
-lean_ctor_set(x_22, 0, x_27);
-return x_22;
+lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; 
+x_28 = lean_ctor_get(x_26, 0);
+x_29 = l_Lean_Meta_evalNat_visit___closed__7;
+x_30 = l_Lean_mkConst(x_29, x_22);
+x_31 = l_Lean_mkNatLit(x_2);
+x_32 = l_Lean_mkApp3(x_30, x_1, x_28, x_31);
+lean_ctor_set(x_26, 0, x_32);
+return x_26;
 }
 else
 {
-lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; 
-x_28 = lean_ctor_get(x_22, 0);
-x_29 = lean_ctor_get(x_22, 1);
-lean_inc(x_29);
-lean_inc(x_28);
+lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; 
+x_33 = lean_ctor_get(x_26, 0);
+x_34 = lean_ctor_get(x_26, 1);
+lean_inc(x_34);
+lean_inc(x_33);
+lean_dec(x_26);
+x_35 = l_Lean_Meta_evalNat_visit___closed__7;
+x_36 = l_Lean_mkConst(x_35, x_22);
+x_37 = l_Lean_mkNatLit(x_2);
+x_38 = l_Lean_mkApp3(x_36, x_1, x_33, x_37);
+x_39 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_39, 0, x_38);
+lean_ctor_set(x_39, 1, x_34);
+return x_39;
+}
+}
+else
+{
+uint8_t x_40; 
 lean_dec(x_22);
-x_30 = l_Lean_Meta_evalNat_visit___closed__3;
-x_31 = l_Lean_mkConst(x_30, x_18);
-x_32 = l_Lean_mkApp3(x_31, x_1, x_28, x_2);
-x_33 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_33, 0, x_32);
-lean_ctor_set(x_33, 1, x_29);
-return x_33;
-}
-}
-else
-{
-uint8_t x_34; 
-lean_dec(x_18);
 lean_dec(x_2);
 lean_dec(x_1);
-x_34 = !lean_is_exclusive(x_22);
-if (x_34 == 0)
+x_40 = !lean_is_exclusive(x_26);
+if (x_40 == 0)
 {
-return x_22;
+return x_26;
 }
 else
 {
-lean_object* x_35; lean_object* x_36; lean_object* x_37; 
-x_35 = lean_ctor_get(x_22, 0);
-x_36 = lean_ctor_get(x_22, 1);
-lean_inc(x_36);
-lean_inc(x_35);
-lean_dec(x_22);
-x_37 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_37, 0, x_35);
-lean_ctor_set(x_37, 1, x_36);
-return x_37;
+lean_object* x_41; lean_object* x_42; lean_object* x_43; 
+x_41 = lean_ctor_get(x_26, 0);
+x_42 = lean_ctor_get(x_26, 1);
+lean_inc(x_42);
+lean_inc(x_41);
+lean_dec(x_26);
+x_43 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_43, 0, x_41);
+lean_ctor_set(x_43, 1, x_42);
+return x_43;
 }
 }
 }
 else
 {
-uint8_t x_38; 
+lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; 
+lean_dec(x_2);
+x_44 = lean_box(0);
+x_45 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_45, 0, x_15);
+lean_ctor_set(x_45, 1, x_44);
+x_46 = l_Lean_Meta_evalNat_visit___closed__9;
+lean_inc(x_45);
+x_47 = l_Lean_mkConst(x_46, x_45);
+lean_inc(x_1);
+x_48 = l_Lean_mkApp(x_47, x_1);
+x_49 = l_Lean_Elab_Term_mkInstMVar(x_48, x_4, x_5, x_6, x_7, x_8, x_9, x_16);
+if (lean_obj_tag(x_49) == 0)
+{
+uint8_t x_50; 
+x_50 = !lean_is_exclusive(x_49);
+if (x_50 == 0)
+{
+lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; 
+x_51 = lean_ctor_get(x_49, 0);
+x_52 = l_Lean_Meta_evalNat_visit___closed__11;
+x_53 = l_Lean_mkConst(x_52, x_45);
+x_54 = l_Lean_mkAppB(x_53, x_1, x_51);
+lean_ctor_set(x_49, 0, x_54);
+return x_49;
+}
+else
+{
+lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; 
+x_55 = lean_ctor_get(x_49, 0);
+x_56 = lean_ctor_get(x_49, 1);
+lean_inc(x_56);
+lean_inc(x_55);
+lean_dec(x_49);
+x_57 = l_Lean_Meta_evalNat_visit___closed__11;
+x_58 = l_Lean_mkConst(x_57, x_45);
+x_59 = l_Lean_mkAppB(x_58, x_1, x_55);
+x_60 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_60, 0, x_59);
+lean_ctor_set(x_60, 1, x_56);
+return x_60;
+}
+}
+else
+{
+uint8_t x_61; 
+lean_dec(x_45);
+lean_dec(x_1);
+x_61 = !lean_is_exclusive(x_49);
+if (x_61 == 0)
+{
+return x_49;
+}
+else
+{
+lean_object* x_62; lean_object* x_63; lean_object* x_64; 
+x_62 = lean_ctor_get(x_49, 0);
+x_63 = lean_ctor_get(x_49, 1);
+lean_inc(x_63);
+lean_inc(x_62);
+lean_dec(x_49);
+x_64 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_64, 0, x_62);
+lean_ctor_set(x_64, 1, x_63);
+return x_64;
+}
+}
+}
+}
+else
+{
+lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; 
+lean_dec(x_2);
+x_65 = lean_box(0);
+x_66 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_66, 0, x_15);
+lean_ctor_set(x_66, 1, x_65);
+x_67 = l_Lean_Meta_evalNat_visit___closed__3;
+lean_inc(x_66);
+x_68 = l_Lean_mkConst(x_67, x_66);
+lean_inc(x_1);
+x_69 = l_Lean_mkApp(x_68, x_1);
+x_70 = l_Lean_Elab_Term_mkInstMVar(x_69, x_4, x_5, x_6, x_7, x_8, x_9, x_16);
+if (lean_obj_tag(x_70) == 0)
+{
+uint8_t x_71; 
+x_71 = !lean_is_exclusive(x_70);
+if (x_71 == 0)
+{
+lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; 
+x_72 = lean_ctor_get(x_70, 0);
+x_73 = l_Lean_Elab_Term_elabNumLit___lambda__1___closed__1;
+x_74 = l_Lean_mkConst(x_73, x_66);
+x_75 = l_Lean_mkAppB(x_74, x_1, x_72);
+lean_ctor_set(x_70, 0, x_75);
+return x_70;
+}
+else
+{
+lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; 
+x_76 = lean_ctor_get(x_70, 0);
+x_77 = lean_ctor_get(x_70, 1);
+lean_inc(x_77);
+lean_inc(x_76);
+lean_dec(x_70);
+x_78 = l_Lean_Elab_Term_elabNumLit___lambda__1___closed__1;
+x_79 = l_Lean_mkConst(x_78, x_66);
+x_80 = l_Lean_mkAppB(x_79, x_1, x_76);
+x_81 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_81, 0, x_80);
+lean_ctor_set(x_81, 1, x_77);
+return x_81;
+}
+}
+else
+{
+uint8_t x_82; 
+lean_dec(x_66);
+lean_dec(x_1);
+x_82 = !lean_is_exclusive(x_70);
+if (x_82 == 0)
+{
+return x_70;
+}
+else
+{
+lean_object* x_83; lean_object* x_84; lean_object* x_85; 
+x_83 = lean_ctor_get(x_70, 0);
+x_84 = lean_ctor_get(x_70, 1);
+lean_inc(x_84);
+lean_inc(x_83);
+lean_dec(x_70);
+x_85 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_85, 0, x_83);
+lean_ctor_set(x_85, 1, x_84);
+return x_85;
+}
+}
+}
+}
+else
+{
+uint8_t x_86; 
 lean_dec(x_9);
 lean_dec(x_8);
 lean_dec(x_7);
@ -33333,29 +33513,29 @@ lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_2);
 lean_dec(x_1);
-x_38 = !lean_is_exclusive(x_14);
-if (x_38 == 0)
+x_86 = !lean_is_exclusive(x_14);
+if (x_86 == 0)
 {
 return x_14;
 }
 else
 {
-lean_object* x_39; lean_object* x_40; lean_object* x_41; 
-x_39 = lean_ctor_get(x_14, 0);
-x_40 = lean_ctor_get(x_14, 1);
-lean_inc(x_40);
-lean_inc(x_39);
+lean_object* x_87; lean_object* x_88; lean_object* x_89; 
+x_87 = lean_ctor_get(x_14, 0);
+x_88 = lean_ctor_get(x_14, 1);
+lean_inc(x_88);
+lean_inc(x_87);
 lean_dec(x_14);
-x_41 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_41, 0, x_39);
-lean_ctor_set(x_41, 1, x_40);
-return x_41;
+x_89 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_89, 0, x_87);
+lean_ctor_set(x_89, 1, x_88);
+return x_89;
 }
 }
 }
 else
 {
-uint8_t x_42; 
+uint8_t x_90; 
 lean_dec(x_9);
 lean_dec(x_8);
 lean_dec(x_7);
@ -33364,23 +33544,23 @@ lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_2);
 lean_dec(x_1);
-x_42 = !lean_is_exclusive(x_11);
-if (x_42 == 0)
+x_90 = !lean_is_exclusive(x_11);
+if (x_90 == 0)
 {
 return x_11;
 }
 else
 {
-lean_object* x_43; lean_object* x_44; lean_object* x_45; 
-x_43 = lean_ctor_get(x_11, 0);
-x_44 = lean_ctor_get(x_11, 1);
-lean_inc(x_44);
-lean_inc(x_43);
+lean_object* x_91; lean_object* x_92; lean_object* x_93; 
+x_91 = lean_ctor_get(x_11, 0);
+x_92 = lean_ctor_get(x_11, 1);
+lean_inc(x_92);
+lean_inc(x_91);
 lean_dec(x_11);
-x_45 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_45, 0, x_43);
-lean_ctor_set(x_45, 1, x_44);
-return x_45;
+x_93 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_93, 0, x_91);
+lean_ctor_set(x_93, 1, x_92);
+return x_93;
 }
 }
 }
@ -33475,7 +33655,7 @@ if (lean_obj_tag(x_11) == 0)
 {
 lean_object* x_12; uint8_t x_13; 
 lean_dec(x_2);
-x_12 = l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabStrLit___spec__1(x_3, x_4, x_5, x_6, x_7, x_8, x_9);
+x_12 = l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__4(x_3, x_4, x_5, x_6, x_7, x_8, x_9);
 lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_6);
@ -33502,13 +33682,12 @@ return x_16;
 }
 else
 {
-lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+lean_object* x_17; lean_object* x_18; 
 x_17 = lean_ctor_get(x_11, 0);
 lean_inc(x_17);
 lean_dec(x_11);
-x_18 = l_Lean_mkNatLit(x_17);
-x_19 = l_Lean_Elab_Term_elabNumLit___lambda__2(x_2, x_18, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
-return x_19;
+x_18 = l_Lean_Elab_Term_elabNumLit___lambda__2(x_2, x_17, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
+return x_18;
 }
 }
 }
@ -33551,6 +33730,19 @@ lean_dec(x_3);
 return x_10;
 }
 }
+lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; 
+x_8 = l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__4(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_8;
+}
+}
 lean_object* l_Lean_Elab_Term_elabNumLit___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
 _start:
 {
@ -37331,7 +37523,7 @@ x_8 = l_Lean_Elab_Term_instMetaEvalTermElabM___rarg(x_1, x_2, x_3, x_4, x_7, x_6
 return x_8;
 }
 }
-static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7516____closed__1() {
+static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7578____closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@ -37341,7 +37533,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7516_(lean_object* x_1) {
+lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7578_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
@ -37353,7 +37545,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6;
 x_4 = lean_ctor_get(x_3, 1);
 lean_inc(x_4);
 lean_dec(x_3);
-x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7516____closed__1;
+x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7578____closed__1;
 x_6 = l_Lean_registerTraceClass(x_5, x_4);
 if (lean_obj_tag(x_6) == 0)
 {
@ -37909,6 +38101,8 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabStrLit___closed__1);
 res = l___regBuiltin_Lean_Elab_Term_elabStrLit(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l_Lean_Elab_Term_elabNumLit___lambda__1___closed__1 = _init_l_Lean_Elab_Term_elabNumLit___lambda__1___closed__1();
+lean_mark_persistent(l_Lean_Elab_Term_elabNumLit___lambda__1___closed__1);
 l___regBuiltin_Lean_Elab_Term_elabNumLit___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabNumLit___closed__1();
 lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabNumLit___closed__1);
 res = l___regBuiltin_Lean_Elab_Term_elabNumLit(lean_io_mk_world());
@ -37967,9 +38161,9 @@ l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__2 = _init_l_Lean_Elab_Te
 lean_mark_persistent(l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__2);
 l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3 = _init_l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3();
 lean_mark_persistent(l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3);
-l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7516____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7516____closed__1();
-lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7516____closed__1);
-res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7516_(lean_io_mk_world());
+l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7578____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7578____closed__1();
+lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7578____closed__1);
+res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7578_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
--- a/stage0/stdlib/Lean/Expr.c
+++ b/stage0/stdlib/Lean/Expr.c
@ -25,6 +25,7 @@ lean_object* lean_expr_update_forall(lean_object*, uint8_t, lean_object*, lean_o
 lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkDecIsFalse___closed__2;
 lean_object* l_Lean_Expr_bvarIdx_x21___closed__3;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__27;
 size_t l_USize_add(size_t, size_t);
 lean_object* l_Lean_Expr_Data_hash___boxed(lean_object*);
 lean_object* l_Lean_Expr_isApp_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -546,7 +547,6 @@ lean_object* l_Lean_Expr_isLambda_match__1___rarg(lean_object*, lean_object*, le
 uint8_t l_Lean_BinderInfo_isExplicit(uint8_t);
 lean_object* l_Lean_BinderInfo_isAuxDecl_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_updateMData_x21___closed__3;
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__31;
 lean_object* l_Lean_Expr_constName_x21_match__1(lean_object*);
 lean_object* l_Lean_mkApp5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
@ -3325,7 +3325,7 @@ return x_4;
 case 3:
 {
 lean_object* x_5; 
-x_5 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__31;
+x_5 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__27;
 return x_5;
 }
 case 4:
--- a/stage0/stdlib/Lean/Meta/Match/Match.c
+++ b/stage0/stdlib/Lean/Meta/Match/Match.c
@ -103,6 +103,7 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstru
 lean_object* l_Lean_Meta_Match_mkMatcher___lambda__1___closed__7;
 lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Meta_isLevelDefEqAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor_match__1(lean_object*);
+extern lean_object* l_Lean_Meta_evalNat_visit___closed__12;
 extern lean_object* l_Array_empty___closed__1;
 lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoCtor_x3f_match__3(lean_object*);
@ -121,6 +122,7 @@ extern lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_507____close
 uint8_t l_Lean_Meta_Match_Unify_occurs(lean_object*, lean_object*);
 lean_object* l_List_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoCtor_x3f___spec__5___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
+extern lean_object* l_Lean_Meta_evalNat_visit___closed__16;
 lean_object* l_List_append___rarg(lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getUElimPos_x3f___closed__3;
 uint8_t lean_name_eq(lean_object*, lean_object*);
@ -460,7 +462,6 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_mkMin
 lean_object* l_List_filterMapM_loop___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__8___closed__1;
 lean_object* l_Lean_Meta_getLocalDecl___at_Lean_Meta_getFVarLocalDecl___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandNatValuePattern___spec__1(lean_object*);
-extern lean_object* l_Lean_Meta_evalNat_visit___closed__8;
 extern lean_object* l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__1;
 uint8_t l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasAsPattern(lean_object*);
 lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasVarPattern_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -711,7 +712,6 @@ lean_object* l_Lean_Meta_MatcherApp_addArg___lambda__2___closed__1;
 lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwNonSupported___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processVariable_match__2___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1;
 lean_object* l_Lean_Meta_cases___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___closed__1;
 extern lean_object* l_Lean_Meta_mkArrow___rarg___closed__2;
@ -16609,7 +16609,7 @@ x_30 = lean_box(0);
 x_31 = l_Lean_mkNatLit(x_29);
 lean_ctor_set(x_12, 0, x_31);
 lean_ctor_set(x_10, 1, x_30);
-x_32 = l_Lean_Meta_evalNat_visit___closed__8;
+x_32 = l_Lean_Meta_evalNat_visit___closed__16;
 x_33 = lean_alloc_ctor(2, 4, 0);
 lean_ctor_set(x_33, 0, x_32);
 lean_ctor_set(x_33, 1, x_30);
@ -16657,7 +16657,7 @@ lean_ctor_set(x_12, 0, x_43);
 x_44 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_44, 0, x_12);
 lean_ctor_set(x_44, 1, x_42);
-x_45 = l_Lean_Meta_evalNat_visit___closed__8;
+x_45 = l_Lean_Meta_evalNat_visit___closed__16;
 x_46 = lean_alloc_ctor(2, 4, 0);
 lean_ctor_set(x_46, 0, x_45);
 lean_ctor_set(x_46, 1, x_42);
@ -16721,7 +16721,7 @@ if (lean_is_scalar(x_51)) {
 }
 lean_ctor_set(x_59, 0, x_12);
 lean_ctor_set(x_59, 1, x_57);
-x_60 = l_Lean_Meta_evalNat_visit___closed__8;
+x_60 = l_Lean_Meta_evalNat_visit___closed__16;
 x_61 = lean_alloc_ctor(2, 4, 0);
 lean_ctor_set(x_61, 0, x_60);
 lean_ctor_set(x_61, 1, x_57);
@ -16889,7 +16889,7 @@ if (lean_is_scalar(x_79)) {
 }
 lean_ctor_set(x_88, 0, x_87);
 lean_ctor_set(x_88, 1, x_85);
-x_89 = l_Lean_Meta_evalNat_visit___closed__8;
+x_89 = l_Lean_Meta_evalNat_visit___closed__16;
 x_90 = lean_alloc_ctor(2, 4, 0);
 lean_ctor_set(x_90, 0, x_89);
 lean_ctor_set(x_90, 1, x_85);
@ -17131,7 +17131,7 @@ if (lean_is_scalar(x_119)) {
 }
 lean_ctor_set(x_128, 0, x_127);
 lean_ctor_set(x_128, 1, x_125);
-x_129 = l_Lean_Meta_evalNat_visit___closed__8;
+x_129 = l_Lean_Meta_evalNat_visit___closed__16;
 x_130 = lean_alloc_ctor(2, 4, 0);
 lean_ctor_set(x_130, 0, x_129);
 lean_ctor_set(x_130, 1, x_125);
@ -21945,16 +21945,6 @@ return x_25;
 }
 }
 }
-static lean_object* _init_l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; 
-x_1 = lean_unsigned_to_nat(1u);
-x_2 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_2, 0, x_1);
-return x_2;
-}
-}
 lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
 _start:
 {
@ -21962,7 +21952,7 @@ lean_object* x_9; lean_object* x_10; lean_object* x_11;
 x_9 = lean_alloc_closure((void*)(l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__1___boxed), 9, 2);
 lean_closure_set(x_9, 0, x_3);
 lean_closure_set(x_9, 1, x_1);
-x_10 = l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1;
+x_10 = l_Lean_Meta_evalNat_visit___closed__12;
 x_11 = l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___spec__1___rarg(x_2, x_10, x_9, x_4, x_5, x_6, x_7, x_8);
 return x_11;
 }
@ -24007,8 +23997,6 @@ l_Lean_Meta_Match_mkMatcher___lambda__3___closed__1 = _init_l_Lean_Meta_Match_mk
 lean_mark_persistent(l_Lean_Meta_Match_mkMatcher___lambda__3___closed__1);
 l_Lean_Meta_Match_mkMatcher___lambda__3___closed__2 = _init_l_Lean_Meta_Match_mkMatcher___lambda__3___closed__2();
 lean_mark_persistent(l_Lean_Meta_Match_mkMatcher___lambda__3___closed__2);
-l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1 = _init_l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1();
-lean_mark_persistent(l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1);
 l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__3___closed__1 = _init_l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__3___closed__1();
 lean_mark_persistent(l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__3___closed__1);
 l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__3___closed__2 = _init_l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__3___closed__2();
--- a/stage0/stdlib/Lean/Meta/Offset.c
+++ b/stage0/stdlib/Lean/Meta/Offset.c
--- a/stage0/stdlib/Lean/Meta/Tactic/Constructor.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Constructor.c
@ -37,11 +37,11 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallMetaTelescopeReducingAux(lean_object*, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_inferType___at_Lean_Meta_existsIntro___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___kind_term____x40_Init_NotationExtra___hyg_2205____closed__2;
 lean_object* l_Lean_Meta_existsIntro___lambda__2___closed__4;
 lean_object* l_Lean_Meta_withMVarContext___at_Lean_Meta_admit___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getMVarType_x27(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_getConstInfo___at_Lean_Meta_getParamNamesImp___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l___kind_term____x40_Init_NotationExtra___hyg_2973____closed__2;
 lean_object* l_Lean_Meta_throwTacticEx___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_existsIntro___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
@ -875,7 +875,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l___kind_term____x40_Init_NotationExtra___hyg_2973____closed__2;
+x_2 = l___kind_term____x40_Init_NotationExtra___hyg_2205____closed__2;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
--- a/stage0/stdlib/Lean/Meta/UnificationHint.c
+++ b/stage0/stdlib/Lean/Meta/UnificationHint.c
@ -23,7 +23,7 @@ lean_object* l_Lean_stringToMessageData(lean_object*);
 lean_object* l_Lean_Meta_tryUnificationHints___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_div(lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_UnificationHint_0__Lean_Meta_decodeUnificationHint_decode___closed__1;
-lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_1136_(lean_object*);
+lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_1175_(lean_object*);
 lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_501_(lean_object*);
 lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_34_(lean_object*);
 extern lean_object* l_Array_back___at___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_insertAux___spec__2___rarg___closed__2;
@ -112,6 +112,7 @@ lean_object* l___private_Lean_Util_Trace_0__Lean_addNode___at___private_Lean_Met
 lean_object* l_Lean_Meta_commitWhen___at_Lean_Meta_tryUnificationHints_tryCandidate___spec__3___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2532____closed__4;
 lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_34____closed__2;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__46;
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l_Lean_addTrace___at_Lean_Meta_isLevelDefEqAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_unificationHintExtension___elambda__3(lean_object*, lean_object*);
@ -198,7 +199,6 @@ lean_object* l___private_Lean_Meta_UnificationHint_0__Lean_Meta_validateHint___b
 lean_object* l___private_Init_Data_Array_BinSearch_0__Array_binInsertAux___at_Lean_Meta_UnificationHints_add___spec__13___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_ConstantInfo_lparams(lean_object*);
 lean_object* l_Lean_Meta_unificationHintExtension___closed__1;
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__25;
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
 lean_object* l_Lean_Meta_unificationHintExtension___elambda__4___rarg(lean_object*);
 lean_object* lean_instantiate_value_lparams(lean_object*, lean_object*);
@ -5510,7 +5510,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Meta_isExprDefEqImp___closed__2;
-x_2 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__25;
+x_2 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__46;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@ -6790,33 +6790,114 @@ return x_14;
 lean_object* l_Lean_Meta_tryUnificationHints(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
 _start:
 {
-lean_object* x_8; uint8_t x_9; 
-x_8 = lean_ctor_get(x_3, 0);
-lean_inc(x_8);
-x_9 = lean_ctor_get_uint8(x_8, 8);
-lean_dec(x_8);
-if (x_9 == 0)
+lean_object* x_8; uint8_t x_17; lean_object* x_18; lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34; 
+x_31 = lean_st_ref_get(x_6, x_7);
+x_32 = lean_ctor_get(x_31, 0);
+lean_inc(x_32);
+x_33 = lean_ctor_get(x_32, 3);
+lean_inc(x_33);
+lean_dec(x_32);
+x_34 = lean_ctor_get_uint8(x_33, sizeof(void*)*1);
+lean_dec(x_33);
+if (x_34 == 0)
 {
-uint8_t x_10; lean_object* x_11; lean_object* x_12; 
+lean_object* x_35; uint8_t x_36; 
+x_35 = lean_ctor_get(x_31, 1);
+lean_inc(x_35);
+lean_dec(x_31);
+x_36 = 0;
+x_17 = x_36;
+x_18 = x_35;
+goto block_30;
+}
+else
+{
+lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; uint8_t x_42; 
+x_37 = lean_ctor_get(x_31, 1);
+lean_inc(x_37);
+lean_dec(x_31);
+x_38 = l_Lean_Meta_tryUnificationHints_tryCandidate___closed__1;
+x_39 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Meta_isLevelDefEqAux___spec__2(x_38, x_3, x_4, x_5, x_6, x_37);
+x_40 = lean_ctor_get(x_39, 0);
+lean_inc(x_40);
+x_41 = lean_ctor_get(x_39, 1);
+lean_inc(x_41);
+lean_dec(x_39);
+x_42 = lean_unbox(x_40);
+lean_dec(x_40);
+x_17 = x_42;
+x_18 = x_41;
+goto block_30;
+}
+block_16:
+{
+lean_object* x_9; uint8_t x_10; 
+x_9 = lean_ctor_get(x_3, 0);
+lean_inc(x_9);
+x_10 = lean_ctor_get_uint8(x_9, 8);
+lean_dec(x_9);
+if (x_10 == 0)
+{
+uint8_t x_11; lean_object* x_12; lean_object* x_13; 
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_10 = 0;
-x_11 = lean_box(x_10);
-x_12 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_12, 0, x_11);
-lean_ctor_set(x_12, 1, x_7);
-return x_12;
+x_11 = 0;
+x_12 = lean_box(x_11);
+x_13 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_13, 0, x_12);
+lean_ctor_set(x_13, 1, x_8);
+return x_13;
 }
 else
 {
-lean_object* x_13; lean_object* x_14; 
-x_13 = lean_box(0);
-x_14 = l_Lean_Meta_tryUnificationHints___lambda__2(x_1, x_2, x_13, x_3, x_4, x_5, x_6, x_7);
-return x_14;
+lean_object* x_14; lean_object* x_15; 
+x_14 = lean_box(0);
+x_15 = l_Lean_Meta_tryUnificationHints___lambda__2(x_1, x_2, x_14, x_3, x_4, x_5, x_6, x_8);
+return x_15;
+}
+}
+block_30:
+{
+if (x_17 == 0)
+{
+x_8 = x_18;
+goto block_16;
+}
+else
+{
+lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; 
+lean_inc(x_1);
+x_19 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_19, 0, x_1);
+x_20 = l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__1;
+x_21 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_21, 0, x_20);
+lean_ctor_set(x_21, 1, x_19);
+x_22 = l_Lean_Meta_isLevelDefEqAux___closed__5;
+x_23 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_23, 0, x_21);
+lean_ctor_set(x_23, 1, x_22);
+lean_inc(x_2);
+x_24 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_24, 0, x_2);
+x_25 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_25, 0, x_23);
+lean_ctor_set(x_25, 1, x_24);
+x_26 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_26, 0, x_25);
+lean_ctor_set(x_26, 1, x_20);
+x_27 = l_Lean_Meta_tryUnificationHints_tryCandidate___closed__1;
+x_28 = l_Lean_addTrace___at_Lean_Meta_isLevelDefEqAux___spec__1(x_27, x_26, x_3, x_4, x_5, x_6, x_18);
+x_29 = lean_ctor_get(x_28, 1);
+lean_inc(x_29);
+lean_dec(x_28);
+x_8 = x_29;
+goto block_16;
+}
 }
 }
 }
@ -6851,7 +6932,7 @@ lean_dec(x_3);
 return x_9;
 }
 }
-lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_1136_(lean_object* x_1) {
+lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_1175_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
@ -6979,7 +7060,7 @@ l_Array_forInUnsafe_loop___at_Lean_Meta_tryUnificationHints___spec__1___closed__
 lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Meta_tryUnificationHints___spec__1___closed__1);
 l_Array_forInUnsafe_loop___at_Lean_Meta_tryUnificationHints___spec__1___closed__2 = _init_l_Array_forInUnsafe_loop___at_Lean_Meta_tryUnificationHints___spec__1___closed__2();
 lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Meta_tryUnificationHints___spec__1___closed__2);
-res = l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_1136_(lean_io_mk_world());
+res = l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_1175_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
--- a/stage0/stdlib/Lean/Parser/Command.c
+++ b/stage0/stdlib/Lean/Parser/Command.c
@ -290,6 +290,7 @@ lean_object* l_Lean_PrettyPrinter_Formatter_atomic_formatter(lean_object*, lean_
 lean_object* l_Lean_Parser_Command_structure___closed__18;
 lean_object* l_Lean_Parser_Command_synth___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_quot___elambda__1___closed__3;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__45;
 lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__15;
 lean_object* l_Lean_Parser_Command_structFields_formatter___closed__2;
 lean_object* l_Lean_Parser_Command_unsafe___elambda__1___closed__9;
@ -389,6 +390,7 @@ lean_object* l_Lean_Parser_Command_exit___elambda__1___closed__8;
 lean_object* l___regBuiltin_Lean_Parser_Command_resolve__name_parenthesizer(lean_object*);
 lean_object* l_Lean_Parser_Command_section___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Command_declModifiers_formatter___closed__6;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__26;
 lean_object* l_Lean_Parser_Command_axiom___closed__6;
 lean_object* l_Lean_Parser_Command_declValEqns___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Command_theorem___closed__5;
@ -420,7 +422,6 @@ lean_object* l_Lean_Parser_Command_exit___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Command_constant_formatter___closed__7;
 extern lean_object* l_Lean_Parser_Term_tupleTail___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Command_declValSimple___elambda__1(lean_object*, lean_object*);
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__30;
 lean_object* l_Lean_Parser_Command_end_formatter___closed__1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_export(lean_object*);
 lean_object* l_Lean_Parser_Term_quot___closed__9;
@ -848,7 +849,6 @@ lean_object* l_Lean_Parser_Command_variables___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Command_inferMod___closed__3;
 lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__3;
 extern lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute;
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__48;
 lean_object* l_Lean_Parser_Command_declaration_formatter___closed__23;
 lean_object* l_Lean_Parser_Command_noncomputable___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___closed__4;
@ -1116,6 +1116,7 @@ lean_object* l_Lean_Parser_Command_classInductive_parenthesizer___closed__5;
 lean_object* l_Lean_Parser_Command_section_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Command_inductive_formatter___closed__1;
 lean_object* l_Lean_Parser_Command_attribute_formatter___closed__4;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__44;
 lean_object* l_Lean_Parser_Command_declId_formatter___closed__5;
 lean_object* l___regBuiltin_Lean_Parser_Command_init__quot_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Command_openSimple___closed__3;
@ -1401,7 +1402,6 @@ lean_object* l_Lean_Parser_Command_declModifiers(uint8_t);
 lean_object* l_Lean_Parser_Command_exit___elambda__1___closed__3;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_builtin__initialize(lean_object*);
 lean_object* l_Lean_Parser_Command_theorem_formatter___closed__4;
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__49;
 lean_object* l_Lean_Parser_Command_ctor_formatter___closed__9;
 lean_object* l_Lean_Parser_Command_structInstBinder___elambda__1___closed__12;
 lean_object* l_Lean_Parser_Command_structFields___closed__3;
@ -1698,6 +1698,7 @@ lean_object* l_Lean_Parser_Command_declSig___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Command_attribute_formatter___closed__6;
 lean_object* l_Lean_Parser_Command_set__option___closed__4;
 lean_object* l_Lean_Parser_Command_example___elambda__1___closed__9;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__25;
 lean_object* l_Lean_Parser_Command_structureTk_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_constant_parenthesizer___closed__6;
 lean_object* l_Lean_Parser_Command_structFields_formatter___closed__5;
@ -1842,7 +1843,6 @@ lean_object* l_Lean_Parser_Command_structure___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Command_declModifiers___elambda__1___closed__14;
 lean_object* l_Lean_Parser_Command_mutual___elambda__1___closed__10;
 lean_object* l_Lean_Parser_commandParser_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__29;
 lean_object* l_Lean_Parser_Command_structCtor___closed__3;
 lean_object* l_Lean_Parser_Command_synth_formatter___closed__1;
 extern lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__10;
@ -5287,7 +5287,7 @@ static lean_object* _init_l_Lean_Parser_Command_optDeclSig___elambda__1___closed
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__30;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__26;
 x_2 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
@ -5297,7 +5297,7 @@ static lean_object* _init_l_Lean_Parser_Command_optDeclSig___elambda__1___closed
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__29;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__25;
 x_2 = l_Lean_Parser_Command_optDeclSig___elambda__1___closed__1;
 x_3 = 1;
 x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -5320,7 +5320,7 @@ static lean_object* _init_l_Lean_Parser_Command_optDeclSig___elambda__1___closed
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__30;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__26;
 x_2 = l_Lean_Parser_Command_optDeclSig___elambda__1___closed__3;
 x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
 lean_closure_set(x_3, 0, x_1);
@ -5357,7 +5357,7 @@ static lean_object* _init_l_Lean_Parser_Command_optDeclSig___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__30;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__26;
 x_2 = l_Lean_Parser_Term_letIdLhs___closed__4;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
@ -5417,7 +5417,7 @@ static lean_object* _init_l_Lean_Parser_Command_declValSimple___elambda__1___clo
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__49;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__45;
 x_2 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
@ -5427,7 +5427,7 @@ static lean_object* _init_l_Lean_Parser_Command_declValSimple___elambda__1___clo
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__48;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__44;
 x_2 = l_Lean_Parser_Command_declValSimple___elambda__1___closed__1;
 x_3 = 1;
 x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -5489,7 +5489,7 @@ static lean_object* _init_l_Lean_Parser_Command_declValSimple___elambda__1___clo
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__49;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__45;
 x_2 = l_Lean_Parser_Command_declValSimple___elambda__1___closed__7;
 x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
 lean_closure_set(x_3, 0, x_1);
@ -5557,7 +5557,7 @@ static lean_object* _init_l_Lean_Parser_Command_declValSimple___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__49;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__45;
 x_2 = l_Lean_Parser_Command_declValSimple___closed__3;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
@ -12231,7 +12231,7 @@ static lean_object* _init_l_Lean_Parser_Command_optDeclSig_formatter___closed__1
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__29;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__25;
 x_2 = l_Lean_Parser_Command_optDeclSig___elambda__1___closed__1;
 x_3 = 1;
 x_4 = lean_box(x_3);
@ -12246,7 +12246,7 @@ static lean_object* _init_l_Lean_Parser_Command_optDeclSig_formatter___closed__2
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__30;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__26;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Term_letIdLhs_formatter___closed__5;
 x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -12270,7 +12270,7 @@ static lean_object* _init_l_Lean_Parser_Command_declValSimple_formatter___closed
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__48;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__44;
 x_2 = l_Lean_Parser_Command_declValSimple___elambda__1___closed__1;
 x_3 = 1;
 x_4 = lean_box(x_3);
@ -12319,7 +12319,7 @@ static lean_object* _init_l_Lean_Parser_Command_declValSimple_formatter___closed
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__49;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__45;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Command_declValSimple_formatter___closed__4;
 x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -15532,7 +15532,7 @@ static lean_object* _init_l_Lean_Parser_Command_optDeclSig_parenthesizer___close
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__30;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__26;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Term_letIdLhs_parenthesizer___closed__5;
 x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -15593,7 +15593,7 @@ static lean_object* _init_l_Lean_Parser_Command_declValSimple_parenthesizer___cl
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__49;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__45;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Command_declValSimple_parenthesizer___closed__3;
 x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
--- a/stage0/stdlib/Lean/Parser/Level.c
+++ b/stage0/stdlib/Lean/Parser/Level.c
@ -89,6 +89,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer(lean_objec
 extern lean_object* l_Lean_Parser_leadingNode_formatter___closed__1;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkPrec_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_max___elambda__1___closed__2;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 lean_object* l_Lean_Parser_checkPrecFn(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_many1Fn(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__3;
@ -97,6 +98,7 @@ lean_object* l_Lean_Parser_Level_num_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_Level_max___closed__3;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_8168____closed__14;
 lean_object* l_Lean_PrettyPrinter_Formatter_trailingNode_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__34;
 lean_object* l_Lean_Parser_Level_hole_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_max___elambda__1___closed__4;
 lean_object* l___regBuiltin_Lean_Parser_Level_addLit_parenthesizer(lean_object*);
@ -190,7 +192,6 @@ lean_object* l_Lean_Parser_Level_max;
 lean_object* l_Lean_Parser_Level_num;
 lean_object* l_Lean_Parser_categoryParser(lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Parser_Level_imax_parenthesizer___closed__1;
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
 lean_object* l_Lean_Parser_Level_max___closed__5;
 lean_object* l_Lean_Parser_Level_num___closed__3;
 lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__10;
@ -250,7 +251,6 @@ lean_object* l_Lean_Parser_Level_imax___closed__6;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_imax_formatter___closed__3;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_many1_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__38;
 lean_object* l_Lean_Parser_Level_addLit___closed__4;
 lean_object* l_Lean_Parser_numLit_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_paren___closed__6;
@ -769,7 +769,7 @@ static lean_object* _init_l_Lean_Parser_Level_max___elambda__1___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 x_2 = l_Lean_Level_LevelToFormat_Result_format___closed__2;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@ -1181,7 +1181,7 @@ static lean_object* _init_l_Lean_Parser_Level_imax___elambda__1___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 x_2 = l_Lean_Level_LevelToFormat_Result_format___closed__4;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@ -1519,7 +1519,7 @@ static lean_object* _init_l_Lean_Parser_Level_hole___elambda__1___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__38;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__34;
 x_2 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
@ -1559,7 +1559,7 @@ static lean_object* _init_l_Lean_Parser_Level_hole___elambda__1___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__38;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__34;
 x_2 = l_Lean_Parser_Level_hole___elambda__1___closed__4;
 x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
 lean_closure_set(x_3, 0, x_1);
@ -1605,7 +1605,7 @@ static lean_object* _init_l_Lean_Parser_Level_hole___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__38;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__34;
 x_2 = l_Lean_Parser_Level_hole___closed__1;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
@ -1666,7 +1666,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___closed__2;
-x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__38;
+x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__34;
 x_4 = 1;
 x_5 = l_Lean_Parser_Level_hole;
 x_6 = lean_unsigned_to_nat(0u);
@ -1703,7 +1703,7 @@ static lean_object* _init_l_Lean_Parser_Level_hole_formatter___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__38;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__34;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Level_hole_formatter___closed__2;
 x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -1736,7 +1736,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_PrettyPrinter_formatterAttribute;
-x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__38;
+x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__34;
 x_4 = l___regBuiltin_Lean_Parser_Level_hole_formatter___closed__1;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
@ -1759,7 +1759,7 @@ static lean_object* _init_l_Lean_Parser_Level_hole_parenthesizer___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__38;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__34;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
 x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -1792,7 +1792,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_PrettyPrinter_parenthesizerAttribute;
-x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__38;
+x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__34;
 x_4 = l___regBuiltin_Lean_Parser_Level_hole_parenthesizer___closed__1;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
@ -1864,7 +1864,7 @@ static lean_object* _init_l___regBuiltinParser_Lean_Parser_Level_num___closed__1
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1882____closed__7;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@ -2033,7 +2033,7 @@ static lean_object* _init_l___regBuiltinParser_Lean_Parser_Level_ident___closed_
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 x_2 = l_Lean_identKind___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@ -2138,7 +2138,7 @@ static lean_object* _init_l_Lean_Parser_Level_addLit___elambda__1___closed__2()
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 x_2 = l_Lean_Parser_Level_addLit___elambda__1___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
--- a/stage0/stdlib/Lean/Parser/Syntax.c
+++ b/stage0/stdlib/Lean/Parser/Syntax.c
--- a/stage0/stdlib/Lean/Parser/Term.c
+++ b/stage0/stdlib/Lean/Parser/Term.c
@ -94,6 +94,7 @@ lean_object* l_Lean_Parser_Term_dbgTrace_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Term_nomatch_parenthesizer___closed__2;
 lean_object* l_Lean_PrettyPrinter_Formatter_visitArgs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_macroLastArg_formatter___closed__2;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__27;
 lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Term___hyg_3476____closed__17;
 lean_object* l___regBuiltin_Lean_Parser_Term_forall_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__10;
@ -838,6 +839,7 @@ lean_object* l___regBuiltin_Lean_Parser_Term_explicit_parenthesizer(lean_object*
 extern lean_object* l_Lean_Parser_Level_num___closed__1;
 lean_object* l___regBuiltin_Lean_Parser_Term_arrow_formatter(lean_object*);
 lean_object* l_Lean_Parser_Term_instBinder___closed__7;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 extern lean_object* l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
 lean_object* l_Lean_Parser_Term_uminus_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_explicit___closed__8;
@ -1654,7 +1656,6 @@ lean_object* l_Lean_Parser_Term_sufficesDecl_formatter(lean_object*, lean_object
 lean_object* l_Lean_Parser_Term_show_formatter___closed__3;
 lean_object* l_Lean_Parser_Term_typeOf___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Term_matchDiscr___elambda__1___closed__1;
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
 extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__10;
 lean_object* l_Lean_Parser_Term_structInstArrayRef_parenthesizer___closed__3;
 lean_object* l_Lean_Parser_Term_paren___closed__6;
@ -2561,6 +2562,7 @@ lean_object* l_Lean_Parser_Term_typeOf___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_letrec_parenthesizer___closed__6;
 lean_object* l_Lean_Parser_Term_num;
 lean_object* l_Lean_Parser_Term_stateRefT_formatter___closed__4;
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__29;
 lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__10;
 lean_object* l___regBuiltin_Lean_Parser_Term_decide_formatter___closed__1;
 lean_object* l_Lean_Parser_Term_haveDecl_parenthesizer___closed__5;
@ -2611,7 +2613,6 @@ lean_object* l_Lean_Parser_Term_haveDecl_formatter___closed__3;
 lean_object* l_Lean_Parser_Term_let_x21___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_letDecl_formatter___closed__5;
 lean_object* l_Lean_Parser_Term_matchDiscr_parenthesizer___closed__1;
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__31;
 lean_object* l_Lean_Parser_Term_macroDollarArg;
 lean_object* l_Lean_Parser_Term_simpleBinderWithoutType___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_anonymousCtor_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -2620,7 +2621,6 @@ lean_object* l_Lean_Parser_Term_letRecDecls_formatter___closed__3;
 lean_object* l_Lean_Parser_Term_ensureTypeOf_parenthesizer___closed__4;
 lean_object* l_Lean_Parser_Term_binderType___closed__2;
 lean_object* l_Lean_Parser_Term_borrowed___closed__5;
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
 lean_object* l_Lean_Parser_Term_explicitUniv___closed__8;
 lean_object* l_Lean_Parser_Term_attrInstance_parenthesizer___closed__7;
 lean_object* l_Lean_Parser_Term_letPatDecl_formatter___closed__5;
@ -7151,7 +7151,7 @@ static lean_object* _init_l_Lean_Parser_Term_sort___elambda__1___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 x_2 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
@ -7161,7 +7161,7 @@ static lean_object* _init_l_Lean_Parser_Term_sort___elambda__1___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__31;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__27;
 x_2 = l_Lean_Parser_Term_sort___elambda__1___closed__1;
 x_3 = 1;
 x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -7172,7 +7172,7 @@ static lean_object* _init_l_Lean_Parser_Term_sort___elambda__1___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__29;
 x_2 = l_String_trim(x_1);
 return x_2;
 }
@ -7203,7 +7203,7 @@ static lean_object* _init_l_Lean_Parser_Term_sort___elambda__1___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 x_2 = l_Lean_Parser_Term_sort___elambda__1___closed__5;
 x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
 lean_closure_set(x_3, 0, x_1);
@ -7259,7 +7259,7 @@ static lean_object* _init_l_Lean_Parser_Term_sort___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 x_2 = l_Lean_Parser_Term_sort___closed__2;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
@ -7320,7 +7320,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l___kind_term____x40_Init_Notation___hyg_3____closed__16;
-x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
+x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 x_4 = 1;
 x_5 = l_Lean_Parser_Term_sort;
 x_6 = lean_unsigned_to_nat(0u);
@ -7332,7 +7332,7 @@ static lean_object* _init_l_Lean_Parser_Term_sort_formatter___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__31;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__27;
 x_2 = l_Lean_Parser_Term_sort___elambda__1___closed__1;
 x_3 = 1;
 x_4 = lean_box(x_3);
@ -7347,7 +7347,7 @@ static lean_object* _init_l_Lean_Parser_Term_sort_formatter___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__29;
 x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_symbol_formatter), 6, 1);
 lean_closure_set(x_2, 0, x_1);
 return x_2;
@ -7369,7 +7369,7 @@ static lean_object* _init_l_Lean_Parser_Term_sort_formatter___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Term_sort_formatter___closed__3;
 x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -7402,7 +7402,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_PrettyPrinter_formatterAttribute;
-x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
+x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 x_4 = l___regBuiltin_Lean_Parser_Term_sort_formatter___closed__1;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
@ -7425,7 +7425,7 @@ static lean_object* _init_l_Lean_Parser_Term_sort_parenthesizer___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Term_type_parenthesizer___closed__7;
 x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -7458,7 +7458,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_PrettyPrinter_parenthesizerAttribute;
-x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__32;
+x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__28;
 x_4 = l___regBuiltin_Lean_Parser_Term_sort_parenthesizer___closed__1;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
@ -43093,7 +43093,7 @@ static lean_object* _init_l_Lean_Parser_Level_quot___elambda__1___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 x_2 = l_Lean_Syntax_isQuot_match__1___rarg___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
--- a/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c
+++ b/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c
@ -182,6 +182,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_parenthesizerForKind___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkPrec_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_term_parenthesizer_match__1___rarg(lean_object*, lean_object*);
+extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_unicodeSymbol_parenthesizer___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer_match__1(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -455,7 +456,6 @@ lean_object* l_Lean_Syntax_getKind(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2405____closed__4;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_38____closed__2;
 uint8_t l_Lean_Parser_isValidSyntaxNodeKind(lean_object*, lean_object*);
-extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
 lean_object* l_Lean_Syntax_Traverser_right(lean_object*);
 lean_object* l_Array_foldlMUnsafe_fold___at_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_visitToken___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -8006,7 +8006,7 @@ static lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__37;
+x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1157____closed__33;
 x_2 = l_myMacro____x40_Init_Notation___hyg_5739____closed__7;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;