chore: update stage0

stage0/src/Init/Data/Array/Subarray.lean

@@ -17,6 +17,27 @@ structure Subarray (α : Type u)  where
 
 namespace Subarray
 
+def size (s : Subarray α) : Nat :=
+  s.stop - s.start
+
+def get (s : Subarray α) (i : Fin s.size) : α :=
+  have : s.start + i.val < s.as.size := by
+   apply Nat.lt_of_lt_of_le _ s.h₂
+   have := i.isLt
+   simp [size] at this
+   rw [Nat.add_comm]
+   exact Nat.add_lt_of_lt_sub s.h₁ this
+  s.as.get ⟨s.start + i.val, this⟩
+
+@[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
+  if h : i < s.size then s.get ⟨i, h⟩ else v₀
+
+def get! [Inhabited α] (s : Subarray α) (i : Nat) : α :=
+  getD s i default
+
+def getOp [Inhabited α] (self : Subarray α) (idx : Nat) : α :=
+  self.get! idx
+
 def popFront (s : Subarray α) : Subarray α :=
   if h : s.start < s.stop then
     { s with start := s.start + 1, h₁ := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) }

stage0/src/Init/Data/Nat/Basic.lean

@@ -610,6 +610,15 @@ theorem le_sub_of_add_le {a b c : Nat} (h : a + b ≤ c) : a ≤ c - b := by
     have hd := Nat.sub_eq_of_eq_add hd.symm
     exact hd.symm
 
+theorem add_lt_of_lt_sub {a b c : Nat} (hle : b ≤ c) (h : a < c - b) : a + b < c := by
+  have : a.succ + b ≤ c := add_le_of_le_sub hle h
+  simp [Nat.succ_add] at this
+  exact this
+
+theorem lt_sub_of_add_lt {a b c : Nat} (h : a + b < c) : a < c - b :=
+  have : a.succ + b ≤ c := by simp [Nat.succ_add]; exact h
+  le_sub_of_add_le this
+
 @[simp] protected theorem pred_zero : pred 0 = 0 :=
   rfl
 

stage0/src/Init/Notation.lean

@@ -218,9 +218,13 @@ macro_rules
 /-- Special identifier introduced by "anonymous" `have : ...`, `suffices p ...` etc. -/
 macro tk:"this" : term => return Syntax.ident tk.getHeadInfo "this".toSubstring `this []
 
-namespace Parser.Tactic
+/-
+  Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer.
+  The only accepted parser for this category is an antiquotation. -/
 declare_syntax_cat rawStx
-/-- `withAnnotateState stx t` annotates the lexical range of `stx : Syntax` with the initial and final state of running tactic `t`. -/
+
+namespace Parser.Tactic
+/-- `with_annotate_state stx t` annotates the lexical range of `stx : Syntax` with the initial and final state of running tactic `t`. -/
 scoped syntax (name := withAnnotateState) "with_annotate_state " rawStx ppSpace tactic : tactic
 
 /--
@@ -350,7 +354,12 @@ syntax (name := rotateRight) "rotate_right" (num)? : tactic
 /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
 macro "try " t:tacticSeq : tactic => `(first | $t | skip)
 /-- `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal, concatenating all goals produced by `tac'`. -/
-macro:1 x:tactic " <;> " y:tactic:0 : tactic => `(tactic| focus ($x:tactic; all_goals $y:tactic))
+macro:1 x:tactic tk:" <;> " y:tactic:0 : tactic => `(tactic|
+  focus
+    $x:tactic
+    -- annotate token with state after executing `x`
+    with_annotate_state $tk skip
+    all_goals $y:tactic)
 
 /-- `eq_refl` is equivalent to `exact rfl`, but has a few optimizatons. -/
 syntax (name := refl) "eq_refl" : tactic

stage0/src/Lean/Data/Json/Parser.lean

@@ -50,17 +50,15 @@ partial def strCore (acc : String) : Parsec String := do
     return acc
   else
     let c ← anyChar
-    let ec ←
-      if c = '\\' then
-        escapedChar
-      -- as to whether c.val > 0xffff should be split up and encoded with multiple \u,
-      -- the JSON standard is not definite: both directly printing the character
-      -- and encoding it with multiple \u is allowed. we choose the former.
-      else if 0x0020 ≤ c.val ∧ c.val ≤ 0x10ffff then
-        pure c
-      else
-        fail "unexpected character in string"
-    strCore (acc.push ec)
+    if c = '\\' then
+      strCore (acc.push (← escapedChar))
+    -- as to whether c.val > 0xffff should be split up and encoded with multiple \u,
+    -- the JSON standard is not definite: both directly printing the character
+    -- and encoding it with multiple \u is allowed. we choose the former.
+    else if 0x0020 ≤ c.val ∧ c.val ≤ 0x10ffff then
+      strCore (acc.push c)
+    else
+      fail "unexpected character in string"
 
 def str : Parsec String := strCore ""
 

stage0/src/Lean/Elab/Match.lean

@@ -67,8 +67,14 @@ private def elabAtomicDiscr (discr : Syntax) : TermElabM Expr := do
       instantiateMVars localDecl.value
   | _ => throwErrorAt discr "unexpected discriminant"
 
+structure Discr where
+  expr : Expr
+  /-- `some h` if discriminant is annotated with the `h : ` notation. -/
+  h?  : Option Syntax := none
+  deriving Inhabited
+
 structure ElabMatchTypeAndDiscrsResult where
-  discrs    : Array Expr
+  discrs    : Array Discr
   matchType : Expr
   /- `true` when performing dependent elimination. We use this to decide whether we optimize the "match unit" case.
      See `isMatchUnit?`. -/
