chore: update stage0

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

@@ -122,7 +122,7 @@ where
 theorem Poly.append_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁ ++ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
   match p₁ with
   | [] => simp!
-  | v :: p₁ => sorry -- TODO(0) simp! [append_denote _ p₁ p₂, Nat.add_assoc]
+  | v :: p₁ => simp! [append_denote _ p₁ p₂, Nat.add_assoc]
 
 theorem Poly.add_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁.add p₂).denote ctx = p₁.denote ctx + p₂.denote ctx :=
   go hugeFuel p₁ p₂

stage0/src/Init/Data/String/Extra.lean

@@ -61,7 +61,7 @@ theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
 
 theorem Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬ i.atEnd = true) : sizeOf i.next < sizeOf i :=
-  have h : i.hasNext = true := by sorry -- TODO(0) simp_arith [atEnd] at h; simp_arith [hasNext, h]
+  have h : i.hasNext = true := by simp_arith [atEnd] at h; simp_arith [hasNext, h]
   sizeOf_next_lt_of_hasNext i h
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)

stage0/src/Init/Meta.lean

@@ -1081,7 +1081,7 @@ macro "declare_simp_like_tactic" opt:((simpAllKind <|> dsimpKind)?) tacName:iden
     else if opt[0].getKind == ``simpAllKind then
       pure (← `(``simpAll), ← `("simp_all "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic))
     else