@@ -88,7 +94,7 @@ private partial def elabMatchTypeAndDiscrs (discrStxs : Array Syntax) (matchOptM
       return { discrs := discrs, matchType := matchType, isDep := isDep, alts := matchAltViews }
   where
     /- Easy case: elaborate discriminant when the match-type has been explicitly provided by the user.  -/
-    elabDiscrsWitMatchType (matchType : Expr) (expectedType : Expr) : TermElabM (Array Expr × Bool) := do
+    elabDiscrsWitMatchType (matchType : Expr) (expectedType : Expr) : TermElabM (Array Discr × Bool) := do
       let mut discrs := #[]
       let mut i := 0
       let mut matchType := matchType
@@ -103,7 +109,7 @@ private partial def elabMatchTypeAndDiscrs (discrStxs : Array Syntax) (matchOptM
           if b.hasLooseBVars then
             isDep := true
           matchType := b.instantiate1 discr
-          discrs := discrs.push discr
+          discrs := discrs.push { expr := discr }
         | _ =>
           throwError "invalid motive provided to match-expression, function type with arity #{discrStxs.size} expected"
       return (discrs, isDep)
@@ -112,41 +118,21 @@ private partial def elabMatchTypeAndDiscrs (discrStxs : Array Syntax) (matchOptM
       { r with isDep := true }
 
     /- Elaborate discriminants inferring the match-type -/
-    elabDiscrs (i : Nat) (discrs : Array Expr) : TermElabM ElabMatchTypeAndDiscrsResult := do
+    elabDiscrs (i : Nat) (discrs : Array Discr) : TermElabM ElabMatchTypeAndDiscrsResult := do
       if h : i < discrStxs.size then
         let discrStx := discrStxs.get ⟨i, h⟩
         let discr     ← elabAtomicDiscr discrStx
         let discr     ← instantiateMVars discr
         let discrType ← inferType discr
         let discrType ← instantiateMVars discrType
-        let discrs    := discrs.push discr
         let userName ← mkUserNameFor discr
-        if discrStx[0].isNone then
-          let mut result ← elabDiscrs (i + 1) discrs
-          let matchTypeBody ← kabstract result.matchType discr
-          if matchTypeBody.hasLooseBVars then
-            result := markIsDep result
-          return { result with matchType := Lean.mkForall userName BinderInfo.default discrType matchTypeBody }
-        else
-          let discrs := discrs.push (← mkEqRefl discr)
-          let result ← elabDiscrs (i + 1) discrs
-          let result := markIsDep result
-          let identStx := discrStx[0][0]
-          withLocalDeclD userName discrType fun x => do
-            let eqType ← mkEq discr x
-            withLocalDeclD identStx.getId eqType fun h => do
-              let matchTypeBody ← kabstract result.matchType discr
-              let matchTypeBody := matchTypeBody.instantiate1 x
-              let matchType ← mkForallFVars #[x, h] matchTypeBody
-              return { result with
-                matchType := matchType
-                alts      := result.alts.map fun altView =>
-                  if i+1 > altView.patterns.size then
-                    -- Unexpected number of patterns. The input is invalid, but we want to process whatever to provide info to users.
-                    altView
-                  else
-                    { altView with patterns := altView.patterns.insertAt (i+1) identStx }
-              }
+        let h? := if discrStx[0].isNone then none else some discrStx[0][0]
+        let discrs := discrs.push { expr := discr, h? }
+        let mut result ← elabDiscrs (i + 1) discrs
+        let matchTypeBody ← kabstract result.matchType discr
+        if matchTypeBody.hasLooseBVars then
+          result := markIsDep result
+        return { result with matchType := Lean.mkForall userName BinderInfo.default discrType matchTypeBody }
       else
         return { discrs, alts := matchAltViews, isDep := false, matchType := expectedType }
 
@@ -783,32 +769,55 @@ private def withoutAuxDiscrs (matchType : Expr) (k : TermElabM α) : TermElabM
       toClear := toClear.push localDecl.fvarId
   withToClear toClear matchType k
 
+/--
+  Generate equalities `h : discr = pattern` for discriminants annotated with `h :`.
+  We use these equalities to elaborate the right-hand-side of a `match` alternative.
+-/
+private def withEqs (discrs : Array Discr) (patterns : List Pattern) (k : Array Expr → TermElabM α) : TermElabM α := do
+  go 0 patterns #[]
+where
+  go (i : Nat) (ps : List Pattern) (eqs : Array Expr) : TermElabM α := do
+    match ps with
+    | [] => k eqs
+    | p::ps =>
+      if h : i < discrs.size then
+        let discr := discrs.get ⟨i, h⟩
+        if let some h := discr.h? then
+          withLocalDeclD h.getId (← mkEq discr.expr (← p.toExpr)) fun eq => do
+            addTermInfo' h eq (isBinder := true)
+            go (i+1) ps (eqs.push eq)
+        else
+          go (i+1) ps eqs
+      else
+        k eqs
+
 /--
   Elaborate the `match` alternative `alt` using the given `matchType`.
   The array `toClear` contains variables that must be cleared before elaborating the `rhs` because
   they have been generalized/refined.
 -/
-private def elabMatchAltView (alt : MatchAltView) (matchType : Expr) (toClear : Array FVarId) : ExceptT PatternElabException TermElabM (AltLHS × Expr) := withRef alt.ref do
+private def elabMatchAltView (discrs : Array Discr) (alt : MatchAltView) (matchType : Expr) (toClear : Array FVarId) : ExceptT PatternElabException TermElabM (AltLHS × Expr) := withRef alt.ref do
   withoutAuxDiscrs matchType do
     let (patternVars, alt) ← collectPatternVars alt
     trace[Elab.match] "patternVars: {patternVars}"
     withPatternVars patternVars fun patternVarDecls => do
-      withElaboratedLHS alt.ref patternVarDecls alt.patterns matchType fun altLHS matchType => do
-        withLocalInstances altLHS.fvarDecls do
-          trace[Elab.match] "elabMatchAltView: {matchType}"
-          let matchType ← instantiateMVars matchType
-          -- If `matchType` is of the form `@m ...`, we create a new metavariable with the current scope.
-          -- This improves the effectiveness of the `isDefEq` default approximations
-          let matchType' ← if matchType.getAppFn.isMVar then mkFreshTypeMVar else pure matchType
-          withToClear toClear matchType' do
-            let rhs ← elabTermEnsuringType alt.rhs matchType'
-            -- We use all approximations to ensure the auxiliary type is defeq to the original one.
-            unless (← fullApproxDefEq <| isDefEq matchType' matchType) do
-              throwError "type mistmatch, alternative {← mkHasTypeButIsExpectedMsg matchType' matchType}"
-            let xs := altLHS.fvarDecls.toArray.map LocalDecl.toExpr
-            let rhs ← if xs.isEmpty then pure <| mkSimpleThunk rhs else mkLambdaFVars xs rhs
-            trace[Elab.match] "rhs: {rhs}"
-            return (altLHS, rhs)
+      withElaboratedLHS alt.ref patternVarDecls alt.patterns matchType fun altLHS matchType =>
+        withEqs discrs altLHS.patterns fun eqs =>
+          withLocalInstances altLHS.fvarDecls do
+            trace[Elab.match] "elabMatchAltView: {matchType}"
+            let matchType ← instantiateMVars matchType
+            -- If `matchType` is of the form `@m ...`, we create a new metavariable with the current scope.
+            -- This improves the effectiveness of the `isDefEq` default approximations
+            let matchType' ← if matchType.getAppFn.isMVar then mkFreshTypeMVar else pure matchType
+            withToClear toClear matchType' do
+              let rhs ← elabTermEnsuringType alt.rhs matchType'
+              -- We use all approximations to ensure the auxiliary type is defeq to the original one.
+              unless (← fullApproxDefEq <| isDefEq matchType' matchType) do
+                throwError "type mistmatch, alternative {← mkHasTypeButIsExpectedMsg matchType' matchType}"
+              let xs := altLHS.fvarDecls.toArray.map LocalDecl.toExpr ++ eqs
+              let rhs ← if xs.isEmpty then pure <| mkSimpleThunk rhs else mkLambdaFVars xs rhs
+              trace[Elab.match] "rhs: {rhs}"
+              return (altLHS, rhs)
 
 /--
   Collect problematic index for the "discriminant refinement feature". This method is invoked
@@ -825,7 +834,7 @@ where
       go (e.getArg! i) path
 
 structure GeneralizeResult where
-  discrs    : Array Expr
+  discrs    : Array Discr
   /-- `FVarId`s of the variables that have been generalized. We store them to clear after in each branch. -/
   toClear   : Array FVarId := #[]
   matchType : Expr
@@ -843,24 +852,25 @@ structure GeneralizeResult where
     but they become inaccessible since they are shadowed by the patterns variables. We assume this is ok since
     this is the exact behavior users would get if they had written it by hand. Recall there is no `clear` in term mode.
 -/
-private def generalize (discrs : Array Expr) (matchType : Expr) (altViews : Array MatchAltView) (generalizing? : Option Bool) : TermElabM GeneralizeResult := do
+private def generalize (discrs : Array Discr) (matchType : Expr) (altViews : Array MatchAltView) (generalizing? : Option Bool) : TermElabM GeneralizeResult := do
   let gen := if let some g := generalizing? then g else true
   if !gen then
     return { discrs, matchType, altViews }
   else
+    let discrExprs := discrs.map (·.expr)
     /- let-decls are currently being ignored by the generalizer. -/
-    let ysFVarIds ← getFVarsToGeneralize discrs (ignoreLetDecls := true)
+    let ysFVarIds ← getFVarsToGeneralize discrExprs (ignoreLetDecls := true)
     if ysFVarIds.isEmpty then
       return { discrs, matchType, altViews }
     else
       let ys := ysFVarIds.map mkFVar
       let matchType' ← forallBoundedTelescope matchType discrs.size fun ds type => do
         let type ← mkForallFVars ys type
-        let (discrs', ds') := Array.unzip <| Array.zip discrs ds |>.filter fun (di, d) => di.isFVar
+        let (discrs', ds') := Array.unzip <| Array.zip discrExprs ds |>.filter fun (di, d) => di.isFVar
         let type := type.replaceFVars discrs' ds'
         mkForallFVars ds type
       if (← isTypeCorrect matchType') then
-        let discrs := discrs ++ ys
+        let discrs := discrs ++  ys.map fun y => { expr := y : Discr }
         let altViews ← altViews.mapM fun altView => do
           let patternVars ← getPatternsVars altView.patterns
           -- We traverse backwards because we want to keep the most recent names.
@@ -882,27 +892,27 @@ private def generalize (discrs : Array Expr) (matchType : Expr) (altViews : Arra
         return { discrs, matchType, altViews }
 
 
-private partial def elabMatchAltViews (generalizing? : Option Bool) (discrs : Array Expr) (matchType : Expr) (altViews : Array MatchAltView) : TermElabM (Array Expr × Expr × Array (AltLHS × Expr) × Bool) := do
+private partial def elabMatchAltViews (generalizing? : Option Bool) (discrs : Array Discr) (matchType : Expr) (altViews : Array MatchAltView) : TermElabM (Array Discr × Expr × Array (AltLHS × Expr) × Bool) := do
   loop discrs #[] matchType altViews none
 where
   /-
     "Discriminant refinement" main loop.
     `first?` contains the first error message we found before updated the `discrs`. -/
-  loop (discrs : Array Expr) (toClear : Array FVarId) (matchType : Expr) (altViews : Array MatchAltView) (first? : Option (SavedState × Exception))
-      : TermElabM (Array Expr × Expr × Array (AltLHS × Expr) × Bool) := do
+  loop (discrs : Array Discr) (toClear : Array FVarId) (matchType : Expr) (altViews : Array MatchAltView) (first? : Option (SavedState × Exception))
+      : TermElabM (Array Discr × Expr × Array (AltLHS × Expr) × Bool) := do
     let s ← saveState
     let { discrs := discrs', toClear := toClear', matchType := matchType', altViews := altViews', refined } ← generalize discrs matchType altViews generalizing?
-    match (← altViews'.mapM (fun altView => elabMatchAltView altView matchType' (toClear ++ toClear')) |>.run) with
+    match (← altViews'.mapM (fun altView => elabMatchAltView discrs' altView matchType' (toClear ++ toClear')) |>.run) with
     | Except.ok alts => return (discrs', matchType', alts, first?.isSome || refined)
     | Except.error { patternIdx := patternIdx, pathToIndex := pathToIndex, ex := ex } =>
-      let some index ← getIndexToInclude? discrs[patternIdx] pathToIndex
+      let some index ← getIndexToInclude? discrs[patternIdx].expr pathToIndex
         | throwEx (← updateFirst first? ex)
       trace[Elab.match] "index to include: {index}"
-      if (← discrs.anyM fun discr => isDefEq discr index) then
+      if (← discrs.anyM fun discr => isDefEq discr.expr index) then
         throwEx (← updateFirst first? ex)
       let first ← updateFirst first? ex
       s.restore (restoreInfo := true)
-      let indices ← collectDeps #[index] discrs
+      let indices ← collectDeps #[index] (discrs.map (·.expr))
       let matchType ←
         try
           updateMatchType indices matchType
@@ -921,7 +931,7 @@ where
         else
           return mkHole ref
       let altViews  := altViews.map fun altView => { altView with patterns := wildcards ++ altView.patterns }
-      let discrs    := indices ++ discrs
+      let discrs    := (indices.map fun i => { expr := i : Discr }) ++ discrs
       let indexFVarIds := indices.filterMap fun | .fvar fvarId .. => some fvarId | _  => none
       loop discrs (toClear ++ indexFVarIds) matchType altViews first
 
@@ -1086,12 +1096,12 @@ private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax
   else
     let numDiscrs := discrs.size
     let matcherName ← mkAuxName `match
-    let matcherResult ← mkMatcher { matcherName, matchType, numDiscrs, lhss := altLHSS }
+    let matcherResult ← mkMatcher { matcherName, matchType, discrInfos := discrs.map fun discr => { hName? := discr.h?.map (·.getId) }, lhss := altLHSS }
     matcherResult.addMatcher
     let motive ← forallBoundedTelescope matchType numDiscrs fun xs matchType => mkLambdaFVars xs matchType
     reportMatcherResultErrors altLHSS matcherResult
     let r := mkApp matcherResult.matcher motive
-    let r := mkAppN r discrs
+    let r := mkAppN r (discrs.map (·.expr))
     let r := mkAppN r rhss
     trace[Elab.match] "result: {r}"
     return r

stage0/src/Lean/Elab/Tactic/Match.lean

@@ -15,6 +15,7 @@ structure AuxMatchTermState where
   nextIdx : Nat := 1
   «cases» : Array Syntax := #[]
 
+open Parser.Tactic in
 private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : StateT AuxMatchTermState MacroM Syntax := do
   let matchAlts := matchTac[5]
   let alts      := matchAlts[0].getArgs
@@ -33,7 +34,11 @@ private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : Sta
     else withFreshMacroScope do
       let newHole ← `(?rhs)
       let newHoleId := newHole[1]
-      let newCase ← `(tactic| case $newHoleId =>%$(alt[2]) ($holeOrTacticSeq:tacticSeq) )
+      let newCase ← `(tactic|
+        case $newHoleId =>%$(alt[2])
+          -- annotate `| ... =>` with state after `case`
+          with_annotate_state $(mkNullNode #[alt[0], alt[2]]) skip
+          $holeOrTacticSeq)
       modify fun s => { s with cases := s.cases.push newCase }
       pure <| alt.setArg 3 newHole
   let result  := matchTac.setKind ``Parser.Term.«match»

stage0/src/Lean/Meta/Eqns.lean

@@ -80,7 +80,7 @@ private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
   By default, we not create equation theorems for nonrecursive definitions.
   You can use `nonRec := true` to override this behavior, a dummy `rfl` proof is created on the fly.
 -/
-def getEqnsFor? (declName : Name) (nonRec := false) : MetaM (Option (Array Name)) := do
+def getEqnsFor? (declName : Name) (nonRec := false) : MetaM (Option (Array Name)) := withLCtx {} {} do
   if let some eqs := eqnsExt.getState (← getEnv) |>.map.find? declName then
     return some eqs
   else if (← shouldGenerateEqnThms declName) then
@@ -134,7 +134,7 @@ def registerGetUnfoldEqnFn (f : GetUnfoldEqnFn) : IO Unit := do
   By default, we not create unfold theorems for nonrecursive definitions.
   You can use `nonRec := true` to override this behavior.
 -/
-def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) := do
+def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) := withLCtx {} {} do
   if (← shouldGenerateEqnThms declName) then
     for f in (← getUnfoldEqnFnsRef.get) do
       if let some r ← f declName then

stage0/src/Lean/Meta/IndPredBelow.lean

@@ -437,7 +437,7 @@ partial def mkBelowMatcher
   withExistingLocalDecls (lhss.foldl (init := []) fun s v => s ++ v.fvarDecls) do
     for lhs in lhss do
       trace[Meta.IndPredBelow.match] "{lhs.patterns.map (·.toMessageData)}"
-  let res ← Match.mkMatcher { matcherName, matchType, numDiscrs := (mkMatcherInput.numDiscrs + 1), lhss }
+  let res ← Match.mkMatcher { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
   res.addMatcher
   -- if a wrong index is picked, the resulting matcher can be type-incorrect.
   -- we check here, so that errors can propagate higher up the call stack.

stage0/src/Lean/Meta/Match/Match.lean

@@ -17,21 +17,37 @@ import Lean.Meta.Match.CaseValues
 
 namespace Lean.Meta.Match
 
-/- The number of patterns in each AltLHS must be equal to majors.length -/
-private def checkNumPatterns (majors : Array Expr) (lhss : List AltLHS) : MetaM Unit := do
-  let num := majors.size
-  if lhss.any fun lhs => lhs.patterns.length != num then
+/-- The number of patterns in each AltLHS must be equal to the number of discriminants. -/
+private def checkNumPatterns (numDiscrs : Nat) (lhss : List AltLHS) : MetaM Unit := do
+  if lhss.any fun lhs => lhs.patterns.length != numDiscrs then
     throwError "incorrect number of patterns"
 
-/- Given a list of `AltLHS`, create a minor premise for each one, convert them into `Alt`, and then execute `k` -/
-private def withAlts {α} (motive : Expr) (lhss : List AltLHS) (k : List Alt → Array (Expr × Nat) → MetaM α) : MetaM α :=
+/--
+  Execute `k hs` where `hs` contains new equalities `h : lhs[i] = rhs[i]` for each `discrInfos[i] = some h`.
+  Assume `lhs.size == rhs.size == discrInfos.size`
+-/
+private partial def withEqs (lhs rhs : Array Expr) (discrInfos : Array DiscrInfo) (k : Array Expr → MetaM α) : MetaM α := do
+  go 0 #[]
+where
+  go (i : Nat) (hs : Array Expr) : MetaM α := do
+    if h : i < lhs.size then
+      if let some hName := discrInfos[i].hName? then
+        withLocalDeclD hName (← mkEq lhs[i] rhs[i]) fun h =>
+          go (i+1) (hs.push h)
+      else
+        go (i+1) hs
+    else
+      k hs
+/-- Given a list of `AltLHS`, create a minor premise for each one, convert them into `Alt`, and then execute `k` -/
+private def withAlts {α} (motive : Expr) (discrs : Array Expr) (discrInfos : Array DiscrInfo) (lhss : List AltLHS) (k : List Alt → Array (Expr × Nat) → MetaM α) : MetaM α :=
   loop lhss [] #[]
 where
   mkMinorType (xs : Array Expr) (lhs : AltLHS) : MetaM Expr :=
     withExistingLocalDecls lhs.fvarDecls do
       let args ← lhs.patterns.toArray.mapM (Pattern.toExpr · (annotate := true))
       let minorType := mkAppN motive args
-      mkForallFVars xs minorType
+      withEqs discrs args discrInfos fun eqs => do
+        mkForallFVars (xs ++ eqs) minorType
 
   loop (lhss : List AltLHS) (alts : List Alt) (minors : Array (Expr × Nat)) : MetaM α := do
     match lhss with
@@ -39,12 +55,13 @@ where
     | lhs::lhss =>
       let xs := lhs.fvarDecls.toArray.map LocalDecl.toExpr
       let minorType ← mkMinorType xs lhs
-      let (minorType, minorNumParams) := if !xs.isEmpty then (minorType, xs.size) else (mkSimpleThunkType minorType, 1)
+      let hasParams := !xs.isEmpty || discrInfos.any fun info => info.hName?.isSome
+      let (minorType, minorNumParams) := if hasParams then (minorType, xs.size) else (mkSimpleThunkType minorType, 1)
       let idx       := alts.length
       let minorName := (`h).appendIndexAfter (idx+1)
       trace[Meta.Match.debug] "minor premise {minorName} : {minorType}"
       withLocalDeclD minorName minorType fun minor => do
-        let rhs    := if xs.isEmpty then mkApp minor (mkConst `Unit.unit) else mkAppN minor xs
+        let rhs    := if hasParams then mkAppN minor xs else mkApp minor (mkConst `Unit.unit)
         let minors := minors.push (minor, minorNumParams)
         let fvarDecls ← lhs.fvarDecls.mapM instantiateLocalDeclMVars
         let alts   := { ref := lhs.ref, idx := idx, rhs := rhs, fvarDecls := fvarDecls, patterns := lhs.patterns : Alt } :: alts
@@ -713,7 +730,7 @@ builtin_initialize matcherExt : EnvExtension (Std.PHashMap (Expr × Bool) Name)
 
 /- Similar to `mkAuxDefinition`, but uses the cache `matcherExt`.
    It also returns an Boolean that indicates whether a new matcher function was added to the environment or not. -/
-def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (Expr × (Option $ MatcherInfo → MetaM Unit)) := do
+def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (Expr × Option (MatcherInfo → MetaM Unit)) := do
   trace[Meta.Match.debug] "{name} : {type} := {value}"
   let compile := bootstrap.genMatcherCode.get (← getOptions)
   let result ← Closure.mkValueTypeClosure type value (zeta := false)
@@ -743,11 +760,14 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
 
 structure MkMatcherInput where
   matcherName : Name
-  matchType : Expr
-  numDiscrs : Nat
-  lhss : List Match.AltLHS
+  matchType   : Expr
+  discrInfos  : Array DiscrInfo
+  lhss        : List Match.AltLHS
 
-/-
+def MkMatcherInput.numDiscrs (m : MkMatcherInput) :=
+  m.discrInfos.size
+
+/--
 Create a dependent matcher for `matchType` where `matchType` is of the form
 `(a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> B[a_1, ..., a_n]`
 where `n = numDiscrs`, and the `lhss` are the left-hand-sides of the `match`-expression alternatives.
@@ -756,29 +776,21 @@ The number of patterns must be the same in each `AltLHS`.
 The generated matcher has the structure described at `MatcherInfo`. The motive argument is of the form
 `(motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v)`
 where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition. -/
-def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult :=
-  let ⟨matcherName, matchType, numDiscrs, lhss⟩ := input
-  forallBoundedTelescope matchType numDiscrs fun majors matchTypeBody => do
-  checkNumPatterns majors lhss
+def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := do
+  let ⟨matcherName, matchType, discrInfos, lhss⟩ := input
+  let numDiscrs := discrInfos.size
+  let numEqs := getNumEqsFromDiscrInfos discrInfos
+  checkNumPatterns numDiscrs lhss
+  forallBoundedTelescope matchType numDiscrs fun discrs matchTypeBody => do
   /- We generate an matcher that can eliminate using different motives with different universe levels.
      `uElim` is the universe level the caller wants to eliminate to.
      If it is not levelZero, we create a matcher that can eliminate in any universe level.
      This is useful for implementing `MatcherApp.addArg` because it may have to change the universe level. -/
   let uElim ← getLevel matchTypeBody
   let uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar
-  let motiveType ← mkForallFVars majors (mkSort uElimGen)
-  withLocalDeclD `motive motiveType fun motive => do
-  trace[Meta.Match.debug] "motiveType: {motiveType}"
-  let mvarType  := mkAppN motive majors
-  trace[Meta.Match.debug] "target: {mvarType}"
-  withAlts motive lhss fun alts minors => do
-    let mvar ← mkFreshExprMVar mvarType
-    let examples := majors.toList.map fun major => Example.var major.fvarId!
-    let (_, s) ← (process { mvarId := mvar.mvarId!, vars := majors.toList, alts := alts, examples := examples }).run {}
-    let args := #[motive] ++ majors ++ minors.map Prod.fst
-    let type ← mkForallFVars args mvarType
-    let val  ← mkLambdaFVars args mvar
+  let mkMatcher (type val : Expr) (minors : Array (Expr × Nat)) (s : State) : MetaM MatcherResult := do
     trace[Meta.Match.debug] "matcher value: {val}\ntype: {type}"
+    trace[Meta.Match.debug] "minors num params: {minors.map (·.2)}"
     /- The option `bootstrap.gen_matcher_code` is a helper hack. It is useful, for example,
        for compiling `src/Init/Data/Int`. It is needed because the compiler uses `Int.decLt`
        for generating code for `Int.casesOn` applications, but `Int.casesOn` is used to
@@ -797,22 +809,57 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult :=
     discard <| isLevelDefEq uElimGen uElim
     let addMatcher :=
       match addMatcher with
-      | some addMatcher =>
+      | some addMatcher => addMatcher <|
         { numParams := matcher.getAppNumArgs
-          numDiscrs,
-          altNumParams := minors.map Prod.snd,
-          uElimPos? }
-        |> addMatcher
+          altNumParams := minors.map fun minor => minor.2 + numEqs
+          discrInfos
+          numDiscrs
+          uElimPos?
+          }
       | none => pure ()
 
     trace[Meta.Match.debug] "matcher: {matcher}"
     let unusedAltIdxs := lhss.length.fold (init := []) fun i r =>
       if s.used.contains i then r else i::r
-    pure {
+    return {
       matcher,
       counterExamples := s.counterExamples,
       unusedAltIdxs := unusedAltIdxs.reverse,
-      addMatcher }
+      addMatcher
+    }
+
+  let motiveType ← mkForallFVars discrs (mkSort uElimGen)
+  trace[Meta.Match.debug] "motiveType: {motiveType}"
+  withLocalDeclD `motive motiveType fun motive => do
+  if discrInfos.any fun info => info.hName?.isSome then
+    forallBoundedTelescope matchType numDiscrs fun discrs' matchTypeBody => do
+    let mvarType ← withEqs discrs discrs' discrInfos fun eqs => mkForallFVars eqs (mkAppN motive discrs')
+    trace[Meta.Match.debug] "target: {mvarType}"
+    withAlts motive discrs discrInfos lhss fun alts minors => do
+      let mvar ← mkFreshExprMVar mvarType
+      trace[Meta.Match.debug] "goal\n{mvar.mvarId!}"
+      let examples := discrs.toList.map fun discr => Example.var discr.fvarId!
+      let (_, s) ← (process { mvarId := mvar.mvarId!, vars := discrs'.toList, alts := alts, examples := examples }).run {}
+      let val ← mkLambdaFVars discrs' mvar
+      trace[Meta.Match.debug] "matcher\nvalue: {val}\ntype: {← inferType val}"
+      let rfls ← (discrs.zip discrInfos).filterMapM fun (discr, info) =>
+        if info.hName?.isNone then return none else return some (← mkEqRefl discr)
+      let val := mkAppN (mkAppN val discrs) rfls
+      let args := #[motive] ++ discrs ++ minors.map Prod.fst
+      let val ← mkLambdaFVars args val
+      let type ← mkForallFVars args (mkAppN motive discrs)
+      mkMatcher type val minors s
+  else
+    let mvarType  := mkAppN motive discrs
+    trace[Meta.Match.debug] "target: {mvarType}"
+    withAlts motive discrs discrInfos lhss fun alts minors => do
+      let mvar ← mkFreshExprMVar mvarType
+      let examples := discrs.toList.map fun discr => Example.var discr.fvarId!
+      let (_, s) ← (process { mvarId := mvar.mvarId!, vars := discrs.toList, alts := alts, examples := examples }).run {}
+      let args := #[motive] ++ discrs ++ minors.map Prod.fst
+      let type ← mkForallFVars args mvarType
+      let val  ← mkLambdaFVars args mvar
+      mkMatcher type val minors s
 
 def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput := do
   let matcherName := matcherApp.matcherName
@@ -843,7 +890,7 @@ def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput
       fvarDecls := localDecls.toList
       patterns := patterns.toList : Match.AltLHS }
 
-  return { matcherName, matchType, numDiscrs := matcherApp.discrs.size, lhss }
+  return { matcherName, matchType, discrInfos := mkArray matcherApp.discrs.size {}, lhss }
 
 
 def withMkMatcherInput

stage0/src/Lean/Meta/Match/MatchEqs.lean

@@ -62,43 +62,60 @@ def unfoldNamedPattern (e : Expr) : MetaM Expr := do
   Meta.transform e (pre := visit)
 
 /--
-  Similar to `forallTelescopeReducing`, but eliminates arguments for named parameters and the associated
-  equation proofs. The continuation `k` takes four arguments `ys args mask type`.
+  Similar to `forallTelescopeReducing`, but
+
+  1. Eliminates arguments for named parameters and the associated equation proofs.
+
+  2. Equality parameters associated with the `h : discr` notation are replaced with `rfl` proofs.
+     Recall that this kind of parameter always occurs after the parameters correspoting to pattern variables.
+     `numNonEqParams` is the size of the prefix.
+
+  The continuation `k` takes four arguments `ys args mask type`.
   - `ys` are variables for the hypotheses that have not been eliminated.
+  - `eqs` are variables for equality hypotheses associated with discriminants annotated with `h : discr`.
   - `args` are the arguments for the alternative `alt` that has type `altType`. `ys.size <= args.size`
   - `mask[i]` is true if the hypotheses has not been eliminated. `mask.size == args.size`.
   - `type` is the resulting type for `altType`.
 
   We use the `mask` to build the splitter proof. See `mkSplitterProof`.
 -/
-partial def forallAltTelescope (altType : Expr) (k : Array Expr → Array Expr → Array Bool → Expr → MetaM α) : MetaM α := do
-  go #[] #[] #[] altType
+partial def forallAltTelescope (altType : Expr) (numNonEqParams : Nat)
+    (k : (ys : Array Expr) → (eqs : Array Expr) → (args : Array Expr) → (mask : Array Bool) → (type : Expr) → MetaM α)
+    : MetaM α := do
+  go #[] #[] #[] #[] 0 altType
 where
-  go (ys : Array Expr) (args : Array Expr) (mask : Array Bool) (type : Expr) : MetaM α := do
+  go (ys : Array Expr) (eqs : Array Expr) (args : Array Expr) (mask : Array Bool) (i : Nat) (type : Expr) : MetaM α := do
     let type ← whnfForall type
     match type with
     | Expr.forallE n d b .. =>
-      let d ← unfoldNamedPattern d
-      withLocalDeclD n d fun y => do
-        let typeNew := b.instantiate1 y
-        if let some (_, lhs, rhs) ← matchEq? d then
-          if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then
-             let some i  := ys.getIdx? lhs | unreachable!
-             let ys      := ys.eraseIdx i
-             let mask    := mask.set! i false
-             let args    := args.map fun arg => if arg == lhs then rhs else arg
-             let args    := args.push (← mkEqRefl rhs)
-             let typeNew := typeNew.replaceFVar lhs rhs
-             return (← go ys args (mask.push false) typeNew)
-        go (ys.push y) (args.push y) (mask.push true) typeNew
+      if i < numNonEqParams then
+        let d ← unfoldNamedPattern d
+        withLocalDeclD n d fun y => do
+          let typeNew := b.instantiate1 y
+          if let some (_, lhs, rhs) ← matchEq? d then
+            if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then
+               let some i  := ys.getIdx? lhs | unreachable!
+               let ys      := ys.eraseIdx i
+               let mask    := mask.set! i false
+               let args    := args.map fun arg => if arg == lhs then rhs else arg
+               let args    := args.push (← mkEqRefl rhs)
+               let typeNew := typeNew.replaceFVar lhs rhs
+               return (← go ys eqs args (mask.push false) (i+1) typeNew)
+          go (ys.push y) eqs (args.push y) (mask.push true) (i+1) typeNew
+      else
+        let some (_, _, rhs) ← matchEq? d | throwError "unexpected match alternative type{indentExpr altType}"
+        let arg ← mkEqRefl rhs
+        withLocalDeclD n d fun eq => do
+          let typeNew := b.instantiate1 eq
+          go ys (eqs.push eq) (args.push arg) (mask.push false) (i+1) typeNew
     | _ =>
       let type ← unfoldNamedPattern type
       /- Recall that alternatives that do not have variables have a `Unit` parameter to ensure
          they are not eagerly evaluated. -/
       if ys.size == 1 then
         if (← inferType ys[0]).isConstOf ``Unit && !(← dependsOn type ys[0].fvarId!) then
-          return (← k #[] #[mkConst ``Unit.unit] #[false] type)
-      k ys args mask type
+          return (← k #[] #[] #[mkConst ``Unit.unit] #[false] type)
+      k ys eqs args mask type
 
   isNamedPatternProof (type : Expr) (h : Expr) : Bool :=
     Option.isSome <| type.find? fun e =>
@@ -258,16 +275,17 @@ private def substSomeVar (mvarId : MVarId) : MetaM (Array MVarId) := withMVarCon
 /--
   Helper method for proving a conditional equational theorem associated with an alternative of
   the `match`-eliminator `matchDeclName`. `type` contains the type of the theorem. -/
-partial def proveCondEqThm (matchDeclName : Name) (type : Expr) : MetaM Expr := do
+partial def proveCondEqThm (matchDeclName : Name) (type : Expr) : MetaM Expr := withLCtx {} {} do
   let type ← instantiateMVars type
-  withLCtx {} {} <| forallTelescope type fun ys target => do
+  forallTelescope type fun ys target => do
     let mvar0  ← mkFreshExprSyntheticOpaqueMVar target
+    trace[Meta.Match.matchEqs] "proveCondEqThm {mvar0.mvarId!}"
     let mvarId ← deltaTarget mvar0.mvarId! (· == matchDeclName)
-    trace[Meta.Match.matchEqs] "{MessageData.ofGoal mvarId}"
     withDefault <| go mvarId 0
     mkLambdaFVars ys (← instantiateMVars mvar0)
 where
   go (mvarId : MVarId) (depth : Nat) : MetaM Unit := withIncRecDepth do
+    trace[Meta.Match.matchEqs] "proveCondEqThm.go {mvarId}"
     let mvarId' ← modifyTargetEqLHS mvarId whnfCore
     let mvarId := mvarId'
     let subgoals ←
@@ -341,6 +359,7 @@ private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult :=
   - `altNews` are the new free variables which contains aditional hypotheses that ensure they are only used
      when the previous overlapping alternatives are not applicable. -/
 private partial def mkSplitterProof (matchDeclName : Name) (template : Expr) (alts altsNew : Array Expr)
+    (altsNewNumParams : Array Nat)
     (altArgMasks : Array (Array Bool)) : MetaM Expr := do
   trace[Meta.Match.matchEqs] "proof template: {template}"
   let map := mkMap
@@ -350,25 +369,26 @@ private partial def mkSplitterProof (matchDeclName : Name) (template : Expr) (al
     proveSubgoal mvarId
   instantiateMVars proof
 where
-  mkMap : FVarIdMap (Expr × Array Bool) := Id.run do
+  mkMap : FVarIdMap (Expr × Nat × Array Bool) := Id.run do
     let mut m := {}
-    for alt in alts, altNew in altsNew, argMask in altArgMasks do
-      m := m.insert alt.fvarId! (altNew, argMask)
+    for alt in alts, altNew in altsNew, numParams in altsNewNumParams, argMask in altArgMasks do
+      m := m.insert alt.fvarId! (altNew, numParams, argMask)
     return m
 
-  convertTemplate (m : FVarIdMap (Expr × Array Bool)) : StateRefT (Array MVarId) MetaM Expr :=
+  convertTemplate (m : FVarIdMap (Expr × Nat × Array Bool)) : StateRefT (Array MVarId) MetaM Expr :=
     transform template fun e => do
       match e.getAppFn with
       | Expr.fvar fvarId .. =>
         match m.find? fvarId with
-        | some (altNew, argMask) =>
+        | some (altNew, numParams, argMask) =>
           trace[Meta.Match.matchEqs] ">> {e}, {altNew}"
           let mut newArgs := #[]
           for arg in e.getAppArgs, includeArg in argMask do
             if includeArg then
               newArgs := newArgs.push arg
           let eNew := mkAppN altNew newArgs
-          let (mvars, _, _) ← forallMetaTelescopeReducing (← inferType eNew) (kind := MetavarKind.syntheticOpaque)
+          /- Recall that `numParams` does not include the equalities associated with discriminants of the form `h : discr`. -/
+          let (mvars, _, _) ← forallMetaBoundedTelescope (← inferType eNew) (numParams - newArgs.size) (kind := MetavarKind.syntheticOpaque)
           modify fun s => s ++ (mvars.map (·.mvarId!))
           let eNew := mkAppN eNew mvars
           return TransformStep.done eNew
@@ -395,15 +415,37 @@ where
     let mvarId ← tryClearMany mvarId (alts.map (·.fvarId!))
     proveSubgoalLoop mvarId
 
+/--
+  Create new alternatives (aka minor premises) by replacing `discrs` with `patterns` at `alts`.
+  Recall that `alts` depends on `discrs` when `numDiscrEqs > 0`, where `numDiscrEqs` is the number of discriminants
+  annotated with `h : discr`.
+-/
+private partial def withNewAlts (numDiscrEqs : Nat) (discrs : Array Expr) (patterns : Array Expr) (alts : Array Expr) (k : Array Expr → MetaM α) : MetaM α :=
+  if numDiscrEqs == 0 then
+    k alts
+  else
+    go 0 #[]
+where
+  go (i : Nat) (altsNew : Array Expr) : MetaM α := do
+   if h : i < alts.size then
+     let alt := alts.get ⟨i, h⟩
+     let altLocalDecl ← getFVarLocalDecl alt
+     let typeNew := altLocalDecl.type.replaceFVars discrs patterns
+     withLocalDecl altLocalDecl.userName altLocalDecl.binderInfo typeNew fun altNew =>
+       go (i+1) (altsNew.push altNew)
+   else
+     k altsNew
+
 /--
   Create conditional equations and splitter for the given match auxiliary declaration. -/
-private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns := do
+private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns := withLCtx {} {} do
   trace[Meta.Match.matchEqs] "mkEquationsFor '{matchDeclName}'"
   withConfig (fun c => { c with etaStruct := .none }) do
   let baseName := mkPrivateName (← getEnv) matchDeclName
   let constInfo ← getConstInfo matchDeclName
   let us := constInfo.levelParams.map mkLevelParam
   let some matchInfo ← getMatcherInfo? matchDeclName | throwError "'{matchDeclName}' is not a matcher function"
+  let numDiscrEqs := getNumEqsFromDiscrInfos matchInfo.discrInfos
   forallTelescopeReducing constInfo.type fun xs matchResultType => do
     let mut eqnNames := #[]
     let params := xs[:matchInfo.numParams]
@@ -416,10 +458,12 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
     let mut splitterAltTypes := #[]
     let mut splitterAltNumParams := #[]
     let mut altArgMasks := #[] -- masks produced by `forallAltTelescope`
-    for alt in alts do
+    for i in [:alts.size] do
+      let altNumParams := matchInfo.altNumParams[i]
+      let altNonEqNumParams := altNumParams - numDiscrEqs
       let thmName := baseName ++ ((`eq).appendIndexAfter idx)
       eqnNames := eqnNames.push thmName
-      let (notAlt, splitterAltType, splitterAltNumParam, argMask) ← forallAltTelescope (← inferType alt) fun ys rhsArgs argMask altResultType => do
+      let (notAlt, splitterAltType, splitterAltNumParam, argMask) ← forallAltTelescope (← inferType alts[i]) altNonEqNumParams fun ys eqs rhsArgs argMask altResultType => do
         let patterns := altResultType.getAppArgs
         let mut hs := #[]
         for notAlt in notAlts do
@@ -427,7 +471,7 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
           if let some h ← simpH? h patterns.size then
             hs := hs.push h
         trace[Meta.Match.matchEqs] "hs: {hs}"
-        let splitterAltType ← mkForallFVars ys (← hs.foldrM (init := altResultType) mkArrow)
+        let splitterAltType ← mkForallFVars ys (← hs.foldrM (init := (← mkForallFVars eqs altResultType)) mkArrow)
         let splitterAltNumParam := hs.size + ys.size
         -- Create a proposition for representing terms that do not match `patterns`
         let mut notAlt := mkConst ``False
@@ -437,20 +481,24 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
           else
             notAlt ← mkArrow (← mkHEq discr pattern) notAlt
         notAlt ← mkForallFVars (discrs ++ ys) notAlt
-        let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts)
-        let rhs := mkAppN alt rhsArgs
-        let thmType ← mkEq lhs rhs
-        let thmType ← hs.foldrM (init := thmType) mkArrow
-        let thmType ← mkForallFVars (params ++ #[motive] ++ alts ++ ys) thmType
-        let thmType ← unfoldNamedPattern thmType
-        let thmVal ← proveCondEqThm matchDeclName thmType
-        addDecl <| Declaration.thmDecl {
-          name        := thmName
-          levelParams := constInfo.levelParams
-          type        := thmType
-          value       := thmVal
-        }
-        return (notAlt, splitterAltType, splitterAltNumParam, argMask)
+        /- Recall that when we use the `h : discr`, the alternative type depends on the discriminant.
+           Thus, we need to create new `alts`. -/
+        withNewAlts numDiscrEqs discrs patterns alts fun alts => do
+          let alt := alts[i]
+          let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts)
+          let rhs := mkAppN alt rhsArgs
+          let thmType ← mkEq lhs rhs
+          let thmType ← hs.foldrM (init := thmType) mkArrow
+          let thmType ← mkForallFVars (params ++ #[motive] ++ ys ++ alts) thmType
+          let thmType ← unfoldNamedPattern thmType
+          let thmVal ← proveCondEqThm matchDeclName thmType
+          addDecl <| Declaration.thmDecl {
+            name        := thmName
+            levelParams := constInfo.levelParams
+            type        := thmType
+            value       := thmVal
+          }
+          return (notAlt, splitterAltType, splitterAltNumParam, argMask)
       notAlts := notAlts.push notAlt
       splitterAltTypes := splitterAltTypes.push splitterAltType
       splitterAltNumParams := splitterAltNumParams.push splitterAltNumParam
@@ -464,7 +512,8 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
       trace[Meta.Match.matchEqs] "splitterType: {splitterType}"
       let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
       let template ← deltaExpand template (· == constInfo.name)
-      let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew altArgMasks)
+      let template := template.headBeta
+      let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltNumParams altArgMasks)
       let splitterName := baseName ++ `splitter
       addDecl <| Declaration.thmDecl {
         name        := splitterName

stage0/src/Lean/Meta/Match/MatcherInfo.lean

@@ -8,6 +8,11 @@ import Lean.Meta.Basic
 namespace Lean.Meta
 namespace Match
 
+structure DiscrInfo where
+  /-- `some h` if the discriminant is annotated with `h:` -/
+  hName? : Option Name := none
+  deriving Inhabited
+
 /--
 A "matcher" auxiliary declaration has the following structure:
 - `numParams` parameters
@@ -18,10 +23,14 @@ A "matcher" auxiliary declaration has the following structure:
    `pos` is the position of the universe level parameter that specifies the elimination universe.
    It is `none` if the matcher only eliminates into `Prop`. -/
 structure MatcherInfo where
-  numParams : Nat
-  numDiscrs : Nat
+  numParams    : Nat
+  numDiscrs    : Nat
   altNumParams : Array Nat
-  uElimPos? : Option Nat
+  uElimPos?    : Option Nat
+  /--
+    `discrInfos[i] = { hName? := some h }` if the i-th discriminant was annotated with `h :`.
+  -/
+  discrInfos   : Array DiscrInfo
 
 def MatcherInfo.numAlts (info : MatcherInfo) : Nat :=
   info.altNumParams.size
@@ -38,6 +47,16 @@ def MatcherInfo.getFirstAltPos (info : MatcherInfo) : Nat :=
 def MatcherInfo.getMotivePos (info : MatcherInfo) : Nat :=
   info.numParams
 
+def getNumEqsFromDiscrInfos (infos : Array DiscrInfo) : Nat := Id.run do
+  let mut r := 0
+  for info in infos do
+    if info.hName?.isSome then
+      r := r + 1
+  return r
+
+def MatcherInfo.getNumDiscrEqs (info : MatcherInfo) : Nat :=
+  getNumEqsFromDiscrInfos info.discrInfos
+
 namespace Extension
 
 structure Entry where

stage0/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -76,7 +76,6 @@ mutual
 end
 
 def isRflProof (proof : Expr) : MetaM Bool := do
-  trace[Meta.debug] "isRflProof: {proof}"
   if let .const declName .. := proof then
     isRflTheorem declName
   else
@@ -383,17 +382,16 @@ where
       else
         return none
 
-def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM SimpTheorems :=
-  withLCtx {} {} do
-    if let some eqns ← getEqnsFor? declName then
-      let mut d := d
-      for eqn in eqns do
-        d ← SimpTheorems.addConst d eqn
-      if hasSmartUnfoldingDecl (← getEnv) declName then
-        d := d.addDeclToUnfoldCore declName
-      return d
-    else
-      return d.addDeclToUnfoldCore declName
+def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM SimpTheorems := do
+  if let some eqns ← getEqnsFor? declName then
+    let mut d := d
+    for eqn in eqns do
+      d ← SimpTheorems.addConst d eqn
+    if hasSmartUnfoldingDecl (← getEnv) declName then
+      d := d.addDeclToUnfoldCore declName
+    return d
+  else
+    return d.addDeclToUnfoldCore declName
 
 abbrev SimpTheoremsArray := Array SimpTheorems
 

stage0/src/Lean/Parser/Term.lean

@@ -144,7 +144,7 @@ def matchAltExpr := matchAlt
 def matchAlts (rhsParser : Parser := termParser) : Parser :=
   leading_parser withPosition $ many1Indent (ppLine >> matchAlt rhsParser)
 
-def matchDiscr := leading_parser optional (atomic (ident >> ":")) >> termParser
+def matchDiscr := leading_parser optional (atomic (ident >> " : ")) >> termParser
 
 def trueVal  := leading_parser nonReservedSymbol "true"
 def falseVal := leading_parser nonReservedSymbol "false"

stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -383,27 +383,34 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
       return { matcherTy := (← getConstInfo c).instantiateTypeLevelParams us, info := info : AppMatchState })
     (fun st => do
       if st.params.size < st.info.numParams then
-        pure { st with params := st.params.push (← getExpr) }
+        return { st with params := st.params.push (← getExpr) }
       else if st.motive.isNone then
-         -- store motive argument separately
-         let lamMotive ← getExpr
-         let piMotive ← lambdaTelescope lamMotive fun xs body => mkForallFVars xs body
-         -- TODO: pp.analyze has not analyzed `piMotive`, only `lamMotive`
-         -- Thus the binder types won't have any annotations
-         let piStx ← withTheReader SubExpr (fun cfg => { cfg with expr := piMotive }) delab
-         let named ← getPPOption getPPAnalysisNamedArg
-         pure { st with motive := (piStx, lamMotive), motiveNamed := named }
+        -- store motive argument separately
+        let lamMotive ← getExpr
+        let piMotive ← lambdaTelescope lamMotive fun xs body => mkForallFVars xs body
+        -- TODO: pp.analyze has not analyzed `piMotive`, only `lamMotive`
+        -- Thus the binder types won't have any annotations
+        let piStx ← withTheReader SubExpr (fun cfg => { cfg with expr := piMotive }) delab
+        let named ← getPPOption getPPAnalysisNamedArg
+        return { st with motive := (piStx, lamMotive), motiveNamed := named }
       else if st.discrs.size < st.info.numDiscrs then
-        pure { st with discrs := st.discrs.push (← delab) }
+        let idx := st.discrs.size
+        let discr ← delab
+        if let some hName := st.info.discrInfos[idx].hName? then
+          -- TODO: we should check whether the corresponding binder name, matches `hName`.
+          -- If it does not we should pretty print this `match` as a regular application.
+          return { st with discrs := st.discrs.push (← `(matchDiscr| $(mkIdent hName):ident : $discr:term)) }
+        else
+          return { st with discrs := st.discrs.push (← `(matchDiscr| $discr:term)) }
       else if st.rhss.size < st.info.altNumParams.size then
         /- We save the variables names here to be able to implement safe_shadowing.
            The pattern delaboration must use the names saved here. -/
         let (varNames, rhs) ← skippingBinders st.info.altNumParams[st.rhss.size] fun varNames => do
           let rhs ← delab
           return (varNames, rhs)
-        pure { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames }
+        return { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames }
       else
-        pure { st with moreArgs := st.moreArgs.push (← delab) })
+        return { st with moreArgs := st.moreArgs.push (← delab) })
 
   if st.discrs.size < st.info.numDiscrs || st.rhss.size < st.info.altNumParams.size then
     -- underapplied
@@ -421,9 +428,9 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
       let opts ← getOptions
       -- TODO: disable the match if other implicits are needed?
       if ← pure st.motiveNamed <||> shouldShowMotive lamMotive opts then
-        `(match (motive := $piStx) $[$st.discrs:term],* with $[| $pats,* => $st.rhss]*)
+        `(match (motive := $piStx) $[$st.discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
       else
-        `(match $[$st.discrs:term],* with $[| $pats,* => $st.rhss]*)
+        `(match $[$st.discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
     return Syntax.mkApp stx st.moreArgs
 
 /--

stage0/src/Lean/PrettyPrinter/Formatter.lean

@@ -234,6 +234,8 @@ def categoryFormatterCore (cat : Name) : Formatter := do
       -- format only last choice
       -- TODO: We could use elaborator data here to format the chosen child when available
       formatterForKind (← getCur).getKind
+  else if cat == `rawStx then
+    withAntiquot.formatter (mkAntiquot.formatter' cat.toString none) (push stx.formatStx *> goLeft)
   else
     withAntiquot.formatter (mkAntiquot.formatter' cat.toString none) (formatterForKind stx.getKind)
   modify fun st => { st with mustBeGrouped := true, isUngrouped := !st.mustBeGrouped }

stage0/src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -350,6 +350,10 @@ def level.parenthesizer : CategoryParenthesizer | prec => do
   maybeParenthesize `level false (fun stx => Unhygienic.run `(level|($stx))) prec $
     parenthesizeCategoryCore `level prec
 
+@[builtinCategoryParenthesizer rawStx]
+def rawStx.parenthesizer : CategoryParenthesizer | _ => do
+  goLeft
+
 @[combinatorParenthesizer Lean.Parser.error]
 def error.parenthesizer (msg : String) : Parenthesizer :=
   pure ()

stage0/src/runtime/stack_overflow.cpp

@@ -73,7 +73,8 @@ bool is_within_stack_guard(void * addr) {
 
 extern "C" LEAN_EXPORT void segv_handler(int signum, siginfo_t * info, void *) {
     if (is_within_stack_guard(info->si_addr)) {
-        fprintf(stderr, "\nStack overflow detected. Aborting.\n");
+        char const msg[] = "\nStack overflow detected. Aborting.\n";
+        write(STDERR_FILENO, msg, sizeof(msg) - 1);
         abort();
     } else {
         // reset signal handler and return; see comments in Rust code

stage0/stdlib/Init/Data/Array/Subarray.c

@@ -25,6 +25,8 @@ lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__15;
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__18;
 static lean_object* l_Array_term_____x5b___x3a___x5d___closed__9;
+LEAN_EXPORT lean_object* l_Subarray_get_x21(lean_object*);
+LEAN_EXPORT lean_object* l_Subarray_getD___rarg___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Subarray_forInUnsafe_loop___at_Array_ofSubarray___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__5;
 LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Subarray_any___spec__1___rarg(lean_object*, lean_object*, size_t, size_t);
@@ -40,6 +42,7 @@ LEAN_EXPORT lean_object* l_Std_Format_joinSep___at_instReprSubarray___spec__1(le
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Subarray_forM___spec__1___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__2;
 LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Subarray_any___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Subarray_size___rarg___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Subarray_foldr(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__1;
@@ -58,6 +61,7 @@ static lean_object* l_Array_term_____x5b___x3a___x5d___closed__23;
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__14;
 LEAN_EXPORT lean_object* l_Subarray_forM(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
+LEAN_EXPORT lean_object* l_Subarray_getD(lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_instReprSubarray___rarg___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b_x3a___x5d__1(lean_object*, lean_object*, lean_object*);
@@ -81,10 +85,12 @@ static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__
 LEAN_EXPORT lean_object* l_Subarray_popFront(lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__13;
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__19;
+LEAN_EXPORT lean_object* l_Subarray_size(lean_object*);
 static lean_object* l_Array_term_____x5b___x3a___x5d___closed__12;
 LEAN_EXPORT lean_object* l_instReprSubarray___rarg(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Subarray_popFront___rarg(lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b_x3a___x5d__1___closed__2;
+lean_object* lean_array_fget(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Subarray_anyM(lean_object*, lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__6;
 LEAN_EXPORT lean_object* l_Subarray_all___rarg___boxed(lean_object*, lean_object*);
@@ -112,19 +118,23 @@ LEAN_EXPORT lean_object* l_Subarray_forInUnsafe(lean_object*, lean_object*, lean
 lean_object* l_Array_foldlMUnsafe_fold___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b_x3a___x5d__1___closed__1;
 static lean_object* l_instReprSubarray___rarg___closed__11;
+LEAN_EXPORT lean_object* l_Subarray_get_x21___rarg___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_term_____x5b___x3a___x5d;
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b_x3a___x5d__1___closed__4;
 LEAN_EXPORT lean_object* l_Subarray_forInUnsafe_loop___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_to_list(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Subarray_foldl___spec__1___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
+LEAN_EXPORT lean_object* l_Subarray_get(lean_object*);
 lean_object* l_List_toString___rarg(lean_object*, lean_object*);
 static lean_object* l_Array_term_____x5b___x3a___x5d___closed__11;
+LEAN_EXPORT lean_object* l_Subarray_get___rarg___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Subarray_foldl(lean_object*, lean_object*);
 static lean_object* l_Array_term_____x5b___x3a___x5d___closed__16;
 LEAN_EXPORT lean_object* l_Subarray_all(lean_object*);
 static lean_object* l_instReprSubarray___rarg___closed__6;
 LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Subarray_allM___spec__1___rarg___lambda__1(lean_object*, uint8_t);
 LEAN_EXPORT lean_object* l_Subarray_foldr___rarg(lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Subarray_getOp___rarg___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_ofSubarray(lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__13;
 static lean_object* l_Array_term_____x5b___x3a___x5d___closed__24;
@@ -133,6 +143,7 @@ static lean_object* l_Array_term_____x5b_x3a___x5d___closed__4;
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__6;
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__21;
 LEAN_EXPORT lean_object* l_Subarray_forInUnsafe_loop___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Subarray_getD___rarg(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Array_term_____x5b_x3a___x5d___closed__2;
 LEAN_EXPORT lean_object* l_Array_extract(lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__9;
@@ -150,6 +161,7 @@ LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Subarray_all___spec__1(lean
 LEAN_EXPORT lean_object* l_Subarray_foldrM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Array_term_____x5b___x3a___x5d___closed__7;
 static lean_object* l_Array_term_____x5b_x3a___x5d___closed__1;
+LEAN_EXPORT lean_object* l_Subarray_getOp(lean_object*);
 static lean_object* l_Array_term_____x5b___x3a___x5d___closed__20;
 static lean_object* l_instReprSubarray___rarg___closed__5;
 LEAN_EXPORT lean_object* l_instAppendSubarray___rarg(lean_object*, lean_object*);
@@ -162,6 +174,7 @@ static lean_object* l_instReprSubarray___rarg___closed__3;
 LEAN_EXPORT lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_instAppendSubarray(lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__12;
+LEAN_EXPORT lean_object* l_Subarray_get_x21___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__11;
 LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Subarray_forRevM___spec__2(lean_object*, lean_object*);
@@ -171,9 +184,11 @@ LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Subarray_allM___spec__1___r
 LEAN_EXPORT lean_object* l_Subarray_instForInSubarray(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__4;
 static lean_object* l_Array_term_____x5b_x3a___x5d___closed__6;
+LEAN_EXPORT lean_object* l_Subarray_getOp___rarg(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Subarray_forInUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_instToStringSubarray___rarg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Subarray_forRevM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Subarray_get___rarg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Subarray_foldr___spec__2(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_term_____x5b_x3a___x5d;
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__17;
@@ -216,6 +231,7 @@ static lean_object* l_instReprSubarray___rarg___closed__13;
 static lean_object* l_Array_term_____x5b___x3a___x5d___closed__18;
 static lean_object* l_Array_term_____x5b___x3a___x5d___closed__5;
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__11;
+LEAN_EXPORT lean_object* l_Subarray_size___rarg(lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__12;
 LEAN_EXPORT lean_object* l_Subarray_allM(lean_object*, lean_object*);
 static lean_object* l_Array_term_____x5b___x3a___x5d___closed__3;
@@ -230,6 +246,168 @@ static lean_object* l_Array_term_____x5b___x3a___x5d___closed__14;
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__9;
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Subarray_foldl___spec__1(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Subarray_size___rarg(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_2 = lean_ctor_get(x_1, 2);
+x_3 = lean_ctor_get(x_1, 1);
+x_4 = lean_nat_sub(x_2, x_3);
+return x_4;
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_size(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Subarray_size___rarg___boxed), 1, 0);
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_size___rarg___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Subarray_size___rarg(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_get___rarg(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
+x_3 = lean_ctor_get(x_1, 0);
+x_4 = lean_ctor_get(x_1, 1);
+x_5 = lean_nat_add(x_4, x_2);
+x_6 = lean_array_fget(x_3, x_5);
+lean_dec(x_5);
+return x_6;
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_get(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Subarray_get___rarg___boxed), 2, 0);
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_get___rarg___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Subarray_get___rarg(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_getD___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; uint8_t x_5; 
+x_4 = l_Subarray_size___rarg(x_1);
+x_5 = lean_nat_dec_lt(x_2, x_4);
+lean_dec(x_4);
+if (x_5 == 0)
+{
+lean_inc(x_3);
+return x_3;
+}
+else
+{
+lean_object* x_6; 
+x_6 = l_Subarray_get___rarg(x_1, x_2);
+return x_6;
+}
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_getD(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Subarray_getD___rarg___boxed), 3, 0);
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_getD___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Subarray_getD___rarg(x_1, x_2, x_3);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_4;
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_get_x21___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; uint8_t x_5; 
+x_4 = l_Subarray_size___rarg(x_2);
+x_5 = lean_nat_dec_lt(x_3, x_4);
+lean_dec(x_4);
+if (x_5 == 0)
+{
+lean_inc(x_1);
+return x_1;
+}
+else
+{
+lean_object* x_6; 
+x_6 = l_Subarray_get___rarg(x_2, x_3);
+return x_6;
+}
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_get_x21(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Subarray_get_x21___rarg___boxed), 3, 0);
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_get_x21___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Subarray_get_x21___rarg(x_1, x_2, x_3);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_4;
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_getOp___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Subarray_get_x21___rarg(x_1, x_2, x_3);
+return x_4;
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_getOp(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Subarray_getOp___rarg___boxed), 3, 0);
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l_Subarray_getOp___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Subarray_getOp___rarg(x_1, x_2, x_3);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_4;
+}
+}
 LEAN_EXPORT lean_object* l_Subarray_popFront___rarg(lean_object* x_1) {
 _start:
 {

stage0/stdlib/Init/Notation.c

@@ -33,7 +33,6 @@ static lean_object* l_Lean_Parser_Syntax_addPrec___closed__17;
 static lean_object* l_term_x25_x5b___x7c___x5d___closed__2;
 static lean_object* l_Lean_Parser_Tactic_exact___closed__6;
 LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticTrivial;
-static lean_object* l_Lean_Parser_Tactic_rawStx_quot___closed__1;
 static lean_object* l_Lean_Parser_Tactic_intros___closed__7;
 static lean_object* l_termDepIfThenElse___closed__26;
 static lean_object* l_term___x2f_x5c_____closed__1;
@@ -54,7 +53,6 @@ static lean_object* l_stx___x3c_x7c_x3e_____closed__9;
 static lean_object* l___aux__Init__Notation______macroRules__termDepIfThenElse__1___closed__14;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__Complement__complement__1(lean_object*, lean_object*, lean_object*);
 static lean_object* l_term___x3c_x24_x3e_____closed__2;
-static lean_object* l_Lean_Parser_Tactic_rawStx_quot___closed__2;
 static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3e____1___closed__5;
 static lean_object* l_term___x2b_x2b_____closed__4;
 static lean_object* l_term___u2264_____closed__3;
@@ -124,7 +122,6 @@ static lean_object* l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___
 static lean_object* l_precMax___closed__3;
 LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_refine_x27;
 static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x24_x3e____1___closed__7;
-static lean_object* l_Lean_Parser_Tactic_rawStx_quot___closed__8;
 static lean_object* l_Lean_Parser_Tactic_first___closed__9;
 static lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticTrivial__6___closed__6;
 static lean_object* l_boolIfThenElse___closed__13;
@@ -281,7 +278,6 @@ static lean_object* l_Lean_Parser_Tactic_simpPre___closed__4;
 static lean_object* l_stx___x2c_x2b___closed__3;
 static lean_object* l_term___x2a_x3e_____closed__6;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HShiftRight__hShiftRight__1___boxed(lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Parser_Tactic_rawStx_quot___closed__9;
 static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e____1___closed__2;
 static lean_object* l_Lean_Parser_Tactic_rwSeq___closed__8;
 static lean_object* l_Lean_Parser_Tactic_simpStar___closed__2;
@@ -345,6 +341,7 @@ static lean_object* l_term___x7c_x7c_x7c_____closed__2;
 static lean_object* l_Lean_Parser_Tactic_injection___closed__8;
 static lean_object* l_Lean_Parser_Tactic_changeWith___closed__5;
 static lean_object* l___aux__Init__Notation______macroRules__term___x2d____1___closed__9;
+static lean_object* l_Lean_rawStx_quot___closed__10;
 LEAN_EXPORT lean_object* l_prioMid;
 static lean_object* l_Lean_Parser_Tactic_rwSeq___closed__1;
 static lean_object* l___aux__Init__Notation______macroRules__term___x2d____1___closed__4;
@@ -474,6 +471,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x2a_x3e____1
 static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3e_x3e____1___closed__2;
 static lean_object* l_term___u2208_____closed__6;
 static lean_object* l_Lean_Parser_Tactic_renameI___closed__2;
+static lean_object* l_Lean_rawStx_quot___closed__7;
 static lean_object* l_termDepIfThenElse___closed__7;
 static lean_object* l_Lean_Parser_Tactic_cases___closed__3;
 static lean_object* l_Lean_Parser_Tactic_generalizeArg___closed__5;
@@ -483,6 +481,7 @@ static lean_object* l_Lean___aux__Init__Notation______macroRules__term_x5b___x5d
 static lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticShow____1___closed__1;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__prioLow__1(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticShow____1___closed__2;
+LEAN_EXPORT lean_object* l_Lean_rawStx_quot;
 static lean_object* l_Lean_Parser_Tactic_clear___closed__4;
 static lean_object* l_Lean_Parser_Tactic_tacticHave_____x3a_x3d_____closed__5;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__or__1___boxed(lean_object*, lean_object*, lean_object*);
@@ -504,7 +503,6 @@ LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x2f_x5c
 LEAN_EXPORT lean_object* l_term___u2227__;
 static lean_object* l_term___x5e_____closed__5;
 lean_object* lean_string_utf8_byte_size(lean_object*);
-static lean_object* l_Lean_Parser_Tactic_rawStx_quot___closed__6;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HDiv__hDiv__1___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l_precArg___closed__1;
 static lean_object* l_term___x3c_x3d_____closed__4;
@@ -773,6 +771,7 @@ static lean_object* l_Lean_Parser_Tactic_dsimp___closed__4;
 static lean_object* l___aux__Init__Notation______macroRules__stx___x3c_x7c_x3e____1___closed__1;
 static lean_object* l_Lean_Parser_Tactic_unfold___closed__3;
 static lean_object* l_term___u2218_____closed__2;
+static lean_object* l_Lean_rawStx_quot___closed__3;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HXor__hXor__1___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l___aux__Init__Notation______macroRules__term___u2209____1___closed__3;
 static lean_object* l_termDepIfThenElse___closed__32;
@@ -1039,7 +1038,6 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x7c_x3e_
 static lean_object* l_Lean_Parser_Tactic_rotateLeft___closed__6;
 static lean_object* l_term_xac_____closed__3;
 static lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticInfer__instance__1___closed__5;
-static lean_object* l_Lean_Parser_Tactic_rawStx_quot___closed__4;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x3d____2(lean_object*, lean_object*, lean_object*);
 static lean_object* l_term_x7b_____x3a___x2f_x2f___x7d___closed__3;
 static lean_object* l___aux__Init__Notation______macroRules__stx___x2b__1___closed__3;
@@ -1063,6 +1061,7 @@ static lean_object* l_term___x3a_x3a_____closed__1;
 static lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticInfer__instance__1___closed__6;
 static lean_object* l_precLead___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_delta;
+static lean_object* l_Lean_rawStx_quot___closed__6;
 static lean_object* l_Lean_Parser_Tactic_casesTarget___closed__1;
 LEAN_EXPORT lean_object* l_term___x3e_x3d__;
 LEAN_EXPORT lean_object* l_prioDefault;
@@ -1228,7 +1227,6 @@ static lean_object* l_Lean_Parser_Tactic_tacticSuffices_____closed__7;
 static lean_object* l___aux__Init__Notation______macroRules__termIfLet___x3a_x3d__Then__Else____1___closed__2;
 static lean_object* l___aux__Init__Notation______macroRules__term___xd7____1___closed__5;
 static lean_object* l___aux__Init__Notation______macroRules__term___x2a____1___closed__4;
-static lean_object* l_Lean_Parser_Tactic_rawStx_quot___closed__10;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x3a_x3a____1(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__Function__comp__1(lean_object*, lean_object*, lean_object*);
 static lean_object* l___aux__Init__Notation______macroRules__term___x5e_x5e_x5e____1___closed__6;
@@ -1389,6 +1387,7 @@ static lean_object* l_term___u2208_____closed__2;
 static lean_object* l_Lean_Parser_Tactic_tacticNext_______x3d_x3e_____closed__6;
 static lean_object* l___aux__Init__Notation______macroRules__termDepIfThenElse__1___closed__1;
 static lean_object* l_term___x5c_x2f_____closed__1;
+static lean_object* l_Lean_rawStx_quot___closed__9;
 static lean_object* l_Lean_Parser_Tactic_tacticRfl_x27___closed__4;
 LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticLet__;
 static lean_object* l_term_x25_x5b___x7c___x5d___closed__9;
@@ -1453,9 +1452,11 @@ static lean_object* l_term___x3e_____closed__1;
 static lean_object* l_term_x25_x5b___x7c___x5d___closed__8;
 static lean_object* l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__7;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__And__1(lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_rawStx_quot___closed__1;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HAnd__hAnd__1___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l_term___x5e_____closed__2;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HMul__hMul__1___boxed(lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_rawStx_quot___closed__2;
 static lean_object* l_Lean_Parser_Tactic_simp___closed__3;
 static lean_object* l___aux__Init__Notation______macroRules__term___x3c____1___closed__4;
 LEAN_EXPORT lean_object* l_prioHigh;
@@ -1518,6 +1519,7 @@ static lean_object* l_term___x2b_x2b_____closed__1;
 static lean_object* l_stx___x3c_x7c_x3e_____closed__7;
 static lean_object* l_Lean_Parser_Tactic_changeWith___closed__6;
 static lean_object* l_Lean_Parser_Tactic_simpPre___closed__2;
+static lean_object* l_Lean_rawStx_quot___closed__8;
 static lean_object* l_Lean_Parser_Tactic_fail___closed__3;
 static lean_object* l_Lean_Parser_Tactic_ac__refl___closed__1;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3d____2(lean_object*, lean_object*, lean_object*);
@@ -1570,6 +1572,7 @@ static lean_object* l___aux__Init__Notation______macroRules__stx___x3c_x7c_x3e__
 static lean_object* l_Lean___aux__Init__Notation______macroRules__term_x5b___x5d__1___closed__4;
 static lean_object* l_Lean_Parser_Tactic_simp___closed__15;
 static lean_object* l_Lean_Parser_Tactic_tacticExists___x2c_x2c___closed__2;
+static lean_object* l_Lean_rawStx_quot___closed__4;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HShiftRight__hShiftRight__1(lean_object*, lean_object*, lean_object*);
 static lean_object* l_term___x3d_____closed__2;
 static lean_object* l_Lean_Parser_Tactic_refine___closed__4;
@@ -1658,12 +1661,12 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x3d_x3d____1
 static lean_object* l___aux__Init__Notation______macroRules__stx_x21____1___closed__3;
 static lean_object* l_Lean_Parser_Tactic_tacticRepeat_____closed__6;
 LEAN_EXPORT lean_object* l_term_x7b_____x3a___x2f_x2f___x7d;
+static lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__2;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x7c_x3e____1(lean_object*, lean_object*, lean_object*);
 static lean_object* l___aux__Init__Notation______macroRules__term___x3c____1___closed__7;
 static lean_object* l_Lean_Parser_Tactic_case___closed__8;
 static lean_object* l_term___x7c_x7c_____closed__6;
 static lean_object* l_termWithout__expected__type_____closed__1;
-LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_rawStx_quot;
 LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_change;
 static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e____1___closed__4;
 static lean_object* l_Lean_Parser_Tactic_simp___closed__5;
@@ -1712,6 +1715,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x7c_x7c_x7c_
 LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__and__1(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_withReducibleAndInstances;
 static lean_object* l_Lean_Parser_Tactic_unfold___closed__6;
+static lean_object* l_Lean_rawStx_quot___closed__5;
 static lean_object* l_termIfLet___x3a_x3d__Then__Else_____closed__6;
 static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x2a_x3e____1___closed__6;
 static lean_object* l_Lean_Parser_Tactic_ac__refl___closed__5;
@@ -1932,7 +1936,6 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x7c_x3e_
 static lean_object* l_Lean_Parser_Tactic_focus___closed__3;
 LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticRepeat____1(lean_object*, lean_object*, lean_object*);
 static lean_object* l_term___x26_x26_x26_____closed__5;
-static lean_object* l_Lean_Parser_Tactic_rawStx_quot___closed__3;
 static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x3d____1___closed__7;
 static lean_object* l_Lean_Parser_Tactic_rwSeq___closed__2;
 static lean_object* l_Lean_Parser_Tactic_changeWith___closed__3;
@@ -2234,7 +2237,6 @@ static lean_object* l_term___x2a_x3e_____closed__2;
 static lean_object* l_Lean_Parser_Tactic_letrec___closed__10;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__prio_x28___x29__1___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Parser_Tactic_split___closed__8;
-static lean_object* l_Lean_Parser_Tactic_rawStx_quot___closed__7;
 static lean_object* l_Lean_Parser_Tactic_tacticAdmit___closed__4;
 static lean_object* l___aux__Init__Notation______macroRules__term___x2b_x2b____1___closed__7;
 static lean_object* l_Lean_termThis___closed__2;
@@ -2275,7 +2277,6 @@ static lean_object* l_Lean_Parser_Tactic_rwSeq___closed__5;
 static lean_object* l_Lean_Parser_Tactic_anyGoals___closed__4;
 static lean_object* l_Lean_Parser_Tactic_unfold___closed__7;
 static lean_object* l_Lean_Parser_Tactic_tacticRfl_x27___closed__5;
-static lean_object* l_Lean_Parser_Tactic_rawStx_quot___closed__5;
 static lean_object* l_Lean_Parser_Tactic_tacticRepeat_____closed__4;
 static lean_object* l_Lean_Parser_Tactic_traceMessage___closed__7;
 LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___u2265____2(lean_object*, lean_object*, lean_object*);
@@ -30755,7 +30756,7 @@ lean_dec(x_2);
 return x_4;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_rawStx_quot___closed__1() {
+static lean_object* _init_l_Lean_rawStx_quot___closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -30763,17 +30764,17 @@ x_1 = lean_mk_string("quot");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_rawStx_quot___closed__2() {
+static lean_object* _init_l_Lean_rawStx_quot___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l___aux__Init__Notation______macroRules__term___u2218____1___closed__2;
-x_2 = l_Lean_Parser_Tactic_rawStx_quot___closed__1;
+x_2 = l_Lean_rawStx_quot___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_rawStx_quot___closed__3() {
+static lean_object* _init_l_Lean_rawStx_quot___closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -30781,17 +30782,17 @@ x_1 = lean_mk_string("`(rawStx|");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_rawStx_quot___closed__4() {
+static lean_object* _init_l_Lean_rawStx_quot___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Parser_Tactic_rawStx_quot___closed__3;
+x_1 = l_Lean_rawStx_quot___closed__3;
 x_2 = lean_alloc_ctor(5, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_rawStx_quot___closed__5() {
+static lean_object* _init_l_Lean_rawStx_quot___closed__5() {
 _start:
 {
 lean_object* x_1; 
@@ -30799,21 +30800,21 @@ x_1 = lean_mk_string("rawStx");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_rawStx_quot___closed__6() {
+static lean_object* _init_l_Lean_rawStx_quot___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Parser_Tactic_rawStx_quot___closed__5;
+x_2 = l_Lean_rawStx_quot___closed__5;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_rawStx_quot___closed__7() {
+static lean_object* _init_l_Lean_rawStx_quot___closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_rawStx_quot___closed__6;
+x_1 = l_Lean_rawStx_quot___closed__6;
 x_2 = lean_unsigned_to_nat(0u);
 x_3 = lean_alloc_ctor(7, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
@@ -30821,12 +30822,12 @@ lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_rawStx_quot___closed__8() {
+static lean_object* _init_l_Lean_rawStx_quot___closed__8() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
-x_2 = l_Lean_Parser_Tactic_rawStx_quot___closed__7;
+x_2 = l_Lean_rawStx_quot___closed__7;
 x_3 = l_prec_x28___x29___closed__8;
 x_4 = lean_alloc_ctor(2, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
@@ -30835,13 +30836,13 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_rawStx_quot___closed__9() {
+static lean_object* _init_l_Lean_rawStx_quot___closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
-x_2 = l_Lean_Parser_Tactic_rawStx_quot___closed__4;
-x_3 = l_Lean_Parser_Tactic_rawStx_quot___closed__8;
+x_2 = l_Lean_rawStx_quot___closed__4;
+x_3 = l_Lean_rawStx_quot___closed__8;
 x_4 = lean_alloc_ctor(2, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -30849,13 +30850,13 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_rawStx_quot___closed__10() {
+static lean_object* _init_l_Lean_rawStx_quot___closed__10() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Parser_Tactic_rawStx_quot___closed__2;
+x_1 = l_Lean_rawStx_quot___closed__2;
 x_2 = lean_unsigned_to_nat(1024u);
-x_3 = l_Lean_Parser_Tactic_rawStx_quot___closed__9;
+x_3 = l_Lean_rawStx_quot___closed__9;
 x_4 = lean_alloc_ctor(3, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -30863,11 +30864,11 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_Lean_Parser_Tactic_rawStx_quot() {
+static lean_object* _init_l_Lean_rawStx_quot() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Tactic_rawStx_quot___closed__10;
+x_1 = l_Lean_rawStx_quot___closed__10;
 return x_1;
 }
 }
@@ -30933,7 +30934,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
 x_2 = l_Lean_Parser_Tactic_withAnnotateState___closed__6;
-x_3 = l_Lean_Parser_Tactic_rawStx_quot___closed__7;
+x_3 = l_Lean_rawStx_quot___closed__7;
 x_4 = lean_alloc_ctor(2, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -34253,6 +34254,14 @@ static lean_object* _init_l_Lean_Parser_Tactic___aux__Init__Notation______macroR
 _start:
 {
 lean_object* x_1; 
+x_1 = lean_mk_string("with_annotate_state");
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__2() {
+_start:
+{
+lean_object* x_1; 
 x_1 = lean_mk_string("all_goals");
 return x_1;
 }
@@ -34277,293 +34286,259 @@ return x_7;
 }
 else
 {
-lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; 
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15; 
 x_8 = lean_unsigned_to_nat(0u);
 x_9 = l_Lean_Syntax_getArg(x_1, x_8);
-x_10 = lean_unsigned_to_nat(2u);
+x_10 = lean_unsigned_to_nat(1u);
 x_11 = l_Lean_Syntax_getArg(x_1, x_10);
+x_12 = lean_unsigned_to_nat(2u);
+x_13 = l_Lean_Syntax_getArg(x_1, x_12);
 lean_dec(x_1);
-x_12 = l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRules__precMax__1___spec__1(x_2, x_3);
-x_13 = !lean_is_exclusive(x_12);
-if (x_13 == 0)
+x_14 = l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRules__precMax__1___spec__1(x_2, x_3);
+x_15 = !lean_is_exclusive(x_14);
+if (x_15 == 0)
 {
-lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_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_object* x_30; lean_object* x_31; lean_object* x_32; 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; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; 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_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; 
-x_14 = lean_ctor_get(x_12, 0);
-x_15 = l_Lean_Parser_Tactic_focus___closed__1;
-lean_inc(x_14);
-x_16 = lean_alloc_ctor(2, 2, 0);
-lean_ctor_set(x_16, 0, x_14);
-lean_ctor_set(x_16, 1, x_15);
-x_17 = l_prec_x28___x29___closed__3;
-lean_inc(x_14);
+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_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_object* x_30; lean_object* x_31; lean_object* x_32; 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; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; 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_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; 
+x_16 = lean_ctor_get(x_14, 0);
+x_17 = l_Lean_Parser_Tactic_focus___closed__1;
+lean_inc(x_16);
 x_18 = lean_alloc_ctor(2, 2, 0);
-lean_ctor_set(x_18, 0, x_14);
+lean_ctor_set(x_18, 0, x_16);
 lean_ctor_set(x_18, 1, x_17);
-x_19 = l___aux__Init__Notation______macroRules__termDepIfThenElse__1___closed__9;
-lean_inc(x_14);
-x_20 = lean_alloc_ctor(2, 2, 0);
-lean_ctor_set(x_20, 0, x_14);
-lean_ctor_set(x_20, 1, x_19);
-x_21 = l___aux__Init__Notation______macroRules__precMax__1___closed__4;
-x_22 = lean_array_push(x_21, x_20);
+x_19 = l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__10;
+x_20 = lean_array_push(x_19, x_9);
+x_21 = l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__12;
+x_22 = lean_array_push(x_20, x_21);
 x_23 = lean_box(2);
-x_24 = l___aux__Init__Notation______macroRules__stx___x2b__1___closed__8;
+x_24 = l_Lean_Parser_Tactic_first___closed__8;
 x_25 = lean_alloc_ctor(1, 3, 0);
 lean_ctor_set(x_25, 0, x_23);
 lean_ctor_set(x_25, 1, x_24);
 lean_ctor_set(x_25, 2, x_22);
-x_26 = l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__10;
-x_27 = lean_array_push(x_26, x_9);
-x_28 = lean_array_push(x_27, x_25);
-x_29 = l_Lean_Parser_Tactic_first___closed__8;
-x_30 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_30, 0, x_23);
-lean_ctor_set(x_30, 1, x_29);
-lean_ctor_set(x_30, 2, x_28);
-x_31 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__1;
-lean_inc(x_14);
-x_32 = lean_alloc_ctor(2, 2, 0);
-lean_ctor_set(x_32, 0, x_14);
-lean_ctor_set(x_32, 1, x_31);
-x_33 = lean_array_push(x_26, x_11);
-x_34 = l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__12;
-x_35 = lean_array_push(x_33, x_34);
-x_36 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_36, 0, x_23);
-lean_ctor_set(x_36, 1, x_29);
-lean_ctor_set(x_36, 2, x_35);
-x_37 = lean_array_push(x_21, x_36);
-x_38 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_38, 0, x_23);
-lean_ctor_set(x_38, 1, x_24);
-lean_ctor_set(x_38, 2, x_37);
-x_39 = lean_array_push(x_21, x_38);
-x_40 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticTry____1___closed__4;
-x_41 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_41, 0, x_23);
-lean_ctor_set(x_41, 1, x_40);
-lean_ctor_set(x_41, 2, x_39);
-x_42 = lean_array_push(x_21, x_41);
-x_43 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticNext_______x3d_x3e____1___closed__1;
-x_44 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_44, 0, x_23);
+x_26 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__1;
+lean_inc(x_16);
+x_27 = lean_alloc_ctor(2, 2, 0);
+lean_ctor_set(x_27, 0, x_16);
+lean_ctor_set(x_27, 1, x_26);
+x_28 = l_Lean_Parser_Tactic_skip___closed__1;
+lean_inc(x_16);
+x_29 = lean_alloc_ctor(2, 2, 0);
+lean_ctor_set(x_29, 0, x_16);
+lean_ctor_set(x_29, 1, x_28);
+x_30 = l___aux__Init__Notation______macroRules__precMax__1___closed__4;
+x_31 = lean_array_push(x_30, x_29);
+x_32 = l_Lean_Parser_Tactic_skip___closed__2;
+x_33 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_33, 0, x_23);
+lean_ctor_set(x_33, 1, x_32);
+lean_ctor_set(x_33, 2, x_31);
+x_34 = l___aux__Init__Notation______unexpand__Function__comp__1___closed__3;
+x_35 = lean_array_push(x_34, x_27);
+x_36 = lean_array_push(x_35, x_11);
+x_37 = lean_array_push(x_36, x_33);
+x_38 = l_Lean_Parser_Tactic_withAnnotateState___closed__4;
+x_39 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_39, 0, x_23);
+lean_ctor_set(x_39, 1, x_38);
+lean_ctor_set(x_39, 2, x_37);
+x_40 = lean_array_push(x_19, x_39);
+x_41 = lean_array_push(x_40, x_21);
+x_42 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_42, 0, x_23);
+lean_ctor_set(x_42, 1, x_24);
+lean_ctor_set(x_42, 2, x_41);
+x_43 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__2;
+x_44 = lean_alloc_ctor(2, 2, 0);
+lean_ctor_set(x_44, 0, x_16);
 lean_ctor_set(x_44, 1, x_43);
-lean_ctor_set(x_44, 2, x_42);
-x_45 = lean_array_push(x_26, x_32);
-x_46 = lean_array_push(x_45, x_44);
-x_47 = l_Lean_Parser_Tactic_allGoals___closed__2;
-x_48 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_48, 0, x_23);
-lean_ctor_set(x_48, 1, x_47);
-lean_ctor_set(x_48, 2, x_46);
-x_49 = lean_array_push(x_26, x_48);
-x_50 = lean_array_push(x_49, x_34);
-x_51 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_51, 0, x_23);
-lean_ctor_set(x_51, 1, x_29);
-lean_ctor_set(x_51, 2, x_50);
-x_52 = lean_array_push(x_26, x_30);
-x_53 = lean_array_push(x_52, x_51);
-x_54 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_54, 0, x_23);
-lean_ctor_set(x_54, 1, x_24);
-lean_ctor_set(x_54, 2, x_53);
-x_55 = lean_array_push(x_21, x_54);
+x_45 = lean_array_push(x_19, x_13);
+x_46 = lean_array_push(x_45, x_21);
+x_47 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_47, 0, x_23);
+lean_ctor_set(x_47, 1, x_24);
+lean_ctor_set(x_47, 2, x_46);
+x_48 = lean_array_push(x_30, x_47);
+x_49 = l___aux__Init__Notation______macroRules__stx___x2b__1___closed__8;
+x_50 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_50, 0, x_23);
+lean_ctor_set(x_50, 1, x_49);
+lean_ctor_set(x_50, 2, x_48);
+x_51 = lean_array_push(x_30, x_50);
+x_52 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticTry____1___closed__4;
+x_53 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_53, 0, x_23);
+lean_ctor_set(x_53, 1, x_52);
+lean_ctor_set(x_53, 2, x_51);
+x_54 = lean_array_push(x_30, x_53);
+x_55 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticNext_______x3d_x3e____1___closed__1;
 x_56 = lean_alloc_ctor(1, 3, 0);
 lean_ctor_set(x_56, 0, x_23);
-lean_ctor_set(x_56, 1, x_40);
-lean_ctor_set(x_56, 2, x_55);
-x_57 = lean_array_push(x_21, x_56);
-x_58 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_58, 0, x_23);
-lean_ctor_set(x_58, 1, x_43);
-lean_ctor_set(x_58, 2, x_57);
-x_59 = l_prec_x28___x29___closed__7;
-x_60 = lean_alloc_ctor(2, 2, 0);
-lean_ctor_set(x_60, 0, x_14);
+lean_ctor_set(x_56, 1, x_55);
+lean_ctor_set(x_56, 2, x_54);
+x_57 = lean_array_push(x_19, x_44);
+x_58 = lean_array_push(x_57, x_56);
+x_59 = l_Lean_Parser_Tactic_allGoals___closed__2;
+x_60 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_60, 0, x_23);
 lean_ctor_set(x_60, 1, x_59);
-x_61 = l___aux__Init__Notation______unexpand__Function__comp__1___closed__3;
-x_62 = lean_array_push(x_61, x_18);
-x_63 = lean_array_push(x_62, x_58);
-x_64 = lean_array_push(x_63, x_60);
-x_65 = l_Lean_Parser_Tactic_paren___closed__1;
-x_66 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_66, 0, x_23);
-lean_ctor_set(x_66, 1, x_65);
-lean_ctor_set(x_66, 2, x_64);
-x_67 = lean_array_push(x_26, x_66);
-x_68 = lean_array_push(x_67, x_34);
+lean_ctor_set(x_60, 2, x_58);
+x_61 = lean_array_push(x_19, x_60);
+x_62 = lean_array_push(x_61, x_21);
+x_63 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_63, 0, x_23);
+lean_ctor_set(x_63, 1, x_24);
+lean_ctor_set(x_63, 2, x_62);
+x_64 = lean_array_push(x_34, x_25);
+x_65 = lean_array_push(x_64, x_42);
+x_66 = lean_array_push(x_65, x_63);
+x_67 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_67, 0, x_23);
+lean_ctor_set(x_67, 1, x_49);
+lean_ctor_set(x_67, 2, x_66);
+x_68 = lean_array_push(x_30, x_67);
 x_69 = lean_alloc_ctor(1, 3, 0);
 lean_ctor_set(x_69, 0, x_23);
-lean_ctor_set(x_69, 1, x_29);
+lean_ctor_set(x_69, 1, x_52);
 lean_ctor_set(x_69, 2, x_68);
-x_70 = lean_array_push(x_21, x_69);
+x_70 = lean_array_push(x_30, x_69);
 x_71 = lean_alloc_ctor(1, 3, 0);
 lean_ctor_set(x_71, 0, x_23);
-lean_ctor_set(x_71, 1, x_24);
+lean_ctor_set(x_71, 1, x_55);
 lean_ctor_set(x_71, 2, x_70);
-x_72 = lean_array_push(x_21, x_71);
-x_73 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_73, 0, x_23);
-lean_ctor_set(x_73, 1, x_40);
-lean_ctor_set(x_73, 2, x_72);
-x_74 = lean_array_push(x_21, x_73);
+x_72 = lean_array_push(x_19, x_18);
+x_73 = lean_array_push(x_72, x_71);
+x_74 = l_Lean_Parser_Tactic_focus___closed__2;
 x_75 = lean_alloc_ctor(1, 3, 0);
 lean_ctor_set(x_75, 0, x_23);
-lean_ctor_set(x_75, 1, x_43);
-lean_ctor_set(x_75, 2, x_74);
-x_76 = lean_array_push(x_26, x_16);
-x_77 = lean_array_push(x_76, x_75);
-x_78 = l_Lean_Parser_Tactic_focus___closed__2;
-x_79 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_79, 0, x_23);
-lean_ctor_set(x_79, 1, x_78);
-lean_ctor_set(x_79, 2, x_77);
-lean_ctor_set(x_12, 0, x_79);
-return x_12;
+lean_ctor_set(x_75, 1, x_74);
+lean_ctor_set(x_75, 2, x_73);
+lean_ctor_set(x_14, 0, x_75);
+return x_14;
 }
 else
 {
-lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; 
-x_80 = lean_ctor_get(x_12, 0);
-x_81 = lean_ctor_get(x_12, 1);
-lean_inc(x_81);
-lean_inc(x_80);
-lean_dec(x_12);
-x_82 = l_Lean_Parser_Tactic_focus___closed__1;
-lean_inc(x_80);
-x_83 = lean_alloc_ctor(2, 2, 0);
-lean_ctor_set(x_83, 0, x_80);
-lean_ctor_set(x_83, 1, x_82);
-x_84 = l_prec_x28___x29___closed__3;
-lean_inc(x_80);
-x_85 = lean_alloc_ctor(2, 2, 0);
-lean_ctor_set(x_85, 0, x_80);
-lean_ctor_set(x_85, 1, x_84);
-x_86 = l___aux__Init__Notation______macroRules__termDepIfThenElse__1___closed__9;
-lean_inc(x_80);
-x_87 = lean_alloc_ctor(2, 2, 0);
-lean_ctor_set(x_87, 0, x_80);
-lean_ctor_set(x_87, 1, x_86);
-x_88 = l___aux__Init__Notation______macroRules__precMax__1___closed__4;
-x_89 = lean_array_push(x_88, x_87);
-x_90 = lean_box(2);
-x_91 = l___aux__Init__Notation______macroRules__stx___x2b__1___closed__8;
-x_92 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_92, 0, x_90);
-lean_ctor_set(x_92, 1, x_91);
-lean_ctor_set(x_92, 2, x_89);
-x_93 = l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__10;
-x_94 = lean_array_push(x_93, x_9);
-x_95 = lean_array_push(x_94, x_92);
-x_96 = l_Lean_Parser_Tactic_first___closed__8;
-x_97 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_97, 0, x_90);
-lean_ctor_set(x_97, 1, x_96);
-lean_ctor_set(x_97, 2, x_95);
-x_98 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__1;
-lean_inc(x_80);
-x_99 = lean_alloc_ctor(2, 2, 0);
-lean_ctor_set(x_99, 0, x_80);
-lean_ctor_set(x_99, 1, x_98);
-x_100 = lean_array_push(x_93, x_11);
-x_101 = l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__12;
-x_102 = lean_array_push(x_100, x_101);
+lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; 
+x_76 = lean_ctor_get(x_14, 0);
+x_77 = lean_ctor_get(x_14, 1);
+lean_inc(x_77);
+lean_inc(x_76);
+lean_dec(x_14);
+x_78 = l_Lean_Parser_Tactic_focus___closed__1;
+lean_inc(x_76);
+x_79 = lean_alloc_ctor(2, 2, 0);
+lean_ctor_set(x_79, 0, x_76);
+lean_ctor_set(x_79, 1, x_78);
+x_80 = l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__10;
+x_81 = lean_array_push(x_80, x_9);
+x_82 = l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__12;
+x_83 = lean_array_push(x_81, x_82);
+x_84 = lean_box(2);
+x_85 = l_Lean_Parser_Tactic_first___closed__8;
+x_86 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_86, 0, x_84);
+lean_ctor_set(x_86, 1, x_85);
+lean_ctor_set(x_86, 2, x_83);
+x_87 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__1;
+lean_inc(x_76);
+x_88 = lean_alloc_ctor(2, 2, 0);
+lean_ctor_set(x_88, 0, x_76);
+lean_ctor_set(x_88, 1, x_87);
+x_89 = l_Lean_Parser_Tactic_skip___closed__1;
+lean_inc(x_76);
+x_90 = lean_alloc_ctor(2, 2, 0);
+lean_ctor_set(x_90, 0, x_76);
+lean_ctor_set(x_90, 1, x_89);
+x_91 = l___aux__Init__Notation______macroRules__precMax__1___closed__4;
+x_92 = lean_array_push(x_91, x_90);
+x_93 = l_Lean_Parser_Tactic_skip___closed__2;
+x_94 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_94, 0, x_84);
+lean_ctor_set(x_94, 1, x_93);
+lean_ctor_set(x_94, 2, x_92);
+x_95 = l___aux__Init__Notation______unexpand__Function__comp__1___closed__3;
+x_96 = lean_array_push(x_95, x_88);
+x_97 = lean_array_push(x_96, x_11);
+x_98 = lean_array_push(x_97, x_94);
+x_99 = l_Lean_Parser_Tactic_withAnnotateState___closed__4;
+x_100 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_100, 0, x_84);
+lean_ctor_set(x_100, 1, x_99);
+lean_ctor_set(x_100, 2, x_98);
+x_101 = lean_array_push(x_80, x_100);
+x_102 = lean_array_push(x_101, x_82);
 x_103 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_103, 0, x_90);