-      pure (← `(``dsimp), ← `("dsimp "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
+      pure (← `(``dsimp), ← `("dsimp "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
   `($stx:command
     @[macro $tacName:ident] def expandSimp : Macro := fun s => do
       let c ← match s[1][0] with

stage0/src/Init/Notation.lean

@@ -219,6 +219,10 @@ macro_rules
 macro tk:"this" : term => return Syntax.ident tk.getHeadInfo "this".toSubstring `this []
 
 namespace Parser.Tactic
+declare_syntax_cat rawStx
+/-- `withAnnotateState 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
+
 /--
 Introduce one or more hypotheses, optionally naming and/or pattern-matching them.
 For each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.
@@ -454,7 +458,7 @@ syntax (name := simpAll) "simp_all " (config)? (discharger)? (&"only ")? ("[" (s
 The `dsimp` tactic is the definitional simplifier. It is similar to `simp` but only applies theorems that hold by
 reflexivity. Thus, the result is guaranteed to be definitionally equal to the input.
 -/
-syntax (name := dsimp) "dsimp " (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
+syntax (name := dsimp) "dsimp " (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? (location)? : tactic
 
 /--
   Delta expand the given definition.

stage0/src/Lean/Elab/Quotation.lean

@@ -131,7 +131,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
           let arr ← match k with
             | `optional => `(match $[$ids:ident],* with
                 | $[some $ids:ident],* => $(quote inner)
-                | none                 => Array.empty)
+                | $[_%$ids],*          => Array.empty)
             | _ =>
               let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id $arr)) ids.back
               `(Array.map (fun $(← mkTuple ids) => $(inner[0])) $arr)

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

@@ -37,8 +37,14 @@ namespace Tactic
 
 structure Context where
   main       : MVarId
-  -- declaration name of the executing elaborator, used by `mkTacticInfo` to persist it in the info tree
+  /-- Declaration name of the executing elaborator, used by `mkTacticInfo` to persist it in the info tree -/
   elaborator : Name
+  /--
+    If `true`, enable "error recovery" in some tactics. For example, `cases` tactic
+    admits unsolved alternatives when `recover == true`. The combinator `withoutRecover <tac>` disables
+    "error recovery" while executing `<tac>`. This is useful for tactics such as `first | ... | ...`.
+  -/
+  recover    : Bool := true
 
 structure SavedState where
   term   : Term.SavedState
@@ -221,9 +227,12 @@ def closeUsingOrAdmit (tac : TacticM Unit) : TacticM Unit := do
   try
     focusAndDone tac
   catch ex =>
-    logException ex
-    admitGoal mvarId
-    setGoals mvarIds
+    if (← read).recover then
+      logException ex
+      admitGoal mvarId
+      setGoals mvarIds
+    else
+      throw ex
 
 instance : MonadBacktrack SavedState TacticM where
   saveState := Tactic.saveState
@@ -237,8 +246,12 @@ instance : MonadExcept Exception TacticM where
   throw    := throw
   tryCatch := Tactic.tryCatch
 
+/-- Execute `x` with error recovery disabled -/
+def withoutRecover (x : TacticM α) : TacticM α :=
+  withReader (fun ctx => { ctx with recover := false }) x
+
 @[inline] protected def orElse {α} (x : TacticM α) (y : Unit → TacticM α) : TacticM α := do
-  try x catch _ => y ()
+  try withoutRecover x catch _ => y ()
 
 instance {α} : OrElse (TacticM α) where
   orElse := Tactic.orElse

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

@@ -9,6 +9,12 @@ import Lean.Elab.Tactic.ElabTerm
 
 namespace Lean.Elab.Tactic
 open Meta
+open Parser.Tactic
+
+@[builtinTactic withAnnotateState] def evalWithAnnotateState : Tactic
+  | `(tactic| with_annotate_state $stx $t) =>
+    withTacticInfoContext stx (evalTactic t)
+  | _ => throwUnsupportedSyntax
 
 @[builtinTactic Lean.Parser.Tactic.«done»] def evalDone : Tactic := fun _ =>
   done
@@ -116,8 +122,11 @@ private def getOptRotation (stx : Syntax) : Nat :=
         evalTactic stx[1]
         mvarIdsNew := mvarIdsNew ++ (← getUnsolvedGoals)
       catch ex =>
-        logException ex
-        mvarIdsNew := mvarIdsNew.push mvarId
+        if (← read).recover then
+          logException ex
+          mvarIdsNew := mvarIdsNew.push mvarId
+        else
+          throw ex
   setGoals mvarIdsNew.toList
 
 @[builtinTactic Parser.Tactic.anyGoals] def evalAnyGoals : Tactic := fun stx => do

stage0/src/Lean/Parser/Module.lean

@@ -72,32 +72,46 @@ private def consumeInput (c : ParserContext) (pos : String.Pos) : String.Pos :=
 def topLevelCommandParserFn : ParserFn :=
   commandParser.fn
 
-partial def parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext) (s : ModuleParserState) (messages : MessageLog) : Syntax × ModuleParserState × MessageLog :=
-  let rec parse (s : ModuleParserState) (messages : MessageLog) :=
-    let { pos := pos, recovering := recovering } := s
+partial def parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext) (mps : ModuleParserState) (messages : MessageLog) : Syntax × ModuleParserState × MessageLog := Id.run do
+  let mut pos := mps.pos
+  let mut recovering := mps.recovering
+  let mut messages := messages
+  let mut stx := Syntax.missing  -- will always be assigned below
+  repeat
     if inputCtx.input.atEnd pos then
-      (mkEOI pos, s, messages)
-    else
-      let c   := mkParserContext inputCtx pmctx
-      let s   := { cache := initCacheForInput c.input, pos := pos : ParserState }
-      let s   := whitespace c s
-      let s   := topLevelCommandParserFn c s
-      match s.errorMsg with
-      | none =>
-         (s.stxStack.back, { pos := s.pos }, messages)
-      | some errorMsg =>
-        -- advance at least one token to prevent infinite loops
-        let pos := if s.pos == pos then consumeInput c s.pos else s.pos
-        /- We ignore commands where `getPos?` is none. This happens only on commands that have a prefix comprised of optional elements.
-           For example, unification hints start with `optional («scoped» <|> «local»)`.
-           We claim a syntactically incorrect command containing no token or identifier is irrelevant for intellisense and should be ignored. -/
-        let ignore := s.stxStack.isEmpty || s.stxStack.back.getPos?.isNone
-        let messages := if recovering && ignore then messages else messages.add <| mkErrorMessage c s.pos (toString errorMsg)
-        if ignore then
-          parse { pos := pos, recovering := true } messages
-        else
-          (s.stxStack.back, { pos := pos, recovering := true }, messages)
-  parse s messages
+      stx := mkEOI pos
+      break
+    let pos' := pos
+    let c := mkParserContext inputCtx pmctx
+    let s := { cache := initCacheForInput c.input, pos := pos : ParserState }
+    let s := whitespace c s
+    let s := topLevelCommandParserFn c s
+    pos := s.pos
+    if recovering && !s.stxStack.isEmpty && s.stxStack.back.isAntiquot then
+      -- top-level antiquotation during recovery is most likely remnant from unfinished quotation, ignore
+      continue
+    match s.errorMsg with
+    | none =>
+      stx := s.stxStack.back
+      recovering := false
+      break
+    | some errorMsg =>
+      -- advance at least one token to prevent infinite loops
+      if pos == pos' then
+        pos := consumeInput c pos
+      /- We ignore commands where `getPos?` is none. This happens only on commands that have a prefix comprised of optional elements.
+          For example, unification hints start with `optional («scoped» <|> «local»)`.
+          We claim a syntactically incorrect command containing no token or identifier is irrelevant for intellisense and should be ignored. -/
+      let ignore := s.stxStack.isEmpty || s.stxStack.back.getPos?.isNone
+      unless recovering && ignore do
+        messages := messages.add <| mkErrorMessage c s.pos (toString errorMsg)
+      recovering := true
+      if ignore then
+        continue
+      else
+        stx := s.stxStack.back
+        break
+  return (stx, { pos, recovering }, messages)
 
 -- only useful for testing since most Lean files cannot be parsed without elaboration
 

stage0/src/Lean/Server/FileWorker/RequestHandling.lean

@@ -165,7 +165,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
   withWaitFindSnap doc (fun s => s.endPos >= hoverPos)
     (notFoundX := return none) fun snap => do
       if let rs@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text hoverPos then
-        let goals ← List.join <$> rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter } =>
+        let goals ← List.join <$> rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } =>
           let ci := if useAfter then { ci with mctx := ti.mctxAfter } else { ci with mctx := ti.mctxBefore }
           let goals := if useAfter then ti.goalsAfter else ti.goalsBefore
           ci.runMetaM {} <| goals.mapM (fun g => Meta.withPPInaccessibleNames (Widget.goalToInteractive g))

stage0/src/Lean/Server/InfoUtils.lean

@@ -25,23 +25,32 @@ def Lean.Syntax.getRange? (stx : Syntax) (originalOnly := false) : Option String
 namespace Lean.Elab
 
 /--
-  For every branch, find the deepest node in that branch matching `p`
-  with a surrounding context (the innermost one) and return all of them. -/
-partial def InfoTree.deepestNodes (p : ContextInfo → Info → Std.PersistentArray InfoTree → Option α) : InfoTree → List α :=
+  Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves). -/
+partial def InfoTree.collectNodesBottomUp (p : ContextInfo → Info → Std.PersistentArray InfoTree → List α → List α) : InfoTree → List α :=
   go none
 where go ctx?
   | context ctx t => go ctx t
   | n@(node i cs) =>
     let ccs := cs.toList.map (go <| i.updateContext? ctx?)
     let cs' := ccs.join
-    if !cs'.isEmpty then cs'
-    else match ctx? with
-      | some ctx => match p ctx i cs with
-        | some a => [a]
-        | _      => []
+    match ctx? with
+      | some ctx => p ctx i cs cs'
       | _        => []
   | _ => []
 
+/--
+  For every branch of the `InfoTree`, find the deepest node in that branch for which `p` returns
+  `some _`  and return the union of all such nodes. The visitor `p` is given a node together with
+  its innermost surrounding `ContextInfo`. -/
+partial def InfoTree.deepestNodes (p : ContextInfo → Info → Std.PersistentArray InfoTree → Option α) (infoTree : InfoTree) : List α :=
+  infoTree.collectNodesBottomUp fun ctx i cs rs =>
+    if rs.isEmpty then
+      match p ctx i cs with
+      | some r => [r]
+      | none   => []
+    else
+      rs
+
 partial def InfoTree.foldInfo (f : ContextInfo → Info → α → α) (init : α) : InfoTree → α :=
   go none init
 where go ctx? a
@@ -210,39 +219,41 @@ structure GoalsAtResult where
   ctxInfo    : ContextInfo
   tacticInfo : TacticInfo
   useAfter   : Bool
+  /-- Whether the tactic info is further indented than the hover position. -/
+  indented   : Bool
 
 /-
   Try to retrieve `TacticInfo` for `hoverPos`.
-  We retrieve the `TacticInfo` `info`, if there is a node of the form `node (ofTacticInfo info) children` s.t.
-  - `hoverPos` is sufficiently inside `info`'s range (see code), and
-  - none of the `children` satisfy the condition above. That is, for composite tactics such as
-    `induction`, we always give preference for information stored in nested (children) tactics.
+  We retrieve all `TacticInfo` nodes s.t. `hoverPos` is inside the node's range plus trailing whitespace.
+  We usually prefer the innermost such nodes so that for composite tactics such as `induction`, we show the nested proofs' states.
+  However, if `hoverPos` is after the tactic, we prefer nodes that are not indented relative to it, meaning that e.g. at `|` in
+  ```lean
+  have := by
+    exact foo
+  |
+  ```
+  we show the (final, see below) state of `have`, not `exact`.
 
   Moreover, we instruct the LSP server to use the state after tactic execution if
   - the hover position is after the info's start position *and*
   - there is no nested tactic info after the hover position (tactic combinators should decide for themselves
-    where to show intermediate states by calling `withTacticInfoContext`)
-
-  Finally, if the hover position is over the infos' trailing whitespace, we only show the last such info
-  (so that we only show the single final state after combinators such as `repeat`). -/
+    where to show intermediate states by calling `withTacticInfoContext`) -/
 partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List GoalsAtResult := Id.run do
-  let goals := t.deepestNodes fun
-    | ctx, i@(Info.ofTacticInfo ti), cs => OptionM.run do
+  t.collectNodesBottomUp fun ctx i cs gs => Id.run do
+    if let Info.ofTacticInfo ti := i then
       if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
         let trailSize := i.stx.getTrailingSize
         -- show info at EOF even if strictly outside token + trail
         let atEOF := tailPos.byteIdx + trailSize == text.source.endPos.byteIdx
-        guard <| pos ≤ hoverPos ∧ (hoverPos.byteIdx < tailPos.byteIdx + trailSize || atEOF)
-        return { ctxInfo := ctx, tacticInfo := ti, useAfter :=
-          hoverPos > pos && !cs.any (hasNestedTactic pos tailPos) }
-      else
-        failure
-    | _, _, _ => none
-  if let (last :: _ :: _) := goals.reverse then
-    -- should be the same for any element in `goals`
-    if last.tacticInfo.stx.getTailPos?.get! <= hoverPos then
-      return [last]
-  goals
+        if pos ≤ hoverPos ∧ (hoverPos.byteIdx < tailPos.byteIdx + trailSize || atEOF) then
+          -- overwrite bottom-up results according to "innermost" heuristics documented above
+          if gs.isEmpty || hoverPos ≥ tailPos && gs.all (·.indented) then
+            return [{
+              ctxInfo := ctx
+              tacticInfo := ti
+              useAfter := hoverPos > pos && !cs.any (hasNestedTactic pos tailPos)
+              indented := (text.toPosition pos).column > (text.toPosition hoverPos).column }]
+    return gs
 where
   hasNestedTactic (pos tailPos) : InfoTree → Bool
     | InfoTree.node i@(Info.ofTacticInfo _) cs => Id.run do

stage0/stdlib/Lean/Elab/Frontend.c

@@ -72,7 +72,6 @@ static lean_object* l_Lean_Elab_Frontend_runCommandElabM___rarg___closed__2;
 lean_object* l___private_Lean_Server_References_0__Lean_Server_toJsonIlean____x40_Lean_Server_References___hyg_754_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Frontend_updateCmdPos___rarg___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1(lean_object*);
-lean_object* l_Lean_Parser_parseCommand_parse(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_906____closed__2;
 LEAN_EXPORT lean_object* l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Server_findModuleRefs(lean_object*, lean_object*, uint8_t);
@@ -120,6 +119,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Frontend_getParserState___boxed(lean_object
 LEAN_EXPORT lean_object* l_Lean_Elab_process(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Frontend_updateCmdPos___rarg(lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_runFrontend___closed__2;
+lean_object* l_Lean_Parser_parseCommand(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_runFrontend___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Frontend_processCommands(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_runFrontend___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -1546,7 +1546,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Frontend_processCommand___lambda__1(lean_ob
 _start:
 {
 lean_object* x_6; 
-x_6 = l_Lean_Parser_parseCommand_parse(x_1, x_2, x_3, x_4);
+x_6 = l_Lean_Parser_parseCommand(x_1, x_2, x_3, x_4);
 return x_6;
 }
 }

stage0/stdlib/Lean/Elab/Tactic/Rewrite.c

@@ -205,6 +205,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalRewriteSeq___lambda__1___boxed(l
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRewriteSeq___closed__8;
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRewriteSeq___closed__6;
 lean_object* l_Lean_Elab_Tactic_replaceMainGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Tactic_withoutRecover___rarg(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_resolveGlobalConstCore___at_Lean_Elab_Tactic_withRWRulesSeq___spec__5___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabRewriteConfig___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Tactic_withRWRulesSeq_go___closed__2;
@@ -995,7 +996,7 @@ return x_20;
 }
 else
 {
-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_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; 
 x_21 = lean_ctor_get(x_5, 0);
 lean_inc(x_21);
 x_22 = lean_ctor_get(x_5, 1);
@@ -1003,14 +1004,15 @@ lean_inc(x_22);
 lean_dec(x_5);
 lean_inc(x_3);
 x_23 = l_Lean_mkIdentFrom(x_3, x_21);
-x_24 = l_Lean_Elab_Tactic_saveState___rarg(x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14);
-x_25 = lean_ctor_get(x_24, 0);
-lean_inc(x_25);
-x_26 = lean_ctor_get(x_24, 1);
-lean_inc(x_26);
-lean_dec(x_24);
-x_27 = lean_box(x_2);
+x_24 = lean_box(x_2);
 lean_inc(x_1);
+x_25 = lean_apply_2(x_1, x_24, x_23);
+x_26 = l_Lean_Elab_Tactic_saveState___rarg(x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14);
+x_27 = lean_ctor_get(x_26, 0);
+lean_inc(x_27);
+x_28 = lean_ctor_get(x_26, 1);
+lean_inc(x_28);
+lean_dec(x_26);
 lean_inc(x_13);
 lean_inc(x_12);
 lean_inc(x_11);
@@ -1019,10 +1021,10 @@ lean_inc(x_9);
 lean_inc(x_8);
 lean_inc(x_7);
 lean_inc(x_6);
-x_28 = lean_apply_11(x_1, x_27, x_23, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_26);
-if (lean_obj_tag(x_28) == 0)
+x_29 = l_Lean_Elab_Tactic_withoutRecover___rarg(x_25, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_28);
+if (lean_obj_tag(x_29) == 0)
 {
-lean_dec(x_25);
+lean_dec(x_27);
 lean_dec(x_22);
 lean_dec(x_13);
 lean_dec(x_12);
@@ -1035,20 +1037,20 @@ lean_dec(x_6);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_1);
-return x_28;
+return x_29;
 }
 else
 {
-lean_object* x_29; lean_object* x_30; lean_object* x_31; 
-x_29 = lean_ctor_get(x_28, 1);
-lean_inc(x_29);
-lean_dec(x_28);
-x_30 = l_Lean_Elab_Tactic_SavedState_restore(x_25, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_29);
-x_31 = lean_ctor_get(x_30, 1);
-lean_inc(x_31);
-lean_dec(x_30);
+lean_object* x_30; lean_object* x_31; lean_object* x_32; 
+x_30 = lean_ctor_get(x_29, 1);
+lean_inc(x_30);
+lean_dec(x_29);
+x_31 = l_Lean_Elab_Tactic_SavedState_restore(x_27, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_30);
+x_32 = lean_ctor_get(x_31, 1);
+lean_inc(x_32);
+lean_dec(x_31);
 x_5 = x_22;
-x_14 = x_31;
+x_14 = x_32;
 goto _start;
 }
 }

stage0/stdlib/Lean/Server/InfoUtils.c

@@ -16,7 +16,9 @@ extern "C" {
 lean_object* l_List_reverse___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__22___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__26(lean_object*);
+LEAN_EXPORT lean_object* l_List_foldr___at_Lean_Elab_InfoTree_goalsAt_x3f___spec__6___boxed(lean_object*, lean_object*);
 size_t lean_usize_add(size_t, size_t);
+LEAN_EXPORT uint8_t l_List_foldr___at_Lean_Elab_InfoTree_goalsAt_x3f___spec__6(uint8_t, lean_object*);
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_deepestNodes(lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__8___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -44,6 +46,7 @@ static lean_object* l___private_Lean_Server_InfoUtils_0__String_reprRange____x40
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__6(lean_object*);
 static lean_object* l_Lean_Elab_InfoTree_termGoalAt_x3f_getHeadFnPos_x3f___closed__3;
 static lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f_hasNestedTactic___closed__2;
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_collectNodesBottomUp_go(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Info_occursBefore_x3f___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__19(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Info_type_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -52,7 +55,6 @@ lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
 LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_InfoTree_goalsAt_x3f_hasNestedTactic___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Server_InfoUtils_0__String_reprRange____x40_Lean_Server_InfoUtils___hyg_34____closed__18;
 LEAN_EXPORT lean_object* l_Array_getMax_x3f___at_Lean_Elab_InfoTree_smallestInfo_x3f___spec__3(lean_object*);
-LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_InfoTree_deepestNodes_go___spec__1(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Info_fmtHover_x3f_isAtomicFormat___boxed(lean_object*);
 size_t lean_usize_sub(size_t, size_t);
 lean_object* l_Lean_Meta_ppExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -64,6 +66,7 @@ lean_object* l_Lean_PrettyPrinter_ppUsing(lean_object*, lean_object*, lean_objec
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f_hasNestedTactic___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_String_instInhabitedRange___closed__1;
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_collectNodesBottomUp(lean_object*);
 static lean_object* l___private_Lean_Server_InfoUtils_0__String_reprRange____x40_Lean_Server_InfoUtils___hyg_34____closed__15;
 LEAN_EXPORT lean_object* l_List_replace___at_Lean_Elab_InfoTree_termGoalAt_x3f___spec__7___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Syntax_getRange_x3f___boxed(lean_object*, lean_object*);
@@ -93,7 +96,6 @@ static lean_object* l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___clos
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__8___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
 lean_object* l_List_join___rarg(lean_object*);
 static lean_object* l___private_Lean_Server_InfoUtils_0__String_reprRange____x40_Lean_Server_InfoUtils___hyg_34____closed__10;
-LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_InfoTree_deepestNodes_go___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_InfoTree_goalsAt_x3f_hasNestedTactic___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_mkHashSet___at_Lean_Elab_InfoTree_termGoalAt_x3f___spec__8(lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__20___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
@@ -113,7 +115,6 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldI
 LEAN_EXPORT lean_object* l_Lean_Elab_Info_docString_x3f___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_PersistentArray_anyM___at_Lean_Elab_InfoTree_goalsAt_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_deepestNodes___rarg(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_deepestNodes_go___rarg(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Std_PersistentArray_anyM___at_Lean_Elab_InfoTree_goalsAt_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Lean_Elab_InfoTree_foldInfo_go___spec__15___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Info_fmtHover_x3f_fmtTerm_x3f___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -144,6 +145,8 @@ LEAN_EXPORT uint8_t l_Std_HashSetImp_contains___at_Lean_Elab_InfoTree_termGoalAt
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Info_docString_x3f___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Lean_Elab_InfoTree_foldInfo_go___spec__2(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_collectNodesBottomUp___rarg(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_InfoTree_collectNodesBottomUp_go___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f_hasNestedTactic___closed__5;
 LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_InfoTree_goalsAt_x3f___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Lean_Elab_Info_contains(lean_object*, lean_object*);
@@ -162,7 +165,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Info_docString_x3f___lambda__2___boxed(lean
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__17___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_InfoTree_getCompletionInfos___closed__1;
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__24___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_termGoalAt_x3f(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__13___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -174,6 +177,7 @@ static lean_object* l_Lean_Elab_Info_docString_x3f___lambda__2___closed__1;
 LEAN_EXPORT lean_object* l_List_elem___at_Lean_Elab_InfoTree_termGoalAt_x3f___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_Nat_repr(lean_object*);
 LEAN_EXPORT lean_object* l_Std_PersistentArray_foldlM___at_Lean_Elab_InfoTree_foldInfo_go___spec__14___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_InfoTree_collectNodesBottomUp_go___spec__1(lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__20___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_InfoTree_termGoalAt_x3f___closed__1;
 static lean_object* l_Lean_Elab_InfoTree_termGoalAt_x3f_getHeadFnPos_x3f___closed__4;
@@ -191,6 +195,7 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldI
 size_t lean_usize_modn(size_t, lean_object*);
 static lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Lean_Elab_InfoTree_foldInfo_go___spec__2___rarg___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_foldInfo_go___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f_hasNestedTactic___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Expr_isConst(lean_object*);
@@ -198,7 +203,6 @@ uint8_t l_Array_isEmpty___rarg(lean_object*);
 static lean_object* l_List_mapTRAux___at_Lean_Elab_InfoTree_smallestInfo_x3f___spec__2___closed__4;
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_smallestInfo_x3f___spec__4(lean_object*, size_t, size_t, lean_object*);
 extern lean_object* l_instInhabitedPos;
-LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_deepestNodes_go(lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_smallestInfo_x3f___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Info_stx(lean_object*);
 lean_object* l_Lean_Elab_Info_toElabInfo_x3f(lean_object*);
@@ -208,7 +212,7 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldI
 LEAN_EXPORT lean_object* l_Lean_Elab_Info_occursInside_x3f(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__17(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Info_range_x3f(lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Info_docString_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_usize_of_nat(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Info_docString_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -224,6 +228,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_foldInfo___rarg(lean_object*, lean
 LEAN_EXPORT lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Lean_Elab_InfoTree_foldInfo_go___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentArray_toList___rarg(lean_object*);
 uint8_t l_Lean_Syntax_isNodeOf(lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_deepestNodes___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_smallestInfo_x3f(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_InfoTree_smallestInfo_x3f___spec__2(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Info_size_x3f(lean_object*);
@@ -232,6 +237,7 @@ lean_object* l_Lean_Syntax_getPos_x3f(lean_object*, uint8_t);
 static lean_object* l_Lean_Elab_Info_fmtHover_x3f___lambda__1___closed__2;
 static lean_object* l___private_Lean_Server_InfoUtils_0__String_reprRange____x40_Lean_Server_InfoUtils___hyg_34____closed__1;
 static lean_object* l___private_Lean_Server_InfoUtils_0__String_reprRange____x40_Lean_Server_InfoUtils___hyg_34____closed__8;
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_deepestNodes___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_redLength___rarg(lean_object*);
 static lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f_hasNestedTactic___closed__10;
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__9(lean_object*);
@@ -245,6 +251,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Server_InfoUtils_0__String_reprRange__
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__21(lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_termGoalAt_x3f_getHeadFnPos_x3f(lean_object*, uint8_t);
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_collectNodesBottomUp_go___rarg(lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Server_InfoUtils_0__String_reprRange____x40_Lean_Server_InfoUtils___hyg_34____closed__2;
 LEAN_EXPORT lean_object* l_Lean_Elab_Info_tailPos_x3f(lean_object*);
 lean_object* l_Lean_Syntax_getArgs(lean_object*);
@@ -739,7 +746,7 @@ x_4 = l_Lean_Syntax_getRange_x3f(x_1, x_3);
 return x_4;
 }
 }
-LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_InfoTree_deepestNodes_go___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_InfoTree_collectNodesBottomUp_go___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
 if (lean_obj_tag(x_3) == 0)
@@ -761,7 +768,7 @@ x_7 = lean_ctor_get(x_3, 0);
 x_8 = lean_ctor_get(x_3, 1);
 lean_inc(x_2);
 lean_inc(x_1);
-x_9 = l_Lean_Elab_InfoTree_deepestNodes_go___rarg(x_1, x_2, x_7);
+x_9 = l_Lean_Elab_InfoTree_collectNodesBottomUp_go___rarg(x_1, x_2, x_7);
 lean_ctor_set(x_3, 1, x_4);
 lean_ctor_set(x_3, 0, x_9);
 {
@@ -782,7 +789,7 @@ lean_inc(x_11);
 lean_dec(x_3);
 lean_inc(x_2);
 lean_inc(x_1);
-x_13 = l_Lean_Elab_InfoTree_deepestNodes_go___rarg(x_1, x_2, x_11);
+x_13 = l_Lean_Elab_InfoTree_collectNodesBottomUp_go___rarg(x_1, x_2, x_11);
 x_14 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_14, 0, x_13);
 lean_ctor_set(x_14, 1, x_4);
@@ -793,15 +800,15 @@ goto _start;
 }
 }
 }
-LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_InfoTree_deepestNodes_go___spec__1(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_InfoTree_collectNodesBottomUp_go___spec__1(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_List_mapTRAux___at_Lean_Elab_InfoTree_deepestNodes_go___spec__1___rarg), 4, 0);
+x_2 = lean_alloc_closure((void*)(l_List_mapTRAux___at_Lean_Elab_InfoTree_collectNodesBottomUp_go___spec__1___rarg), 4, 0);
 return x_2;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_deepestNodes_go___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_collectNodesBottomUp_go___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 switch (lean_obj_tag(x_3)) {
@@ -822,94 +829,118 @@ goto _start;
 }
 case 1:
 {
-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_ctor_get(x_3, 0);
-lean_inc(x_8);
-x_9 = lean_ctor_get(x_3, 1);
-lean_inc(x_9);
-lean_dec(x_3);
-lean_inc(x_2);
-x_10 = l_Lean_Elab_Info_updateContext_x3f(x_2, x_8);
-lean_inc(x_9);
-x_11 = l_Std_PersistentArray_toList___rarg(x_9);
-x_12 = lean_box(0);
-lean_inc(x_1);
-x_13 = l_List_mapTRAux___at_Lean_Elab_InfoTree_deepestNodes_go___spec__1___rarg(x_1, x_10, x_11, x_12);
-x_14 = l_List_join___rarg(x_13);
-x_15 = l_List_isEmpty___rarg(x_14);
-if (x_15 == 0)
-{
-lean_dec(x_9);
-lean_dec(x_8);
-lean_dec(x_2);
-lean_dec(x_1);
-return x_14;
-}
-else
-{
-lean_dec(x_14);
 if (lean_obj_tag(x_2) == 0)
 {
-lean_object* x_16; 
-lean_dec(x_9);
-lean_dec(x_8);
+lean_object* x_8; 
+lean_dec(x_3);
 lean_dec(x_1);
-x_16 = lean_box(0);
-return x_16;
+x_8 = lean_box(0);
+return x_8;
 }
 else
 {
-lean_object* x_17; lean_object* x_18; 
-x_17 = lean_ctor_get(x_2, 0);
-lean_inc(x_17);
-lean_dec(x_2);
-x_18 = lean_apply_3(x_1, x_17, x_8, x_9);
-if (lean_obj_tag(x_18) == 0)
-{
-lean_object* x_19; 
-x_19 = lean_box(0);
-return x_19;
-}
-else
-{
-lean_object* x_20; lean_object* x_21; 
-x_20 = lean_ctor_get(x_18, 0);
-lean_inc(x_20);
-lean_dec(x_18);
-x_21 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_21, 0, x_20);
-lean_ctor_set(x_21, 1, x_12);
-return x_21;
-}
-}
+lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_9 = lean_ctor_get(x_3, 0);
+lean_inc(x_9);
+x_10 = lean_ctor_get(x_3, 1);
+lean_inc(x_10);
+lean_dec(x_3);
+x_11 = lean_ctor_get(x_2, 0);
+lean_inc(x_11);
+x_12 = l_Lean_Elab_Info_updateContext_x3f(x_2, x_9);
+lean_inc(x_10);
+x_13 = l_Std_PersistentArray_toList___rarg(x_10);
+x_14 = lean_box(0);
+lean_inc(x_1);
+x_15 = l_List_mapTRAux___at_Lean_Elab_InfoTree_collectNodesBottomUp_go___spec__1___rarg(x_1, x_12, x_13, x_14);
+x_16 = l_List_join___rarg(x_15);
+x_17 = lean_apply_4(x_1, x_11, x_9, x_10, x_16);
+return x_17;
 }
 }
 default: 
 {
-lean_object* x_22; 
+lean_object* x_18; 
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_22 = lean_box(0);
-return x_22;
+x_18 = lean_box(0);
+return x_18;
 }
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_deepestNodes_go(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_collectNodesBottomUp_go(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Lean_Elab_InfoTree_deepestNodes_go___rarg), 3, 0);
+x_2 = lean_alloc_closure((void*)(l_Lean_Elab_InfoTree_collectNodesBottomUp_go___rarg), 3, 0);
 return x_2;
 }
 }
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_collectNodesBottomUp___rarg(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; 
+x_3 = lean_box(0);
+x_4 = l_Lean_Elab_InfoTree_collectNodesBottomUp_go___rarg(x_1, x_3, x_2);
+return x_4;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_collectNodesBottomUp(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Elab_InfoTree_collectNodesBottomUp___rarg), 2, 0);
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_deepestNodes___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+uint8_t x_6; 
+x_6 = l_List_isEmpty___rarg(x_5);
+if (x_6 == 0)
+{
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+lean_inc(x_5);
+return x_5;
+}
+else
+{
+lean_object* x_7; 
+x_7 = lean_apply_3(x_1, x_2, x_3, x_4);
+if (lean_obj_tag(x_7) == 0)
+{
+lean_object* x_8; 
+x_8 = lean_box(0);
+return x_8;
+}
+else
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_9 = lean_ctor_get(x_7, 0);
+lean_inc(x_9);
+lean_dec(x_7);
+x_10 = lean_box(0);
+x_11 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_11, 0, x_9);
+lean_ctor_set(x_11, 1, x_10);
+return x_11;
+}
+}
+}
+}
 LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_deepestNodes___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; lean_object* x_4; 
-x_3 = lean_box(0);
-x_4 = l_Lean_Elab_InfoTree_deepestNodes_go___rarg(x_1, x_3, x_2);
+x_3 = lean_alloc_closure((void*)(l_Lean_Elab_InfoTree_deepestNodes___rarg___lambda__1___boxed), 5, 1);
+lean_closure_set(x_3, 0, x_1);
+x_4 = l_Lean_Elab_InfoTree_collectNodesBottomUp___rarg(x_3, x_2);
 return x_4;
 }
 }
@@ -921,6 +952,15 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_InfoTree_deepestNodes___rarg), 2, 0
 return x_2;
 }
 }
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_deepestNodes___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+lean_object* x_6; 
+x_6 = l_Lean_Elab_InfoTree_deepestNodes___rarg___lambda__1(x_1, x_2, x_3, x_4, x_5);
+lean_dec(x_5);
+return x_6;
+}
+}
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_InfoTree_foldInfo_go___spec__4___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, size_t x_4, size_t x_5, lean_object* x_6) {
 _start:
 {
@@ -6917,171 +6957,242 @@ return x_6;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+LEAN_EXPORT uint8_t l_List_foldr___at_Lean_Elab_InfoTree_goalsAt_x3f___spec__6(uint8_t x_1, lean_object* x_2) {
+_start:
+{
+if (lean_obj_tag(x_2) == 0)
+{
+return x_1;
+}
+else
+{
+lean_object* x_3; uint8_t x_4; 
+x_3 = lean_ctor_get(x_2, 0);
+x_4 = lean_ctor_get_uint8(x_3, sizeof(void*)*2 + 1);
+if (x_4 == 0)
+{
+uint8_t x_5; 
+x_5 = 0;
+return x_5;
+}
+else
+{
+lean_object* x_6; 
+x_6 = lean_ctor_get(x_2, 1);
+x_2 = x_6;
+goto _start;
+}
+}
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
 if (lean_obj_tag(x_4) == 0)
 {
-lean_object* x_6; lean_object* x_7; 
-x_6 = lean_ctor_get(x_4, 0);
-x_7 = l_Lean_Elab_Info_pos_x3f(x_4);
-if (lean_obj_tag(x_7) == 0)
+lean_object* x_7; lean_object* x_8; 
+x_7 = lean_ctor_get(x_4, 0);
+x_8 = l_Lean_Elab_Info_pos_x3f(x_4);
+if (lean_obj_tag(x_8) == 0)
 {
-lean_object* x_8; 
 lean_dec(x_5);
 lean_dec(x_3);
-x_8 = lean_box(0);
-return x_8;
+lean_inc(x_6);
+return x_6;
 }
 else
 {
 lean_object* x_9; lean_object* x_10; 
-x_9 = lean_ctor_get(x_7, 0);
+x_9 = lean_ctor_get(x_8, 0);
 lean_inc(x_9);
-lean_dec(x_7);
+lean_dec(x_8);
 x_10 = l_Lean_Elab_Info_tailPos_x3f(x_4);
 if (lean_obj_tag(x_10) == 0)
 {
-lean_object* x_11; 
 lean_dec(x_9);
 lean_dec(x_5);
 lean_dec(x_3);
-x_11 = lean_box(0);
-return x_11;
+lean_inc(x_6);
+return x_6;
 }
 else
 {
-lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; uint8_t x_32; uint8_t x_33; 
-x_12 = lean_ctor_get(x_10, 0);
-lean_inc(x_12);
-if (lean_is_exclusive(x_10)) {
- lean_ctor_release(x_10, 0);
- x_13 = x_10;
-} else {
- lean_dec_ref(x_10);
- x_13 = lean_box(0);
-}
-x_27 = l_Lean_Elab_Info_stx(x_4);
-x_28 = l_Lean_Syntax_getTrailingSize(x_27);
-lean_dec(x_27);
-x_29 = lean_nat_add(x_12, x_28);
-lean_dec(x_28);
-x_30 = lean_ctor_get(x_2, 0);
-x_31 = lean_string_utf8_byte_size(x_30);
-x_32 = lean_nat_dec_eq(x_29, x_31);
-lean_dec(x_31);
-x_33 = lean_nat_dec_le(x_9, x_1);
-if (x_33 == 0)
+lean_object* x_11; lean_object* x_12; lean_object* x_31; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; uint8_t x_44; uint8_t x_45; 
+x_11 = lean_ctor_get(x_10, 0);
+lean_inc(x_11);
+lean_dec(x_10);
+x_39 = l_Lean_Elab_Info_stx(x_4);
+x_40 = l_Lean_Syntax_getTrailingSize(x_39);
+lean_dec(x_39);
+x_41 = lean_nat_add(x_11, x_40);
+lean_dec(x_40);
+x_42 = lean_ctor_get(x_2, 0);
+x_43 = lean_string_utf8_byte_size(x_42);
+x_44 = lean_nat_dec_eq(x_41, x_43);
+lean_dec(x_43);
+x_45 = lean_nat_dec_le(x_9, x_1);
+if (x_45 == 0)
 {
-lean_object* x_34; 
-lean_dec(x_29);
-lean_dec(x_13);
+lean_dec(x_41);
+lean_dec(x_11);
+lean_dec(x_9);
+lean_dec(x_5);
+lean_dec(x_3);
+lean_inc(x_6);
+return x_6;
+}
+else
+{
+uint8_t x_46; 
+x_46 = lean_nat_dec_lt(x_1, x_41);
+lean_dec(x_41);
+if (x_46 == 0)
+{
+if (x_44 == 0)
+{
+lean_dec(x_11);
+lean_dec(x_9);
+lean_dec(x_5);
+lean_dec(x_3);
+lean_inc(x_6);
+return x_6;
+}
+else
+{
+lean_object* x_47; 
+x_47 = lean_box(0);
+x_31 = x_47;
+goto block_38;
+}
+}
+else
+{
+lean_object* x_48; 
+x_48 = lean_box(0);
+x_31 = x_48;
+goto block_38;
+}
+}
+block_30:
+{
+uint8_t x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19; 
 lean_dec(x_12);
+x_13 = lean_nat_dec_lt(x_9, x_1);
+x_14 = l_Lean_FileMap_toPosition(x_2, x_1);
+x_15 = lean_ctor_get(x_14, 1);
+lean_inc(x_15);
+lean_dec(x_14);
+x_16 = l_Lean_FileMap_toPosition(x_2, x_9);
+x_17 = lean_ctor_get(x_16, 1);
+lean_inc(x_17);
+lean_dec(x_16);
+x_18 = lean_nat_dec_lt(x_15, x_17);
+lean_dec(x_17);
+lean_dec(x_15);
+x_19 = lean_box(0);
+if (x_13 == 0)
+{
+uint8_t x_20; lean_object* x_21; lean_object* x_22; 
+lean_dec(x_11);
 lean_dec(x_9);
 lean_dec(x_5);
-lean_dec(x_3);
-x_34 = lean_box(0);
-return x_34;
+x_20 = 0;
+lean_inc(x_7);
+x_21 = lean_alloc_ctor(0, 2, 2);
+lean_ctor_set(x_21, 0, x_3);
+lean_ctor_set(x_21, 1, x_7);
+lean_ctor_set_uint8(x_21, sizeof(void*)*2, x_20);
+lean_ctor_set_uint8(x_21, sizeof(void*)*2 + 1, x_18);
+x_22 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_22, 0, x_21);
+lean_ctor_set(x_22, 1, x_19);
+return x_22;
 }
 else
 {
-uint8_t x_35; 
-x_35 = lean_nat_dec_lt(x_1, x_29);
-lean_dec(x_29);
-if (x_35 == 0)
+uint8_t x_23; 
+x_23 = l_Std_PersistentArray_anyM___at_Lean_Elab_InfoTree_goalsAt_x3f___spec__1(x_1, x_9, x_11, x_5);
+lean_dec(x_11);
+lean_dec(x_9);
+if (x_23 == 0)
 {
+uint8_t x_24; lean_object* x_25; lean_object* x_26; 
+x_24 = 1;
+lean_inc(x_7);
+x_25 = lean_alloc_ctor(0, 2, 2);
+lean_ctor_set(x_25, 0, x_3);
+lean_ctor_set(x_25, 1, x_7);
+lean_ctor_set_uint8(x_25, sizeof(void*)*2, x_24);
+lean_ctor_set_uint8(x_25, sizeof(void*)*2 + 1, x_18);
+x_26 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_26, 0, x_25);
+lean_ctor_set(x_26, 1, x_19);
+return x_26;
+}
+else
+{
+uint8_t x_27; lean_object* x_28; lean_object* x_29; 
+x_27 = 0;
+lean_inc(x_7);
+x_28 = lean_alloc_ctor(0, 2, 2);
+lean_ctor_set(x_28, 0, x_3);
+lean_ctor_set(x_28, 1, x_7);
+lean_ctor_set_uint8(x_28, sizeof(void*)*2, x_27);
+lean_ctor_set_uint8(x_28, sizeof(void*)*2 + 1, x_18);
+x_29 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_29, 0, x_28);
+lean_ctor_set(x_29, 1, x_19);
+return x_29;
+}
+}
+}
+block_38:
+{
+uint8_t x_32; 
+lean_dec(x_31);
+x_32 = l_List_isEmpty___rarg(x_6);
 if (x_32 == 0)
 {
-lean_object* x_36; 
-lean_dec(x_13);
-lean_dec(x_12);
+uint8_t x_33; 
+x_33 = lean_nat_dec_le(x_11, x_1);
+if (x_33 == 0)
+{
+lean_dec(x_11);
 lean_dec(x_9);
 lean_dec(x_5);
 lean_dec(x_3);
+lean_inc(x_6);
+return x_6;
+}
+else
+{
+uint8_t x_34; uint8_t x_35; 
+x_34 = 1;
+x_35 = l_List_foldr___at_Lean_Elab_InfoTree_goalsAt_x3f___spec__6(x_34, x_6);
+if (x_35 == 0)
+{
+lean_dec(x_11);
+lean_dec(x_9);
+lean_dec(x_5);
+lean_dec(x_3);
+lean_inc(x_6);
+return x_6;
+}
+else
+{
+lean_object* x_36; 
 x_36 = lean_box(0);
-return x_36;
+x_12 = x_36;
+goto block_30;
+}
+}
 }
 else
 {
 lean_object* x_37; 
 x_37 = lean_box(0);
-x_14 = x_37;
-goto block_26;
-}
-}
-else
-{
-lean_object* x_38; 
-x_38 = lean_box(0);
-x_14 = x_38;
-goto block_26;
-}
-}
-block_26:
-{
-uint8_t x_15; 
-lean_dec(x_14);
-x_15 = lean_nat_dec_lt(x_9, x_1);
-if (x_15 == 0)
-{
-uint8_t x_16; lean_object* x_17; lean_object* x_18; 
-lean_dec(x_12);
-lean_dec(x_9);
-lean_dec(x_5);
-x_16 = 0;
-lean_inc(x_6);
-x_17 = lean_alloc_ctor(0, 2, 1);
-lean_ctor_set(x_17, 0, x_3);
-lean_ctor_set(x_17, 1, x_6);
-lean_ctor_set_uint8(x_17, sizeof(void*)*2, x_16);
-if (lean_is_scalar(x_13)) {
- x_18 = lean_alloc_ctor(1, 1, 0);
-} else {
- x_18 = x_13;
-}
-lean_ctor_set(x_18, 0, x_17);
-return x_18;
-}
-else
-{
-uint8_t x_19; 
-x_19 = l_Std_PersistentArray_anyM___at_Lean_Elab_InfoTree_goalsAt_x3f___spec__1(x_1, x_9, x_12, x_5);
-lean_dec(x_12);
-lean_dec(x_9);
-if (x_19 == 0)
-{
-uint8_t x_20; lean_object* x_21; lean_object* x_22; 
-x_20 = 1;
-lean_inc(x_6);
-x_21 = lean_alloc_ctor(0, 2, 1);
-lean_ctor_set(x_21, 0, x_3);
-lean_ctor_set(x_21, 1, x_6);
-lean_ctor_set_uint8(x_21, sizeof(void*)*2, x_20);
-if (lean_is_scalar(x_13)) {
- x_22 = lean_alloc_ctor(1, 1, 0);
-} else {
- x_22 = x_13;
-}
-lean_ctor_set(x_22, 0, x_21);
-return x_22;
-}
-else
-{
-uint8_t x_23; lean_object* x_24; lean_object* x_25; 
-x_23 = 0;
-lean_inc(x_6);
-x_24 = lean_alloc_ctor(0, 2, 1);
-lean_ctor_set(x_24, 0, x_3);
-lean_ctor_set(x_24, 1, x_6);
-lean_ctor_set_uint8(x_24, sizeof(void*)*2, x_23);
-if (lean_is_scalar(x_13)) {
- x_25 = lean_alloc_ctor(1, 1, 0);
-} else {
- x_25 = x_13;
-}
-lean_ctor_set(x_25, 0, x_24);
-return x_25;
-}
+x_12 = x_37;
+goto block_30;
 }
 }
 }
@@ -7089,185 +7200,23 @@ return x_25;
 }
 else
 {
-lean_object* x_39; 
 lean_dec(x_5);
 lean_dec(x_3);
-x_39 = lean_box(0);
-return x_39;
+lean_inc(x_6);
+return x_6;
 }
 }
 }
 LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-lean_inc(x_3);
-x_4 = lean_alloc_closure((void*)(l_Lean_Elab_InfoTree_goalsAt_x3f___lambda__1___boxed), 5, 2);
+lean_object* x_4; lean_object* x_5; 
+x_4 = lean_alloc_closure((void*)(l_Lean_Elab_InfoTree_goalsAt_x3f___lambda__1___boxed), 6, 2);
 lean_closure_set(x_4, 0, x_3);
 lean_closure_set(x_4, 1, x_1);
-x_5 = l_Lean_Elab_InfoTree_deepestNodes___rarg(x_4, x_2);
-lean_inc(x_5);
-x_6 = l_List_reverse___rarg(x_5);
-if (lean_obj_tag(x_6) == 0)
-{
-lean_dec(x_3);
+x_5 = l_Lean_Elab_InfoTree_collectNodesBottomUp___rarg(x_4, x_2);
 return x_5;
 }
-else
-{
-lean_object* x_7; 
-x_7 = lean_ctor_get(x_6, 1);
-lean_inc(x_7);
-if (lean_obj_tag(x_7) == 0)
-{
-lean_dec(x_6);
-lean_dec(x_3);
-return x_5;
-}
-else
-{
-uint8_t x_8; 
-x_8 = !lean_is_exclusive(x_7);
-if (x_8 == 0)
-{
-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; lean_object* x_16; 
-x_9 = lean_ctor_get(x_7, 1);
-lean_dec(x_9);
-x_10 = lean_ctor_get(x_7, 0);
-lean_dec(x_10);
-x_11 = lean_ctor_get(x_6, 0);
-lean_inc(x_11);
-lean_dec(x_6);
-x_12 = lean_ctor_get(x_11, 1);
-lean_inc(x_12);
-x_13 = lean_ctor_get(x_12, 0);
-lean_inc(x_13);
-lean_dec(x_12);
-x_14 = lean_ctor_get(x_13, 1);
-lean_inc(x_14);
-lean_dec(x_13);
-x_15 = 0;
-x_16 = l_Lean_Syntax_getTailPos_x3f(x_14, x_15);
-if (lean_obj_tag(x_16) == 0)
-{
-lean_object* x_17; lean_object* x_18; uint8_t x_19; 
-x_17 = l_List_mapTRAux___at_Lean_Elab_InfoTree_smallestInfo_x3f___spec__2___closed__4;
-x_18 = l_panic___at_Lean_Elab_InfoTree_smallestInfo_x3f___spec__1(x_17);
-x_19 = lean_nat_dec_le(x_18, x_3);
-lean_dec(x_3);
-lean_dec(x_18);
-if (x_19 == 0)
-{
-lean_dec(x_11);
-lean_free_object(x_7);
-return x_5;
-}
-else
-{
-lean_object* x_20; 
-lean_dec(x_5);
-x_20 = lean_box(0);
-lean_ctor_set(x_7, 1, x_20);
-lean_ctor_set(x_7, 0, x_11);
-return x_7;
-}
-}
-else
-{
-lean_object* x_21; uint8_t x_22; 
-x_21 = lean_ctor_get(x_16, 0);
-lean_inc(x_21);
-lean_dec(x_16);
-x_22 = lean_nat_dec_le(x_21, x_3);
-lean_dec(x_3);
-lean_dec(x_21);
-if (x_22 == 0)
-{
-lean_dec(x_11);
-lean_free_object(x_7);
-return x_5;
-}
-else
-{
-lean_object* x_23; 
-lean_dec(x_5);
-x_23 = lean_box(0);
-lean_ctor_set(x_7, 1, x_23);
-lean_ctor_set(x_7, 0, x_11);
-return x_7;
-}
-}
-}
-else
-{
-lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28; lean_object* x_29; 
-lean_dec(x_7);
-x_24 = lean_ctor_get(x_6, 0);
-lean_inc(x_24);
-lean_dec(x_6);
-x_25 = lean_ctor_get(x_24, 1);
-lean_inc(x_25);
-x_26 = lean_ctor_get(x_25, 0);
-lean_inc(x_26);
-lean_dec(x_25);
-x_27 = lean_ctor_get(x_26, 1);
-lean_inc(x_27);
-lean_dec(x_26);
-x_28 = 0;
-x_29 = l_Lean_Syntax_getTailPos_x3f(x_27, x_28);
-if (lean_obj_tag(x_29) == 0)
-{
-lean_object* x_30; lean_object* x_31; uint8_t x_32; 
-x_30 = l_List_mapTRAux___at_Lean_Elab_InfoTree_smallestInfo_x3f___spec__2___closed__4;
-x_31 = l_panic___at_Lean_Elab_InfoTree_smallestInfo_x3f___spec__1(x_30);
-x_32 = lean_nat_dec_le(x_31, x_3);
-lean_dec(x_3);
-lean_dec(x_31);
-if (x_32 == 0)
-{
-lean_dec(x_24);
-return x_5;
-}
-else
-{
-lean_object* x_33; lean_object* x_34; 
-lean_dec(x_5);
-x_33 = lean_box(0);
-x_34 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_34, 0, x_24);
-lean_ctor_set(x_34, 1, x_33);
-return x_34;
-}
-}
-else
-{
-lean_object* x_35; uint8_t x_36; 
-x_35 = lean_ctor_get(x_29, 0);
-lean_inc(x_35);
-lean_dec(x_29);
-x_36 = lean_nat_dec_le(x_35, x_3);
-lean_dec(x_3);
-lean_dec(x_35);
-if (x_36 == 0)
-{
-lean_dec(x_24);
-return x_5;
-}
-else
-{
-lean_object* x_37; lean_object* x_38; 
-lean_dec(x_5);
-x_37 = lean_box(0);
-x_38 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_38, 0, x_24);
-lean_ctor_set(x_38, 1, x_37);
-return x_38;
-}
-}
-}
-}
-}
-}
 }
 LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_InfoTree_goalsAt_x3f___spec__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) {
 _start:
@@ -7344,15 +7293,28 @@ x_6 = lean_box(x_5);
 return x_6;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+LEAN_EXPORT lean_object* l_List_foldr___at_Lean_Elab_InfoTree_goalsAt_x3f___spec__6___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_6; 
-x_6 = l_Lean_Elab_InfoTree_goalsAt_x3f___lambda__1(x_1, x_2, x_3, x_4, x_5);
+uint8_t x_3; uint8_t x_4; lean_object* x_5; 
+x_3 = lean_unbox(x_1);
+lean_dec(x_1);
+x_4 = l_List_foldr___at_Lean_Elab_InfoTree_goalsAt_x3f___spec__6(x_3, x_2);
+lean_dec(x_2);
+x_5 = lean_box(x_4);
+return x_5;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_goalsAt_x3f___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; 
+x_7 = l_Lean_Elab_InfoTree_goalsAt_x3f___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_6);
 lean_dec(x_4);
 lean_dec(x_2);
 lean_dec(x_1);
-return x_6;
+return x_7;
 }
 }
 static lean_object* _init_l_Lean_Elab_InfoTree_termGoalAt_x3f_getHeadFnPos_x3f___closed__1() {

stage0/stdlib/Lean/Server/Snapshots.c

@@ -96,7 +96,6 @@ LEAN_EXPORT lean_object* l_Lean_Server_Snapshots_parseNextCmd(lean_object*, lean
 LEAN_EXPORT lean_object* l_Lean_Server_Snapshots_Snapshot_isAtEnd___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_Snapshots_compileNextCmd___lambda__3(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getPos_x3f(lean_object*, uint8_t);
-lean_object* l_Lean_Parser_parseCommand_parse(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_instInhabitedInfoTree;
 uint8_t l_String_isEmpty(lean_object*);
@@ -144,6 +143,7 @@ static lean_object* l_Lean_Server_Snapshots_initFn____x40_Lean_Server_Snapshots_
 LEAN_EXPORT lean_object* l_Lean_Server_Snapshots_dummyTacticCache;
 LEAN_EXPORT lean_object* l_Lean_Server_Snapshots_compileNextCmd___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_get_set_stdin(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_parseCommand(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Server_Snapshots_compileNextCmd(lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l_panic___at_Lean_Elab_InfoTree_smallestInfo_x3f___spec__1(lean_object*);
 static lean_object* l_Lean_Server_Snapshots_initFn____x40_Lean_Server_Snapshots___hyg_6____closed__4;
@@ -1027,7 +1027,7 @@ x_13 = lean_ctor_get(x_2, 2);
 lean_inc(x_13);
 x_14 = l_Lean_Server_Snapshots_Snapshot_msgLog(x_2);
 lean_dec(x_2);
-x_15 = l_Lean_Parser_parseCommand_parse(x_1, x_12, x_13, x_14);
+x_15 = l_Lean_Parser_parseCommand(x_1, x_12, x_13, x_14);
 x_16 = lean_ctor_get(x_15, 0);
 lean_inc(x_16);
 lean_dec(x_15);
@@ -1044,7 +1044,7 @@ lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_ob
 x_7 = l_Lean_Server_Snapshots_Snapshot_msgLog(x_1);
 lean_inc(x_3);
 lean_inc(x_2);
-x_8 = l_Lean_Parser_parseCommand_parse(x_2, x_3, x_4, x_7);
+x_8 = l_Lean_Parser_parseCommand(x_2, x_3, x_4, x_7);
 x_9 = lean_ctor_get(x_8, 1);
 lean_inc(x_9);
 x_10 = lean_ctor_get(x_8, 0);
@@ -1944,7 +1944,7 @@ lean_ctor_set(x_21, 2, x_19);
 lean_ctor_set(x_21, 3, x_20);
 x_22 = l_Lean_Server_Snapshots_Snapshot_msgLog(x_2);
 lean_inc(x_1);
-x_23 = l_Lean_Parser_parseCommand_parse(x_1, x_21, x_6, x_22);
+x_23 = l_Lean_Parser_parseCommand(x_1, x_21, x_6, x_22);
 x_24 = lean_ctor_get(x_23, 1);
 lean_inc(x_24);
 x_25 = lean_ctor_get(x_23, 0);