-lean_ctor_set(x_103, 1, x_96);
+lean_ctor_set(x_103, 0, x_84);
+lean_ctor_set(x_103, 1, x_85);
 lean_ctor_set(x_103, 2, x_102);
-x_104 = lean_array_push(x_88, x_103);
-x_105 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_105, 0, x_90);
-lean_ctor_set(x_105, 1, x_91);
-lean_ctor_set(x_105, 2, x_104);
-x_106 = lean_array_push(x_88, x_105);
-x_107 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticTry____1___closed__4;
+x_104 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__2;
+x_105 = lean_alloc_ctor(2, 2, 0);
+lean_ctor_set(x_105, 0, x_76);
+lean_ctor_set(x_105, 1, x_104);
+x_106 = lean_array_push(x_80, x_13);
+x_107 = lean_array_push(x_106, x_82);
 x_108 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_108, 0, x_90);
-lean_ctor_set(x_108, 1, x_107);
-lean_ctor_set(x_108, 2, x_106);
-x_109 = lean_array_push(x_88, x_108);
-x_110 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticNext_______x3d_x3e____1___closed__1;
+lean_ctor_set(x_108, 0, x_84);
+lean_ctor_set(x_108, 1, x_85);
+lean_ctor_set(x_108, 2, x_107);
+x_109 = lean_array_push(x_91, x_108);
+x_110 = l___aux__Init__Notation______macroRules__stx___x2b__1___closed__8;
 x_111 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_111, 0, x_90);
+lean_ctor_set(x_111, 0, x_84);
 lean_ctor_set(x_111, 1, x_110);
 lean_ctor_set(x_111, 2, x_109);
-x_112 = lean_array_push(x_93, x_99);
-x_113 = lean_array_push(x_112, x_111);
-x_114 = l_Lean_Parser_Tactic_allGoals___closed__2;
-x_115 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_115, 0, x_90);
-lean_ctor_set(x_115, 1, x_114);
-lean_ctor_set(x_115, 2, x_113);
-x_116 = lean_array_push(x_93, x_115);
-x_117 = lean_array_push(x_116, x_101);
-x_118 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_118, 0, x_90);
-lean_ctor_set(x_118, 1, x_96);
-lean_ctor_set(x_118, 2, x_117);
-x_119 = lean_array_push(x_93, x_97);
-x_120 = lean_array_push(x_119, x_118);
+x_112 = lean_array_push(x_91, x_111);
+x_113 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticTry____1___closed__4;
+x_114 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_114, 0, x_84);
+lean_ctor_set(x_114, 1, x_113);
+lean_ctor_set(x_114, 2, x_112);
+x_115 = lean_array_push(x_91, x_114);
+x_116 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticNext_______x3d_x3e____1___closed__1;
+x_117 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_117, 0, x_84);
+lean_ctor_set(x_117, 1, x_116);
+lean_ctor_set(x_117, 2, x_115);
+x_118 = lean_array_push(x_80, x_105);
+x_119 = lean_array_push(x_118, x_117);
+x_120 = l_Lean_Parser_Tactic_allGoals___closed__2;
 x_121 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_121, 0, x_90);
-lean_ctor_set(x_121, 1, x_91);
-lean_ctor_set(x_121, 2, x_120);
-x_122 = lean_array_push(x_88, x_121);
-x_123 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_123, 0, x_90);
-lean_ctor_set(x_123, 1, x_107);
-lean_ctor_set(x_123, 2, x_122);
-x_124 = lean_array_push(x_88, x_123);
-x_125 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_125, 0, x_90);
-lean_ctor_set(x_125, 1, x_110);
-lean_ctor_set(x_125, 2, x_124);
-x_126 = l_prec_x28___x29___closed__7;
-x_127 = lean_alloc_ctor(2, 2, 0);
-lean_ctor_set(x_127, 0, x_80);
-lean_ctor_set(x_127, 1, x_126);
-x_128 = l___aux__Init__Notation______unexpand__Function__comp__1___closed__3;
-x_129 = lean_array_push(x_128, x_85);
-x_130 = lean_array_push(x_129, x_125);
-x_131 = lean_array_push(x_130, x_127);
-x_132 = l_Lean_Parser_Tactic_paren___closed__1;
-x_133 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_133, 0, x_90);
-lean_ctor_set(x_133, 1, x_132);
-lean_ctor_set(x_133, 2, x_131);
-x_134 = lean_array_push(x_93, x_133);
-x_135 = lean_array_push(x_134, x_101);
+lean_ctor_set(x_121, 0, x_84);
+lean_ctor_set(x_121, 1, x_120);
+lean_ctor_set(x_121, 2, x_119);
+x_122 = lean_array_push(x_80, x_121);
+x_123 = lean_array_push(x_122, x_82);
+x_124 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_124, 0, x_84);
+lean_ctor_set(x_124, 1, x_85);
+lean_ctor_set(x_124, 2, x_123);
+x_125 = lean_array_push(x_95, x_86);
+x_126 = lean_array_push(x_125, x_103);
+x_127 = lean_array_push(x_126, x_124);
+x_128 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_128, 0, x_84);
+lean_ctor_set(x_128, 1, x_110);
+lean_ctor_set(x_128, 2, x_127);
+x_129 = lean_array_push(x_91, x_128);
+x_130 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_130, 0, x_84);
+lean_ctor_set(x_130, 1, x_113);
+lean_ctor_set(x_130, 2, x_129);
+x_131 = lean_array_push(x_91, x_130);
+x_132 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_132, 0, x_84);
+lean_ctor_set(x_132, 1, x_116);
+lean_ctor_set(x_132, 2, x_131);
+x_133 = lean_array_push(x_80, x_79);
+x_134 = lean_array_push(x_133, x_132);
+x_135 = l_Lean_Parser_Tactic_focus___closed__2;
 x_136 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_136, 0, x_90);
-lean_ctor_set(x_136, 1, x_96);
-lean_ctor_set(x_136, 2, x_135);
-x_137 = lean_array_push(x_88, x_136);
-x_138 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_138, 0, x_90);
-lean_ctor_set(x_138, 1, x_91);
-lean_ctor_set(x_138, 2, x_137);
-x_139 = lean_array_push(x_88, x_138);
-x_140 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_140, 0, x_90);
-lean_ctor_set(x_140, 1, x_107);
-lean_ctor_set(x_140, 2, x_139);
-x_141 = lean_array_push(x_88, x_140);
-x_142 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_142, 0, x_90);
-lean_ctor_set(x_142, 1, x_110);
-lean_ctor_set(x_142, 2, x_141);
-x_143 = lean_array_push(x_93, x_83);
-x_144 = lean_array_push(x_143, x_142);
-x_145 = l_Lean_Parser_Tactic_focus___closed__2;
-x_146 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_146, 0, x_90);
-lean_ctor_set(x_146, 1, x_145);
-lean_ctor_set(x_146, 2, x_144);
-x_147 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_147, 0, x_146);
-lean_ctor_set(x_147, 1, x_81);
-return x_147;
+lean_ctor_set(x_136, 0, x_84);
+lean_ctor_set(x_136, 1, x_135);
+lean_ctor_set(x_136, 2, x_134);
+x_137 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_137, 0, x_136);
+lean_ctor_set(x_137, 1, x_77);
+return x_137;
 }
 }
 }
@@ -48979,28 +48954,28 @@ l_Lean___aux__Init__Notation______macroRules__Lean__termThis__1___closed__2 = _i
 lean_mark_persistent(l_Lean___aux__Init__Notation______macroRules__Lean__termThis__1___closed__2);
 l_Lean___aux__Init__Notation______macroRules__Lean__termThis__1___closed__3 = _init_l_Lean___aux__Init__Notation______macroRules__Lean__termThis__1___closed__3();
 lean_mark_persistent(l_Lean___aux__Init__Notation______macroRules__Lean__termThis__1___closed__3);
-l_Lean_Parser_Tactic_rawStx_quot___closed__1 = _init_l_Lean_Parser_Tactic_rawStx_quot___closed__1();
-lean_mark_persistent(l_Lean_Parser_Tactic_rawStx_quot___closed__1);
-l_Lean_Parser_Tactic_rawStx_quot___closed__2 = _init_l_Lean_Parser_Tactic_rawStx_quot___closed__2();
-lean_mark_persistent(l_Lean_Parser_Tactic_rawStx_quot___closed__2);
-l_Lean_Parser_Tactic_rawStx_quot___closed__3 = _init_l_Lean_Parser_Tactic_rawStx_quot___closed__3();
-lean_mark_persistent(l_Lean_Parser_Tactic_rawStx_quot___closed__3);
-l_Lean_Parser_Tactic_rawStx_quot___closed__4 = _init_l_Lean_Parser_Tactic_rawStx_quot___closed__4();
-lean_mark_persistent(l_Lean_Parser_Tactic_rawStx_quot___closed__4);
-l_Lean_Parser_Tactic_rawStx_quot___closed__5 = _init_l_Lean_Parser_Tactic_rawStx_quot___closed__5();
-lean_mark_persistent(l_Lean_Parser_Tactic_rawStx_quot___closed__5);
-l_Lean_Parser_Tactic_rawStx_quot___closed__6 = _init_l_Lean_Parser_Tactic_rawStx_quot___closed__6();
-lean_mark_persistent(l_Lean_Parser_Tactic_rawStx_quot___closed__6);
-l_Lean_Parser_Tactic_rawStx_quot___closed__7 = _init_l_Lean_Parser_Tactic_rawStx_quot___closed__7();
-lean_mark_persistent(l_Lean_Parser_Tactic_rawStx_quot___closed__7);
-l_Lean_Parser_Tactic_rawStx_quot___closed__8 = _init_l_Lean_Parser_Tactic_rawStx_quot___closed__8();
-lean_mark_persistent(l_Lean_Parser_Tactic_rawStx_quot___closed__8);
-l_Lean_Parser_Tactic_rawStx_quot___closed__9 = _init_l_Lean_Parser_Tactic_rawStx_quot___closed__9();
-lean_mark_persistent(l_Lean_Parser_Tactic_rawStx_quot___closed__9);
-l_Lean_Parser_Tactic_rawStx_quot___closed__10 = _init_l_Lean_Parser_Tactic_rawStx_quot___closed__10();
-lean_mark_persistent(l_Lean_Parser_Tactic_rawStx_quot___closed__10);
-l_Lean_Parser_Tactic_rawStx_quot = _init_l_Lean_Parser_Tactic_rawStx_quot();
-lean_mark_persistent(l_Lean_Parser_Tactic_rawStx_quot);
+l_Lean_rawStx_quot___closed__1 = _init_l_Lean_rawStx_quot___closed__1();
+lean_mark_persistent(l_Lean_rawStx_quot___closed__1);
+l_Lean_rawStx_quot___closed__2 = _init_l_Lean_rawStx_quot___closed__2();
+lean_mark_persistent(l_Lean_rawStx_quot___closed__2);
+l_Lean_rawStx_quot___closed__3 = _init_l_Lean_rawStx_quot___closed__3();
+lean_mark_persistent(l_Lean_rawStx_quot___closed__3);
+l_Lean_rawStx_quot___closed__4 = _init_l_Lean_rawStx_quot___closed__4();
+lean_mark_persistent(l_Lean_rawStx_quot___closed__4);
+l_Lean_rawStx_quot___closed__5 = _init_l_Lean_rawStx_quot___closed__5();
+lean_mark_persistent(l_Lean_rawStx_quot___closed__5);
+l_Lean_rawStx_quot___closed__6 = _init_l_Lean_rawStx_quot___closed__6();
+lean_mark_persistent(l_Lean_rawStx_quot___closed__6);
+l_Lean_rawStx_quot___closed__7 = _init_l_Lean_rawStx_quot___closed__7();
+lean_mark_persistent(l_Lean_rawStx_quot___closed__7);
+l_Lean_rawStx_quot___closed__8 = _init_l_Lean_rawStx_quot___closed__8();
+lean_mark_persistent(l_Lean_rawStx_quot___closed__8);
+l_Lean_rawStx_quot___closed__9 = _init_l_Lean_rawStx_quot___closed__9();
+lean_mark_persistent(l_Lean_rawStx_quot___closed__9);
+l_Lean_rawStx_quot___closed__10 = _init_l_Lean_rawStx_quot___closed__10();
+lean_mark_persistent(l_Lean_rawStx_quot___closed__10);
+l_Lean_rawStx_quot = _init_l_Lean_rawStx_quot();
+lean_mark_persistent(l_Lean_rawStx_quot);
 l_Lean_Parser_Tactic_withAnnotateState___closed__1 = _init_l_Lean_Parser_Tactic_withAnnotateState___closed__1();
 lean_mark_persistent(l_Lean_Parser_Tactic_withAnnotateState___closed__1);
 l_Lean_Parser_Tactic_withAnnotateState___closed__2 = _init_l_Lean_Parser_Tactic_withAnnotateState___closed__2();
@@ -49565,6 +49540,8 @@ l_Lean_Parser_Tactic_tactic___x3c_x3b_x3e__ = _init_l_Lean_Parser_Tactic_tactic_
 lean_mark_persistent(l_Lean_Parser_Tactic_tactic___x3c_x3b_x3e__);
 l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__1 = _init_l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__1();
 lean_mark_persistent(l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__1);
+l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__2 = _init_l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__2();
+lean_mark_persistent(l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tactic___x3c_x3b_x3e____1___closed__2);
 l_Lean_Parser_Tactic_refl___closed__1 = _init_l_Lean_Parser_Tactic_refl___closed__1();
 lean_mark_persistent(l_Lean_Parser_Tactic_refl___closed__1);
 l_Lean_Parser_Tactic_refl___closed__2 = _init_l_Lean_Parser_Tactic_refl___closed__2();

stage0/stdlib/Lean/Data/Json/Parser.c

@@ -56,7 +56,6 @@ LEAN_EXPORT lean_object* l_Lean_Json_Parser_num___lambda__3___closed__3___boxed_
 static lean_object* l_Lean_Json_Parser_objectCore___closed__4;
 static lean_object* l_Lean_Json_Parser_num___lambda__5___closed__2;
 static lean_object* l_Lean_Json_Parser_str___closed__1;
-LEAN_EXPORT lean_object* l_Lean_Json_Parser_strCore___lambda__1(lean_object*, uint32_t, lean_object*);
 static lean_object* l_Lean_Json_Parser_num___closed__3;
 static lean_object* l_Lean_Json_Parser_anyCore___rarg___closed__10;
 lean_object* l_Nat_repr(lean_object*);
@@ -76,7 +75,6 @@ LEAN_EXPORT lean_object* l_Lean_Json_Parser_arrayCore(lean_object*, lean_object*
 LEAN_EXPORT lean_object* l_Lean_Json_Parser_strCore(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Json_Parser_num___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_uint32_dec_eq(uint32_t, uint32_t);
-LEAN_EXPORT lean_object* l_Lean_Json_Parser_strCore___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Json_Parser_objectCore___closed__2;
 static lean_object* l_Lean_Json_Parser_num___lambda__5___closed__3;
 LEAN_EXPORT lean_object* l_Lean_Json_Parser_escapedChar___boxed__const__3;
@@ -1096,15 +1094,6 @@ return x_22;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Json_Parser_strCore___lambda__1(lean_object* x_1, uint32_t x_2, lean_object* x_3) {
-_start:
-{
-lean_object* x_4; lean_object* x_5; 
-x_4 = lean_string_push(x_1, x_2);
-x_5 = l_Lean_Json_Parser_strCore(x_4, x_3);
-return x_5;
-}
-}
 static lean_object* _init_l_Lean_Json_Parser_strCore___closed__1() {
 _start:
 {
@@ -1173,73 +1162,67 @@ return x_19;
 else
 {
 lean_object* x_20; 
-x_20 = l_Lean_Json_Parser_strCore___lambda__1(x_1, x_6, x_9);
-return x_20;
+x_20 = lean_string_push(x_1, x_6);
+x_1 = x_20;
+x_2 = x_9;
+goto _start;
 }
 }
 }
 else
 {
-lean_object* x_21; 
-x_21 = l_Lean_Json_Parser_escapedChar(x_9);
-if (lean_obj_tag(x_21) == 0)
+lean_object* x_22; 
+x_22 = l_Lean_Json_Parser_escapedChar(x_9);
+if (lean_obj_tag(x_22) == 0)
 {
-lean_object* x_22; lean_object* x_23; uint32_t x_24; lean_object* x_25; 
-x_22 = lean_ctor_get(x_21, 0);
-lean_inc(x_22);
-x_23 = lean_ctor_get(x_21, 1);
+lean_object* x_23; lean_object* x_24; uint32_t x_25; lean_object* x_26; 
+x_23 = lean_ctor_get(x_22, 0);
 lean_inc(x_23);
-lean_dec(x_21);
-x_24 = lean_unbox_uint32(x_23);
-lean_dec(x_23);
-x_25 = l_Lean_Json_Parser_strCore___lambda__1(x_1, x_24, x_22);
-return x_25;
+x_24 = lean_ctor_get(x_22, 1);
+lean_inc(x_24);
+lean_dec(x_22);
+x_25 = lean_unbox_uint32(x_24);
+lean_dec(x_24);
+x_26 = lean_string_push(x_1, x_25);
+x_1 = x_26;
+x_2 = x_23;
+goto _start;
 }
 else
 {
-uint8_t x_26; 
+uint8_t x_28; 
 lean_dec(x_1);
-x_26 = !lean_is_exclusive(x_21);
-if (x_26 == 0)
+x_28 = !lean_is_exclusive(x_22);
+if (x_28 == 0)
 {
-return x_21;
+return x_22;
 }
 else
 {
-lean_object* x_27; lean_object* x_28; lean_object* x_29; 
-x_27 = lean_ctor_get(x_21, 0);
-x_28 = lean_ctor_get(x_21, 1);
-lean_inc(x_28);
-lean_inc(x_27);
-lean_dec(x_21);
-x_29 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_29, 0, x_27);
-lean_ctor_set(x_29, 1, x_28);
-return x_29;
-}
-}
-}
-}
-else
-{
-lean_object* x_30; lean_object* x_31; 
-x_30 = l_String_Iterator_next(x_2);
-x_31 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_31, 0, x_30);
-lean_ctor_set(x_31, 1, x_1);
+lean_object* x_29; lean_object* x_30; lean_object* x_31; 
+x_29 = lean_ctor_get(x_22, 0);
+x_30 = lean_ctor_get(x_22, 1);
+lean_inc(x_30);
+lean_inc(x_29);
+lean_dec(x_22);
+x_31 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_31, 0, x_29);
+lean_ctor_set(x_31, 1, x_30);
 return x_31;
 }
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Json_Parser_strCore___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
+else
 {
-uint32_t x_4; lean_object* x_5; 
-x_4 = lean_unbox_uint32(x_2);
-lean_dec(x_2);
-x_5 = l_Lean_Json_Parser_strCore___lambda__1(x_1, x_4, x_3);
-return x_5;
+lean_object* x_32; lean_object* x_33; 
+x_32 = l_String_Iterator_next(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_1);
+return x_33;
+}
+}
 }
 }
 static lean_object* _init_l_Lean_Json_Parser_str___closed__1() {

stage0/stdlib/Lean/Elab/Syntax.c

@@ -87,7 +87,6 @@ static lean_object* l_Lean_Elab_Term_toParserDescr_processSepBy1___lambda__1___c
 static lean_object* l_Lean_Elab_Term_toParserDescr_processAtom___lambda__1___closed__3;
 static lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__13;
 static lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__41;
-static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6891____closed__1;
 LEAN_EXPORT lean_object* l_Lean_Elab_Term_toParserDescr_processSepBy1___lambda__1(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_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Term_quoteAutoTactic___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_SourceInfo_fromRef(lean_object*);
@@ -144,6 +143,7 @@ static lean_object* l_Lean_Elab_Command_expandNoKindMacroRulesAux___lambda__1___
 static lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__22;
 LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_elabSyntax___spec__6___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabSyntax___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6894____closed__1;
 lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Term_toParserDescr_process___closed__15;
 static lean_object* l_Lean_Elab_Term_toParserDescr_processAtom___closed__2;
@@ -307,7 +307,7 @@ lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__2;
 lean_object* l_String_capitalize(lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6891_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6894_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_resolveGlobalName___at_Lean_Elab_Term_toParserDescr_resolveParserName___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Term_toParserDescr_process___closed__13;
 static lean_object* l_Lean_Elab_Term_toParserDescr_processNonReserved___closed__7;
@@ -19735,7 +19735,7 @@ lean_dec(x_2);
 return x_4;
 }
 }
-static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6891____closed__1() {
+static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6894____closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@@ -19745,11 +19745,11 @@ x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6891_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6894_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6891____closed__1;
+x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6894____closed__1;
 x_3 = l_Lean_registerTraceClass(x_2, x_1);
 return x_3;
 }
@@ -20465,9 +20465,9 @@ l_Lean_Elab_Command_expandNoKindMacroRulesAux___lambda__1___closed__5 = _init_l_
 lean_mark_persistent(l_Lean_Elab_Command_expandNoKindMacroRulesAux___lambda__1___closed__5);
 l_Lean_Elab_Command_expandNoKindMacroRulesAux___lambda__1___closed__6 = _init_l_Lean_Elab_Command_expandNoKindMacroRulesAux___lambda__1___closed__6();
 lean_mark_persistent(l_Lean_Elab_Command_expandNoKindMacroRulesAux___lambda__1___closed__6);
-l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6891____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6891____closed__1();
-lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6891____closed__1);
-res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6891_(lean_io_mk_world());
+l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6894____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6894____closed__1();
+lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6894____closed__1);
+res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_6894_(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));

stage0/stdlib/Lean/Meta/Match/MatcherInfo.c

@@ -13,6 +13,8 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+static lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__3;
+static lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__5;
 size_t lean_usize_add(size_t, size_t);
 LEAN_EXPORT lean_object* l_Lean_Meta_getMatcherInfo_x3f___rarg(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_Match_addMatcherInfo___closed__7;
@@ -24,6 +26,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Match_MatcherInfo_arity___boxed(lean_object
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 uint8_t lean_usize_dec_eq(size_t, size_t);
 lean_object* lean_array_uget(lean_object*, size_t);
+LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Match_getNumEqsFromDiscrInfos___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_isMatcherCore___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_isMatcherAppCore_x3f(lean_object*, lean_object*);
 lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
@@ -48,6 +51,7 @@ size_t lean_usize_shift_right(size_t, size_t);
 LEAN_EXPORT lean_object* l_Lean_SMap_switch___at_Lean_Meta_Match_Extension_State_switch___spec__1(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_getMatcherInfo_x3f___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_SMap_insert___at_Lean_Meta_Match_Extension_State_addEntry___spec__1(lean_object*, lean_object*, lean_object*);
+uint8_t lean_usize_dec_lt(size_t, size_t);
 LEAN_EXPORT lean_object* l_Lean_Meta_Match_MatcherInfo_getFirstDiscrPos___boxed(lean_object*);
 extern lean_object* l_Lean_levelZero;
 lean_object* lean_nat_add(lean_object*, lean_object*);
@@ -55,10 +59,10 @@ lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg(lean_object*, le
 LEAN_EXPORT lean_object* l_Lean_Meta_Match_MatcherInfo_getFirstAltPos___boxed(lean_object*);
 lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
 size_t lean_uint64_to_usize(uint64_t);
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__2(lean_object*, size_t, size_t, lean_object*);
 lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_SMap_find_x3f___at_Lean_Meta_Match_Extension_getMatcherInfo_x3f___spec__1(lean_object*, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__3(lean_object*, size_t, size_t, lean_object*);
 lean_object* lean_st_ref_take(lean_object*, lean_object*);
 static lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_Meta_Match_Extension_State_addEntry___spec__3___closed__3;
 lean_object* lean_nat_sub(lean_object*, lean_object*);
@@ -70,7 +74,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Match_Extension_State_addEntry(lean_object*
 static lean_object* l_Lean_Meta_Match_Extension_instInhabitedState___closed__1;
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Lean_Meta_isMatcherAppCore(lean_object*, lean_object*);
-static lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__1;
 lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_mkHashMapImp___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_Meta_Match_Extension_State_addEntry___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -90,14 +93,11 @@ static lean_object* l_Lean_Meta_Match_addMatcherInfo___closed__8;
 size_t lean_usize_shift_left(size_t, size_t);
 lean_object* lean_array_to_list(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey___boxed(lean_object*);
-static lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__2;
-LEAN_EXPORT lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__1(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_instInhabitedExpr;
-static lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__6;
 LEAN_EXPORT lean_object* l_Lean_Meta_Match_addMatcherInfo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_usize_modn(size_t, lean_object*);
 uint8_t l_Lean_Expr_isConst(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_instInhabitedDiscrInfo;
 LEAN_EXPORT lean_object* l_Lean_Meta_Match_Extension_addMatcherInfo(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_Match_MatcherInfo_getMotivePos___boxed(lean_object*);
 size_t lean_usize_mul(size_t, size_t);
@@ -111,9 +111,11 @@ LEAN_EXPORT lean_object* l_Lean_Meta_matchMatcherApp_x3f___rarg(lean_object*, le
 lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
 size_t lean_usize_land(size_t, size_t);
 lean_object* l_Lean_SimplePersistentEnvExtension_getState___rarg(lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__4;
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_getNumEqsFromDiscrInfos(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_Match_addMatcherInfo___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_Meta_Match_Extension_State_addEntry___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_MatcherInfo_getNumDiscrEqs___boxed(lean_object*);
 static lean_object* l_Lean_Meta_Match_addMatcherInfo___closed__4;
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Meta_Match_Extension_getMatcherInfo_x3f___spec__2(lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_Match_addMatcherInfo___closed__3;
@@ -124,17 +126,19 @@ LEAN_EXPORT lean_object* l_Lean_Meta_matchMatcherApp_x3f(lean_object*);
 lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_HashMap_insert___at_Lean_Meta_Match_Extension_State_addEntry___spec__6(lean_object*, lean_object*, lean_object*);
 lean_object* lean_list_to_array(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308_(lean_object*);
 static lean_object* l_Lean_Meta_Match_addMatcherInfo___closed__9;
 LEAN_EXPORT lean_object* l_Lean_Meta_isMatcherApp___rarg(lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__1;
+LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Match_getNumEqsFromDiscrInfos___spec__1(lean_object*, size_t, size_t, lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 uint8_t lean_usize_dec_le(size_t, size_t);
 lean_object* l_Lean_mkApp(lean_object*, lean_object*);
 static size_t l_Std_PersistentHashMap_insertAux___at_Lean_Meta_Match_Extension_State_addEntry___spec__3___closed__2;
 static size_t l_Std_PersistentHashMap_insertAux___at_Lean_Meta_Match_Extension_State_addEntry___spec__3___closed__1;
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_getNumEqsFromDiscrInfos___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_MatcherApp_toExpr(lean_object*);
-LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____lambda__1(lean_object*);
+static lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__4;
 LEAN_EXPORT lean_object* l_Lean_Meta_getMatcherInfoCore_x3f(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_Match_Extension_instInhabitedState;
 LEAN_EXPORT lean_object* l_Std_HashMapImp_expand___at_Lean_Meta_Match_Extension_State_addEntry___spec__8(lean_object*, lean_object*);
@@ -145,10 +149,10 @@ lean_object* lean_nat_mul(lean_object*, lean_object*);
 lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_Match_addMatcherInfo___closed__6;
-static lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__3;
 static lean_object* l_Lean_Meta_Match_addMatcherInfo___closed__5;
 lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_Match_MatcherInfo_arity(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_MatcherInfo_getNumDiscrEqs(lean_object*);
 lean_object* lean_mk_array(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_isMatcherAppCore___boxed(lean_object*, lean_object*);
 extern lean_object* l_Lean_Expr_instBEqExpr;
@@ -157,24 +161,45 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Match_MatcherInfo_getFirstAltPos(lean_objec
 LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Meta_Match_Extension_State_map___default___spec__1___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Std_AssocList_find_x3f___at_Lean_Meta_Match_Extension_getMatcherInfo_x3f___spec__6(lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_Match_Extension_State_map___default___closed__3;
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_DiscrInfo_hName_x3f___default;
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAux___at_Lean_Meta_Match_Extension_getMatcherInfo_x3f___spec__3(lean_object*, size_t, lean_object*);
-LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__2(lean_object*, size_t, size_t, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_isMatcherApp___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__2;
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____lambda__1(lean_object*);
 lean_object* l_Lean_Expr_getAppFn(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_Match_MatcherInfo_numAlts(lean_object*);
 lean_object* lean_usize_to_nat(size_t);
 LEAN_EXPORT lean_object* l_Lean_Meta_Match_Extension_getMatcherInfo_x3f(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_AssocList_foldlM___at_Lean_Meta_Match_Extension_State_addEntry___spec__10(lean_object*, lean_object*);
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
+static lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__6;
 lean_object* l_Lean_Expr_constName_x21(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__1(lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_mkEmptyEntries(lean_object*, lean_object*);
-static lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__5;
 LEAN_EXPORT lean_object* l_Std_AssocList_find_x3f___at_Lean_Meta_Match_Extension_getMatcherInfo_x3f___spec__6___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_Meta_Match_Extension_getMatcherInfo_x3f___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__3(lean_object*, size_t, size_t, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_isMatcher___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_Meta_Match_Extension_State_addEntry___spec__3(lean_object*, size_t, size_t, lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
+static lean_object* _init_l_Lean_Meta_Match_DiscrInfo_hName_x3f___default() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_box(0);
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_Meta_Match_instInhabitedDiscrInfo() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_box(0);
+return x_1;
+}
+}
 LEAN_EXPORT lean_object* l_Lean_Meta_Match_MatcherInfo_numAlts(lean_object* x_1) {
 _start:
 {
@@ -278,6 +303,96 @@ lean_dec(x_1);
 return x_2;
 }
 }
+LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Match_getNumEqsFromDiscrInfos___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
+_start:
+{
+uint8_t x_5; 
+x_5 = lean_usize_dec_lt(x_3, x_2);
+if (x_5 == 0)
+{
+return x_4;
+}
+else
+{
+lean_object* x_6; 
+x_6 = lean_array_uget(x_1, x_3);
+if (lean_obj_tag(x_6) == 0)
+{
+size_t x_7; size_t x_8; 
+x_7 = 1;
+x_8 = lean_usize_add(x_3, x_7);
+x_3 = x_8;
+goto _start;
+}
+else
+{
+lean_object* x_10; lean_object* x_11; size_t x_12; size_t x_13; 
+lean_dec(x_6);
+x_10 = lean_unsigned_to_nat(1u);
+x_11 = lean_nat_add(x_4, x_10);
+lean_dec(x_4);
+x_12 = 1;
+x_13 = lean_usize_add(x_3, x_12);
+x_3 = x_13;
+x_4 = x_11;
+goto _start;
+}
+}
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_getNumEqsFromDiscrInfos(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; size_t x_3; size_t x_4; lean_object* x_5; lean_object* x_6; 
+x_2 = lean_array_get_size(x_1);
+x_3 = lean_usize_of_nat(x_2);
+lean_dec(x_2);
+x_4 = 0;
+x_5 = lean_unsigned_to_nat(0u);
+x_6 = l_Array_forInUnsafe_loop___at_Lean_Meta_Match_getNumEqsFromDiscrInfos___spec__1(x_1, x_3, x_4, x_5);
+return x_6;
+}
+}
+LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Match_getNumEqsFromDiscrInfos___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+size_t x_5; size_t x_6; lean_object* x_7; 
+x_5 = lean_unbox_usize(x_2);
+lean_dec(x_2);
+x_6 = lean_unbox_usize(x_3);
+lean_dec(x_3);
+x_7 = l_Array_forInUnsafe_loop___at_Lean_Meta_Match_getNumEqsFromDiscrInfos___spec__1(x_1, x_5, x_6, x_4);
+lean_dec(x_1);
+return x_7;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_getNumEqsFromDiscrInfos___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Lean_Meta_Match_getNumEqsFromDiscrInfos(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_MatcherInfo_getNumDiscrEqs(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; 
+x_2 = lean_ctor_get(x_1, 4);
+x_3 = l_Lean_Meta_Match_getNumEqsFromDiscrInfos(x_2);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_MatcherInfo_getNumDiscrEqs___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Lean_Meta_Match_MatcherInfo_getNumDiscrEqs(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
 LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Meta_Match_Extension_State_map___default___spec__1(lean_object* x_1) {
 _start:
 {
@@ -1416,7 +1531,7 @@ x_2 = l_Lean_SMap_switch___at_Lean_Meta_Match_Extension_State_switch___spec__1(x
 return x_2;
 }
 }
-LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__2(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__2(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
 _start:
 {
 uint8_t x_5; 
@@ -1438,7 +1553,7 @@ return x_4;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__3(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__3(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
 _start:
 {
 uint8_t x_5; 
@@ -1476,7 +1591,7 @@ size_t x_15; size_t x_16; lean_object* x_17;
 x_15 = 0;
 x_16 = lean_usize_of_nat(x_7);
 lean_dec(x_7);
-x_17 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__2(x_6, x_15, x_16, x_4);
+x_17 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__2(x_6, x_15, x_16, x_4);
 lean_dec(x_6);
 x_2 = x_11;
 x_4 = x_17;
@@ -1490,7 +1605,7 @@ return x_4;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__1(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; lean_object* x_4; uint8_t x_5; 
@@ -1519,24 +1634,24 @@ size_t x_7; size_t x_8; lean_object* x_9;
 x_7 = 0;
 x_8 = lean_usize_of_nat(x_3);
 lean_dec(x_3);
-x_9 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__3(x_2, x_7, x_8, x_1);
+x_9 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__3(x_2, x_7, x_8, x_1);
 lean_dec(x_2);
 return x_9;
 }
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____lambda__1(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____lambda__1(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_2 = l_Lean_Meta_Match_Extension_instInhabitedState___closed__2;
-x_3 = l_Lean_mkStateFromImportedEntries___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__1(x_2, x_1);
+x_3 = l_Lean_mkStateFromImportedEntries___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__1(x_2, x_1);
 x_4 = l_Lean_SMap_switch___at_Lean_Meta_Match_Extension_State_switch___spec__1(x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__1() {
+static lean_object* _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -1544,17 +1659,17 @@ x_1 = lean_mk_string("matcher");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__2() {
+static lean_object* _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__1;
+x_2 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__3() {
+static lean_object* _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -1563,7 +1678,7 @@ lean_closure_set(x_1, 0, lean_box(0));
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__4() {
+static lean_object* _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__4() {
 _start:
 {
 lean_object* x_1; 
@@ -1571,22 +1686,22 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Meta_Match_Extension_State_addEntry), 2,
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__5() {
+static lean_object* _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__5() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____lambda__1), 1, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____lambda__1), 1, 0);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__6() {
+static lean_object* _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__2;
-x_2 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__4;
-x_3 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__5;
-x_4 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__3;
+x_1 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__2;
+x_2 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__4;
+x_3 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__5;
+x_4 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__3;
 x_5 = lean_alloc_ctor(0, 4, 0);
 lean_ctor_set(x_5, 0, x_1);
 lean_ctor_set(x_5, 1, x_2);
@@ -1595,16 +1710,16 @@ lean_ctor_set(x_5, 3, x_4);
 return x_5;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__6;
+x_2 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__6;
 x_3 = l_Lean_registerSimplePersistentEnvExtension___rarg(x_2, x_1);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
 size_t x_5; size_t x_6; lean_object* x_7; 
@@ -1612,12 +1727,12 @@ x_5 = lean_unbox_usize(x_2);
 lean_dec(x_2);
 x_6 = lean_unbox_usize(x_3);
 lean_dec(x_3);
-x_7 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__2(x_1, x_5, x_6, x_4);
+x_7 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__2(x_1, x_5, x_6, x_4);
 lean_dec(x_1);
 return x_7;
 }
 }
-LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
 size_t x_5; size_t x_6; lean_object* x_7; 
@@ -1625,7 +1740,7 @@ x_5 = lean_unbox_usize(x_2);
 lean_dec(x_2);
 x_6 = lean_unbox_usize(x_3);
 lean_dec(x_3);
-x_7 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____spec__3(x_1, x_5, x_6, x_4);
+x_7 = l_Array_foldlMUnsafe_fold___at_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____spec__3(x_1, x_5, x_6, x_4);
 lean_dec(x_1);
 return x_7;
 }
@@ -2851,6 +2966,10 @@ lean_dec_ref(res);
 res = initialize_Lean_Meta_Basic(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l_Lean_Meta_Match_DiscrInfo_hName_x3f___default = _init_l_Lean_Meta_Match_DiscrInfo_hName_x3f___default();
+lean_mark_persistent(l_Lean_Meta_Match_DiscrInfo_hName_x3f___default);
+l_Lean_Meta_Match_instInhabitedDiscrInfo = _init_l_Lean_Meta_Match_instInhabitedDiscrInfo();
+lean_mark_persistent(l_Lean_Meta_Match_instInhabitedDiscrInfo);
 l_Lean_Meta_Match_Extension_State_map___default___closed__1 = _init_l_Lean_Meta_Match_Extension_State_map___default___closed__1();
 lean_mark_persistent(l_Lean_Meta_Match_Extension_State_map___default___closed__1);
 l_Lean_Meta_Match_Extension_State_map___default___closed__2 = _init_l_Lean_Meta_Match_Extension_State_map___default___closed__2();
@@ -2869,19 +2988,19 @@ l_Std_PersistentHashMap_insertAux___at_Lean_Meta_Match_Extension_State_addEntry_
 l_Std_PersistentHashMap_insertAux___at_Lean_Meta_Match_Extension_State_addEntry___spec__3___closed__2 = _init_l_Std_PersistentHashMap_insertAux___at_Lean_Meta_Match_Extension_State_addEntry___spec__3___closed__2();
 l_Std_PersistentHashMap_insertAux___at_Lean_Meta_Match_Extension_State_addEntry___spec__3___closed__3 = _init_l_Std_PersistentHashMap_insertAux___at_Lean_Meta_Match_Extension_State_addEntry___spec__3___closed__3();
 lean_mark_persistent(l_Std_PersistentHashMap_insertAux___at_Lean_Meta_Match_Extension_State_addEntry___spec__3___closed__3);
-l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__1 = _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__1();
-lean_mark_persistent(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__1);
-l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__2 = _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__2();
-lean_mark_persistent(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__2);
-l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__3 = _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__3();
-lean_mark_persistent(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__3);
-l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__4 = _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__4();
-lean_mark_persistent(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__4);
-l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__5 = _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__5();
-lean_mark_persistent(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__5);
-l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__6 = _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__6();
-lean_mark_persistent(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177____closed__6);
-if (builtin) {res = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_177_(lean_io_mk_world());
+l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__1 = _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__1();
+lean_mark_persistent(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__1);
+l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__2 = _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__2();
+lean_mark_persistent(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__2);
+l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__3 = _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__3();
+lean_mark_persistent(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__3);
+l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__4 = _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__4();
+lean_mark_persistent(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__4);
+l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__5 = _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__5();
+lean_mark_persistent(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__5);
+l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__6 = _init_l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__6();
+lean_mark_persistent(l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308____closed__6);
+if (builtin) {res = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_308_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 l_Lean_Meta_Match_Extension_extension = lean_io_result_get_value(res);
 lean_mark_persistent(l_Lean_Meta_Match_Extension_extension);

stage0/stdlib/Lean/PrettyPrinter/Formatter.c

@@ -24,9 +24,8 @@ uint8_t l_Lean_Syntax_isAntiquotSuffixSplice(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_visitArgs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_usize_add(size_t, size_t);
 extern lean_object* l_Lean_fieldIdxKind;
-LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_4227_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_4272_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_checkTailWs_formatter___rarg(lean_object*);
-static lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__1;
 uint8_t l_Lean_Syntax_isTokenAntiquot(lean_object*);
 uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_810____at_Lean_Parser_ParserState_hasError___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
@@ -56,13 +55,11 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_sepByNoAntiquot_formatte
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 uint8_t lean_usize_dec_eq(size_t, size_t);
 lean_object* lean_array_uget(lean_object*, size_t);
-LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_pushLine___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___closed__8;
 LEAN_EXPORT lean_object* l_Lean_addTrace___at_Lean_PrettyPrinter_Formatter_categoryFormatterCore___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_pushToken___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_checkNoImmediateColon_formatter___rarg(lean_object*);
-static lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__2;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_visitArgs___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_formatTerm(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_Traverser_up(lean_object*);
@@ -152,7 +149,9 @@ LEAN_EXPORT lean_object* l_Lean_addTrace___at_Lean_PrettyPrinter_format___spec__
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_throwBacktrack___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_pushToken___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_fill(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__3;
 static lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___closed__9;
+static lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__7;
 lean_object* l_Lean_Parser_registerAliasCore___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_getStack___boxed(lean_object*);
 static lean_object* l_Lean_PrettyPrinter_Formatter_checkKind___closed__5;
@@ -224,6 +223,7 @@ static lean_object* l_Lean_PrettyPrinter_Formatter_symbolNoAntiquot_formatter___
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___closed__5;
 static lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___closed__3;
+static lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__5;
 lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_instMonadTraverserFormatterM___lambda__1___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_node_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -239,7 +239,7 @@ lean_object* lean_st_mk_ref(lean_object*, lean_object*);
 static lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___lambda__1___closed__4;
 lean_object* l_Lean_Syntax_getId(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_sepBy1NoAntiquot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_skip_formatter(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_PrettyPrinter_format___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_charLitKind;
@@ -258,6 +258,7 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_errorAtSavedPos_formatte
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_checkNoWsBefore_formatter___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_PrettyPrinter_Formatter_0__Lean_PrettyPrinter_Formatter_getExprPos_x3f___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_instOrElseFormatterM(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_scientificLitNoAntiquot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_PrettyPrinter_Formatter_0__Lean_PrettyPrinter_Formatter_getExprPos_x3f(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_formatterAttribute;
@@ -271,6 +272,7 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_checkLhsPrec_formatter(l
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_checkKind___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_mkAntiquot_formatter_x27___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Syntax_MonadTraverser_goUp___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__6;
 lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_reverse___rarg(lean_object*);
 static lean_object* l_Lean_PrettyPrinter_Formatter_identNoAntiquot_formatter___closed__2;
@@ -292,8 +294,10 @@ LEAN_EXPORT lean_object* l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPri
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Nat_forM_loop___at_Lean_PrettyPrinter_Formatter_manyNoAntiquot_formatter___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_PrettyPrinter_formatTactic___closed__2;
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_ite(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__2;
 size_t lean_usize_of_nat(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_checkLineEq_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_format(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -367,18 +371,18 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_instMonadTraverserFormat
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_evalInsideQuot_formatter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_getStackSize___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_errorAtSavedPos_formatter(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__3;
 LEAN_EXPORT lean_object* l_Lean_Syntax_MonadTraverser_getCur___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__1(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_withForbidden_formatter___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_pushToken___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_instCoeForAllFormatterFormatterAliasValue(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_checkNoWsBefore_formatter(lean_object*);
 static lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___closed__2;
-static lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__5;
+static lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__1;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_setLhsPrec_formatter(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_pushToken___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_withOpen_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__4;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_pushNone_formatter___boxed(lean_object*);
 lean_object* l_Std_Format_getIndent(lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_PrettyPrinter_Formatter_0__Lean_PrettyPrinter_Formatter_push(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -391,6 +395,7 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_visitAtom___lambda__1___
 static lean_object* l_Lean_PrettyPrinter_Formatter_pushToken___lambda__2___closed__3;
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_checkNoImmediateColon_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_skip_formatter___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_parseToken(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_pushToken___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -413,7 +418,7 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_withoutInfo_formatter(le
 extern lean_object* l_Std_instInhabitedFormat;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_concat___lambda__1___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_parserOfStack_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_4536_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_4581_(lean_object*);
 static lean_object* l_Lean_addTrace___at_Lean_PrettyPrinter_Formatter_categoryFormatterCore___spec__2___closed__7;
 lean_object* lean_int_sub(lean_object*, lean_object*);
 static lean_object* l_Lean_PrettyPrinter_Formatter_symbolNoAntiquot_formatter___closed__6;
@@ -435,7 +440,6 @@ lean_object* lean_simp_macro_scopes(lean_object*);
 static lean_object* l_Lean_addTrace___at_Lean_PrettyPrinter_Formatter_categoryFormatterCore___spec__2___closed__5;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_pushToken___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___closed__2;
-static lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__4;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_checkColGe_formatter___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_FormatterM_orElse(lean_object*);
 lean_object* l_Lean_KeyedDeclsAttribute_init___rarg(lean_object*, lean_object*, lean_object*);
@@ -4812,13 +4816,25 @@ return x_53;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___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) {
 _start:
 {
+lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_7 = l___private_Lean_PrettyPrinter_Formatter_0__Lean_PrettyPrinter_Formatter_push(x_1, x_2, x_3, x_4, x_5, x_6);
+x_8 = lean_ctor_get(x_7, 1);
+lean_inc(x_8);
+lean_dec(x_7);
+x_9 = l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__2___rarg(x_3, x_4, x_5, x_8);
+return x_9;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3(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; 
 x_7 = l_Lean_Syntax_getKind(x_1);
 x_8 = l_Lean_PrettyPrinter_Formatter_formatterForKindUnsafe(x_7, x_2, x_3, x_4, x_5, x_6);
 return x_8;
 }
 }
-static lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__1() {
+static lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -4826,7 +4842,7 @@ x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_categoryFormatte
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__2() {
+static lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__2() {
 _start:
 {
 lean_object* x_1; 
@@ -4834,17 +4850,35 @@ x_1 = lean_mk_string("choice");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__3() {
+static lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__2;
+x_2 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__2;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__4() {
+static lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__4() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("rawStx");
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__4;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__6() {
 _start:
 {
 lean_object* x_1; 
@@ -4852,128 +4886,197 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Syntax_MonadTraverser_getCur___at_Lean_P
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__5() {
+static lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__7() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__2), 6, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3), 6, 0);
 return x_1;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3(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_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__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, lean_object* x_8) {
 _start:
 {
 lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; 
-x_9 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__1;
+x_9 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__1;
+lean_inc(x_1);
 x_10 = l_Lean_Syntax_getKind(x_1);
-x_11 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__3;
+x_11 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__3;
 x_12 = lean_name_eq(x_10, x_11);
 if (x_12 == 0)
 {
-uint8_t x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; 
-x_13 = 1;
-x_14 = l_Lean_Name_toString(x_2, x_13);
-x_15 = lean_box(0);
-x_16 = lean_box(x_13);
-x_17 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_mkAntiquot_formatter_x27___boxed), 8, 3);
-lean_closure_set(x_17, 0, x_14);
-lean_closure_set(x_17, 1, x_15);
-lean_closure_set(x_17, 2, x_16);
-x_18 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_formatterForKindUnsafe), 6, 1);
-lean_closure_set(x_18, 0, x_10);
+lean_object* x_13; uint8_t x_14; 
+x_13 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__5;
+x_14 = lean_name_eq(x_2, x_13);
+if (x_14 == 0)
+{
+uint8_t 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_dec(x_1);
+x_15 = 1;
+x_16 = l_Lean_Name_toString(x_2, x_15);
+x_17 = lean_box(0);
+x_18 = lean_box(x_15);
+x_19 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_mkAntiquot_formatter_x27___boxed), 8, 3);
+lean_closure_set(x_19, 0, x_16);
+lean_closure_set(x_19, 1, x_17);
+lean_closure_set(x_19, 2, x_18);
+x_20 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_formatterForKindUnsafe), 6, 1);
+lean_closure_set(x_20, 0, x_10);
 lean_inc(x_7);
 lean_inc(x_6);
 lean_inc(x_5);
 lean_inc(x_4);
-x_19 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_17, x_18, x_4, x_5, x_6, x_7, x_8);
-if (lean_obj_tag(x_19) == 0)
+x_21 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_19, x_20, x_4, x_5, x_6, x_7, x_8);
+if (lean_obj_tag(x_21) == 0)
 {
-lean_object* x_20; lean_object* x_21; lean_object* x_22; 
-x_20 = lean_ctor_get(x_19, 0);
-lean_inc(x_20);
-x_21 = lean_ctor_get(x_19, 1);
-lean_inc(x_21);
-lean_dec(x_19);
-x_22 = lean_apply_6(x_9, x_20, x_4, x_5, x_6, x_7, x_21);
-return x_22;
+lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+x_22 = lean_ctor_get(x_21, 0);
+lean_inc(x_22);
+x_23 = lean_ctor_get(x_21, 1);
+lean_inc(x_23);
+lean_dec(x_21);
+x_24 = lean_apply_6(x_9, x_22, x_4, x_5, x_6, x_7, x_23);
+return x_24;
 }
 else
 {
-uint8_t x_23; 
+uint8_t x_25; 
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_4);
-x_23 = !lean_is_exclusive(x_19);
-if (x_23 == 0)
+x_25 = !lean_is_exclusive(x_21);
+if (x_25 == 0)
 {
-return x_19;
+return x_21;
 }
 else
 {
-lean_object* x_24; lean_object* x_25; lean_object* x_26; 
-x_24 = lean_ctor_get(x_19, 0);
-x_25 = lean_ctor_get(x_19, 1);
-lean_inc(x_25);
-lean_inc(x_24);
-lean_dec(x_19);
-x_26 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_26, 0, x_24);
-lean_ctor_set(x_26, 1, x_25);
-return x_26;
+lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_26 = lean_ctor_get(x_21, 0);
+x_27 = lean_ctor_get(x_21, 1);
+lean_inc(x_27);
+lean_inc(x_26);
+lean_dec(x_21);
+x_28 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_28, 0, x_26);
+lean_ctor_set(x_28, 1, x_27);
+return x_28;
 }
 }
 }
 else
 {
-lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; 
+uint8_t x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; 
+lean_dec(x_10);
+x_29 = 1;
+x_30 = l_Lean_Name_toString(x_2, x_29);
+x_31 = lean_box(0);
+x_32 = lean_box(x_29);
+x_33 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_mkAntiquot_formatter_x27___boxed), 8, 3);
+lean_closure_set(x_33, 0, x_30);
+lean_closure_set(x_33, 1, x_31);
+lean_closure_set(x_33, 2, x_32);
+x_34 = 0;
+x_35 = lean_unsigned_to_nat(0u);
+x_36 = l_Lean_Syntax_formatStxAux(x_31, x_34, x_35, x_1);
+x_37 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__2___boxed), 6, 1);
+lean_closure_set(x_37, 0, x_36);
+lean_inc(x_7);
+lean_inc(x_6);
+lean_inc(x_5);
+lean_inc(x_4);
+x_38 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_33, x_37, x_4, x_5, x_6, x_7, x_8);
+if (lean_obj_tag(x_38) == 0)
+{
+lean_object* x_39; lean_object* x_40; lean_object* x_41; 
+x_39 = lean_ctor_get(x_38, 0);
+lean_inc(x_39);
+x_40 = lean_ctor_get(x_38, 1);
+lean_inc(x_40);
+lean_dec(x_38);
+x_41 = lean_apply_6(x_9, x_39, x_4, x_5, x_6, x_7, x_40);
+return x_41;
+}
+else
+{
+uint8_t x_42; 
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+x_42 = !lean_is_exclusive(x_38);
+if (x_42 == 0)
+{
+return x_38;
+}
+else
+{
+lean_object* x_43; lean_object* x_44; lean_object* x_45; 
+x_43 = lean_ctor_get(x_38, 0);
+x_44 = lean_ctor_get(x_38, 1);
+lean_inc(x_44);
+lean_inc(x_43);
+lean_dec(x_38);
+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;
+}
+}
+}
+}
+else
+{
+lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; 
 lean_dec(x_10);
 lean_dec(x_2);
-x_27 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__4;
-x_28 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__5;
-x_29 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_PrettyPrinter_Formatter_categoryFormatterCore___spec__1___rarg), 7, 2);
-lean_closure_set(x_29, 0, x_27);
-lean_closure_set(x_29, 1, x_28);
+lean_dec(x_1);
+x_46 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__6;
+x_47 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__7;
+x_48 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_PrettyPrinter_Formatter_categoryFormatterCore___spec__1___rarg), 7, 2);
+lean_closure_set(x_48, 0, x_46);
+lean_closure_set(x_48, 1, x_47);
 lean_inc(x_7);
 lean_inc(x_6);
 lean_inc(x_5);
 lean_inc(x_4);
-x_30 = l_Lean_PrettyPrinter_Formatter_visitArgs(x_29, x_4, x_5, x_6, x_7, x_8);
-if (lean_obj_tag(x_30) == 0)
+x_49 = l_Lean_PrettyPrinter_Formatter_visitArgs(x_48, x_4, x_5, x_6, x_7, x_8);
+if (lean_obj_tag(x_49) == 0)
 {
-lean_object* x_31; lean_object* x_32; lean_object* x_33; 
-x_31 = lean_ctor_get(x_30, 0);
-lean_inc(x_31);
-x_32 = lean_ctor_get(x_30, 1);
-lean_inc(x_32);
-lean_dec(x_30);
-x_33 = lean_apply_6(x_9, x_31, x_4, x_5, x_6, x_7, x_32);
-return x_33;
+lean_object* x_50; lean_object* x_51; lean_object* x_52; 
+x_50 = lean_ctor_get(x_49, 0);
+lean_inc(x_50);
+x_51 = lean_ctor_get(x_49, 1);
+lean_inc(x_51);
+lean_dec(x_49);
+x_52 = lean_apply_6(x_9, x_50, x_4, x_5, x_6, x_7, x_51);
+return x_52;
 }
 else
 {
-uint8_t x_34; 
+uint8_t x_53; 
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_4);
-x_34 = !lean_is_exclusive(x_30);
-if (x_34 == 0)
+x_53 = !lean_is_exclusive(x_49);
+if (x_53 == 0)
 {
-return x_30;
+return x_49;
 }
 else
 {
-lean_object* x_35; lean_object* x_36; lean_object* x_37; 
-x_35 = lean_ctor_get(x_30, 0);
-x_36 = lean_ctor_get(x_30, 1);
-lean_inc(x_36);
-lean_inc(x_35);
-lean_dec(x_30);
-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_54; lean_object* x_55; lean_object* x_56; 
+x_54 = lean_ctor_get(x_49, 0);
+x_55 = lean_ctor_get(x_49, 1);
+lean_inc(x_55);
+lean_inc(x_54);
+lean_dec(x_49);
+x_56 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_56, 0, x_54);
+lean_ctor_set(x_56, 1, x_55);
+return x_56;
 }
 }
 }
@@ -5099,7 +5202,7 @@ if (x_21 == 0)
 {
 lean_object* x_23; lean_object* x_24; 
 x_23 = lean_box(0);
-x_24 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3(x_18, x_1, x_23, x_2, x_3, x_4, x_5, x_22);
+x_24 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4(x_18, x_1, x_23, x_2, x_3, x_4, x_5, x_22);
 return x_24;
 }
 else
@@ -5126,7 +5229,7 @@ lean_inc(x_35);
 x_36 = lean_ctor_get(x_34, 1);
 lean_inc(x_36);
 lean_dec(x_34);
-x_37 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3(x_18, x_1, x_35, x_2, x_3, x_4, x_5, x_36);
+x_37 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4(x_18, x_1, x_35, x_2, x_3, x_4, x_5, x_36);
 lean_dec(x_35);
 return x_37;
 }
@@ -5203,7 +5306,7 @@ if (x_61 == 0)
 {
 lean_object* x_63; lean_object* x_64; 
 x_63 = lean_box(0);
-x_64 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3(x_58, x_1, x_63, x_2, x_3, x_4, x_5, x_62);
+x_64 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4(x_58, x_1, x_63, x_2, x_3, x_4, x_5, x_62);
 return x_64;
 }
 else
@@ -5230,7 +5333,7 @@ lean_inc(x_75);
 x_76 = lean_ctor_get(x_74, 1);
 lean_inc(x_76);
 lean_dec(x_74);
-x_77 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3(x_58, x_1, x_75, x_2, x_3, x_4, x_5, x_76);
+x_77 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4(x_58, x_1, x_75, x_2, x_3, x_4, x_5, x_76);
 lean_dec(x_75);
 return x_77;
 }
@@ -5275,11 +5378,23 @@ lean_dec(x_1);
 return x_7;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___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_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__2___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) {
+_start:
+{
+lean_object* x_7; 
+x_7 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_7;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__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, lean_object* x_8) {
 _start:
 {
 lean_object* x_9; 
-x_9 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
+x_9 = l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
 lean_dec(x_3);
 return x_9;
 }
@@ -7776,7 +7891,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_PrettyPrinter_Formatter_symbolNoAntiquot_formatter___closed__5;
 x_2 = l_Lean_PrettyPrinter_Formatter_symbolNoAntiquot_formatter___closed__6;
-x_3 = lean_unsigned_to_nat(369u);
+x_3 = lean_unsigned_to_nat(371u);
 x_4 = lean_unsigned_to_nat(42u);
 x_5 = l_Lean_PrettyPrinter_Formatter_symbolNoAntiquot_formatter___closed__7;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -10207,7 +10322,7 @@ x_10 = l_Lean_PrettyPrinter_Formatter_ite___rarg(x_9, x_2, x_3, x_4, x_5, x_6, x
 return x_10;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_4227_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_4272_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; uint8_t x_4; 
@@ -11005,7 +11120,7 @@ x_6 = l_Lean_PrettyPrinter_formatCategory(x_5, x_1, x_2, x_3, x_4);
 return x_6;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_4536_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_4581_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
@@ -11155,16 +11270,20 @@ l_Lean_addTrace___at_Lean_PrettyPrinter_Formatter_categoryFormatterCore___spec__
 lean_mark_persistent(l_Lean_addTrace___at_Lean_PrettyPrinter_Formatter_categoryFormatterCore___spec__2___closed__6);
 l_Lean_addTrace___at_Lean_PrettyPrinter_Formatter_categoryFormatterCore___spec__2___closed__7 = _init_l_Lean_addTrace___at_Lean_PrettyPrinter_Formatter_categoryFormatterCore___spec__2___closed__7();
 lean_mark_persistent(l_Lean_addTrace___at_Lean_PrettyPrinter_Formatter_categoryFormatterCore___spec__2___closed__7);
-l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__1 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__1();
-lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__1);
-l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__2 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__2();
-lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__2);
-l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__3 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__3();
-lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__3);
-l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__4 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__4();
-lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__4);
-l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__5 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__5();
-lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__3___closed__5);
+l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__1 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__1();
+lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__1);
+l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__2 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__2();
+lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__2);
+l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__3 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__3();
+lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__3);
+l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__4 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__4();
+lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__4);
+l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__5 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__5();
+lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__5);
+l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__6 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__6();
+lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__6);
+l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__7 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__7();
+lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___lambda__4___closed__7);
 l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___closed__1 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___closed__1();
 lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___closed__1);
 l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___closed__2 = _init_l_Lean_PrettyPrinter_Formatter_categoryFormatterCore___closed__2();
@@ -11243,7 +11362,7 @@ l_Lean_PrettyPrinter_Formatter_identNoAntiquot_formatter___closed__2 = _init_l_L
 lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_identNoAntiquot_formatter___closed__2);
 l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___boxed__const__1 = _init_l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___boxed__const__1();
 lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___boxed__const__1);
-if (builtin) {res = l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_4227_(lean_io_mk_world());
+if (builtin) {res = l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_4272_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 l_Lean_PrettyPrinter_Formatter_formatterAliasesRef = lean_io_result_get_value(res);
 lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_formatterAliasesRef);
@@ -11272,7 +11391,7 @@ l_Lean_PrettyPrinter_formatCommand___closed__1 = _init_l_Lean_PrettyPrinter_form
 lean_mark_persistent(l_Lean_PrettyPrinter_formatCommand___closed__1);
 l_Lean_PrettyPrinter_formatCommand___closed__2 = _init_l_Lean_PrettyPrinter_formatCommand___closed__2();
 lean_mark_persistent(l_Lean_PrettyPrinter_formatCommand___closed__2);
-res = l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_4536_(lean_io_mk_world());
+res = l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_4581_(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));

stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c

@@ -26,6 +26,7 @@ static lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_term_parenth
 static lean_object* l_Lean_PrettyPrinter_Parenthesizer_parenthesizerForKindUnsafe___closed__3;
 size_t lean_usize_add(size_t, size_t);
 static lean_object* l_Lean_PrettyPrinter_mkCategoryParenthesizerAttribute___lambda__1___closed__1;
+static lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__3;
 static lean_object* l_Lean_PrettyPrinter_Parenthesizer_term_parenthesizer___lambda__1___closed__1;
 static lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___lambda__4___closed__2;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkNoImmediateColon_parenthesizer___rarg(lean_object*);
@@ -41,6 +42,7 @@ LEAN_EXPORT lean_object* l_List_forM___at_Lean_PrettyPrinter_Parenthesizer_sepBy
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_charLitNoAntiquot_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_pushNone_parenthesizer(lean_object*);
+static lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__5;
 static lean_object* l_Lean_PrettyPrinter_parenthesize___closed__1;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_rawIdentNoAntiquot_parenthesizer___boxed(lean_object*);
 static lean_object* l_Lean_PrettyPrinter_mkCategoryParenthesizerAttribute___lambda__1___closed__2;
@@ -87,7 +89,7 @@ lean_object* lean_environment_find(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Syntax_MonadTraverser_goUp___at_Lean_PrettyPrinter_Parenthesizer_visitArgs___spec__4___boxed(lean_object*);
 uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_4149_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_4170_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___lambda__9___boxed(lean_object**);
 LEAN_EXPORT lean_object* l_Lean_Syntax_MonadTraverser_setCur___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_PrettyPrinter_Parenthesizer_term_parenthesizer___lambda__1___closed__6;
@@ -143,6 +145,7 @@ lean_object* l_Lean_PrettyPrinter_runForNodeKind___rarg(lean_object*, lean_objec
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_rawIdentNoAntiquot_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_numLitNoAntiquot_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_errorAtSavedPos_parenthesizer___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_PrettyPrinter_Parenthesizer_term_parenthesizer___lambda__1___closed__9;
@@ -240,6 +243,7 @@ static lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_level_parent
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkWsBefore_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_scientificLitNoAntiquot_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_toString(lean_object*, uint8_t);
+LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_withForbidden_parenthesizer(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_term_parenthesizer___lambda__2(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_pushNone_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -372,13 +376,14 @@ static lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_tactic_paren
 static lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___lambda__10___closed__6;
 LEAN_EXPORT lean_object* l_Lean_Syntax_MonadTraverser_goRight___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_decQuotDepth_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__4;
 static lean_object* l_Option_format___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__6___closed__2;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_withAntiquotSuffixSplice_parenthesizer___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_Traverser_down(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer(lean_object*);
 static lean_object* l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___lambda__1___closed__2;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_mkCategoryParenthesizerAttribute___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_3867_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_3888_(lean_object*);
 static lean_object* l_Lean_addTrace___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__2___closed__8;
 static lean_object* l_Option_format___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__6___closed__4;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_setExpected_parenthesizer(lean_object*);
@@ -404,6 +409,7 @@ extern lean_object* l_Lean_Core_instMonadCoreM;
 uint8_t l_Lean_Parser_isValidSyntaxNodeKind(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_Traverser_right(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_PrettyPrinter_mkParenthesizerAttribute___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__2;
 LEAN_EXPORT 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_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_visitToken___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_addPrecCheck(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -412,6 +418,7 @@ LEAN_EXPORT lean_object* l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPri
 static lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__2;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_nameLitNoAntiquot_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Syntax_MonadTraverser_goRight___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__1;
 LEAN_EXPORT lean_object* l_ReaderT_pure___at_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___spec__1(lean_object*);
 static lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___closed__3;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_withForbidden_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -478,6 +485,7 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_instCoeParenthesizer
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_parenthesizeCategoryCore___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_PrettyPrinter_mkParenthesizerAttribute___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_withAntiquotSuffixSplice_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_trailingNode_parenthesizer___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_withAntiquotSuffixSplice_parenthesizer(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkLineEq_parenthesizer___rarg(lean_object*);
@@ -501,6 +509,7 @@ static lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___cl
 lean_object* lean_nat_mod(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_withForbidden_parenthesizer___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_State_minPrec___default;
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_PrettyPrinter_mkCategoryParenthesizerAttribute___closed__3;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_strLitNoAntiquot_parenthesizer___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___lambda__9(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -518,6 +527,7 @@ lean_object* l_Nat_min(lean_object*, lean_object*);
 static lean_object* l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__6;
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_PrettyPrinter_backtrackExceptionId;
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer(lean_object*, lean_object*);
 static lean_object* l_Lean_PrettyPrinter_parenthesizeTerm___closed__1;
 static lean_object* l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__3;
 static lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__6;
@@ -7820,6 +7830,101 @@ x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
 return x_6;
 }
 }
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Parenthesizer_visitArgs___spec__2___rarg(x_1, x_2, x_3, x_4);
+return x_5;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___rarg___boxed), 4, 0);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___rarg(x_1, x_2, x_3, x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_5;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("rawStx");
+return x_1;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__10;
+x_2 = l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__3;
+x_2 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__3;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__5() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___boxed), 2, 0);
+return x_1;
+}
+}
+LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
+x_2 = l_Lean_PrettyPrinter_Parenthesizer_categoryParser_parenthesizer___closed__1;
+x_3 = l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__2;
+x_4 = l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__4;
+x_5 = l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__5;
+x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
+return x_6;
+}
+}
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_error_parenthesizer___rarg(lean_object* x_1) {
 _start:
 {
@@ -10333,7 +10438,7 @@ x_10 = l_Lean_PrettyPrinter_Parenthesizer_ite___rarg(x_9, x_2, x_3, x_4, x_5, x_
 return x_10;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_3867_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_3888_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; uint8_t x_4; 
@@ -11085,7 +11190,7 @@ x_6 = l_Lean_PrettyPrinter_parenthesize(x_5, x_1, x_2, x_3, x_4);
 return x_6;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_4149_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_4170_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
@@ -11448,6 +11553,19 @@ lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_level_paren
 res = l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__1();
+lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__1);
+l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__2 = _init_l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__2();
+lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__2);
+l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__3 = _init_l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__3();
+lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__3);
+l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__4 = _init_l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__4();
+lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__4);
+l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__5 = _init_l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__5();
+lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer___closed__5);
+res = l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_rawStx_parenthesizer(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__1 = _init_l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__1();
 lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__1);
 l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__2 = _init_l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__2();
@@ -11466,7 +11584,7 @@ l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___closed__1 = _
 lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___closed__1);
 l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___boxed__const__1 = _init_l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___boxed__const__1();
 lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_interpolatedStr_parenthesizer___boxed__const__1);
-if (builtin) {res = l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_3867_(lean_io_mk_world());
+if (builtin) {res = l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_3888_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 l_Lean_PrettyPrinter_Parenthesizer_parenthesizerAliasesRef = lean_io_result_get_value(res);
 lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_parenthesizerAliasesRef);
@@ -11491,7 +11609,7 @@ l_Lean_PrettyPrinter_parenthesizeCommand___closed__2 = _init_l_Lean_PrettyPrinte
 lean_mark_persistent(l_Lean_PrettyPrinter_parenthesizeCommand___closed__2);
 l_Lean_PrettyPrinter_parenthesizeCommand___closed__3 = _init_l_Lean_PrettyPrinter_parenthesizeCommand___closed__3();
 lean_mark_persistent(l_Lean_PrettyPrinter_parenthesizeCommand___closed__3);
-res = l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_4149_(lean_io_mk_world());
+res = l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_4170_(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));