diff --git a/src/Init.lean b/src/Init.lean
index 2f99ab920c..54792ce061 100644
--- a/src/Init.lean
+++ b/src/Init.lean
@@ -40,3 +40,4 @@ import Init.Syntax
 import Init.Internal
 import Init.Try
 import Init.BinderNameHint
+import Init.Task
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 6a70d09000..2e565ee7ac 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -137,9 +137,14 @@ def mapTasks (f : List α → BaseIO β) (tasks : List (Task α)) (prio := Task.
   go tasks []
 where
   go
+    | [], as =>
+      if sync then
+        return .pure (← f as.reverse)
+      else
+        f as.reverse |>.asTask prio
+    | [t], as => BaseIO.mapTask (fun a => f (a :: as).reverse) t prio sync
     | t::ts, as =>
       BaseIO.bindTask t (fun a => go ts (a :: as)) prio sync
-    | [], as => f as.reverse |>.asTask prio
 
 end BaseIO
 
diff --git a/src/Init/Task.lean b/src/Init/Task.lean
new file mode 100644
index 0000000000..47f5cc40e0
--- /dev/null
+++ b/src/Init/Task.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2025 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+
+Additional `Task` definitions.
+-/
+prelude
+import Init.Core
+import Init.Data.List.Basic
+
+namespace Task
+
+/--
+Creates a task that, when all `tasks` have finished, computes the result of `f` applied to their
+results.
+-/
+def mapList (f : List α → β) (tasks : List (Task α)) (prio := Task.Priority.default)
+    (sync := false) : Task β :=
+  go tasks []
+where
+  go
+    | [], as =>
+      if sync then
+        .pure <| f as.reverse
+      else
+        Task.spawn (prio := prio) fun _ => f as.reverse
+    | [t], as => t.map (fun a => f (a :: as).reverse) prio sync
+    | t::ts, as => t.bind (fun a => go ts (a :: as)) prio sync
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 56069eaa38..d61abf1124 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -462,11 +462,12 @@ def wrapAsyncAsSnapshot (act : Unit → CoreM Unit) (cancelTk? : Option IO.Cance
   let t ← wrapAsync (cancelTk? := cancelTk?) fun _ => do
     IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get (← getOptions)) do
       let tid ← IO.getTID
-      -- reset trace state and message log so as not to report them twice
+      -- reset trace/info state and message log so as not to report them twice
       modify fun st => { st with
         messages := st.messages.markAllReported
         traceState := { tid }
         snapshotTasks := #[]
+        infoState := {}
       }
       try
         withTraceNode `Elab.async (fun _ => return desc) do
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index aeb0b820e3..e83c3f4d1e 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -226,13 +226,16 @@ private def runCore (x : CoreM α) : CommandElabM α := do
   }
   let (ea, coreS) ← liftM x
   modify fun s => { s with
-    env               := coreS.env
-    nextMacroScope    := coreS.nextMacroScope
-    ngen              := coreS.ngen
-    infoState.trees   := s.infoState.trees.append coreS.infoState.trees
-    traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
-    snapshotTasks     := coreS.snapshotTasks
-    messages          := s.messages ++ coreS.messages
+    env                      := coreS.env
+    nextMacroScope           := coreS.nextMacroScope
+    ngen                     := coreS.ngen
+    infoState.trees          := s.infoState.trees.append coreS.infoState.trees
+    -- we assume substitution of `assingment` has already happened, but for lazy assignments we only
+    -- do it at the very end
+    infoState.lazyAssignment := coreS.infoState.lazyAssignment
+    traceState.traces        := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
+    snapshotTasks            := coreS.snapshotTasks
+    messages                 := s.messages ++ coreS.messages
   }
   return ea
 
@@ -299,20 +302,20 @@ Interrupt and abort exceptions are caught but not logged.
   EIO.catchExceptions (withLogging x ctx ref) (fun _ => pure ())
 
 @[inherit_doc Core.wrapAsync]
-def wrapAsync (act : Unit → CommandElabM α) (cancelTk? : Option IO.CancelToken) :
-    CommandElabM (EIO Exception α) := do
+def wrapAsync {α β : Type} (act : α → CommandElabM β) (cancelTk? : Option IO.CancelToken) :
+    CommandElabM (α → EIO Exception β) := do
   let ctx ← read
   let ctx := { ctx with cancelTk? }
   let st ← get
-  return act () |>.run ctx |>.run' st
+  return (act · |>.run ctx |>.run' st)
 
 open Language in
 @[inherit_doc Core.wrapAsyncAsSnapshot]
 -- `CoreM` and `CommandElabM` are too different to meaningfully share this code
-def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit) (cancelTk? : Option IO.CancelToken)
+def wrapAsyncAsSnapshot {α : Type} (act : α → CommandElabM Unit) (cancelTk? : Option IO.CancelToken)
     (desc : String := by exact decl_name%.toString) :
-    CommandElabM (BaseIO SnapshotTree) := do
-  let t ← wrapAsync (cancelTk? := cancelTk?) fun _ => do
+    CommandElabM (α → BaseIO SnapshotTree) := do
+  let f ← wrapAsync (cancelTk? := cancelTk?) fun a => do
     IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get (← getOptions)) do
       let tid ← IO.getTID
       -- reset trace state and message log so as not to report them twice
@@ -323,15 +326,15 @@ def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit) (cancelTk? : Option I
       }
       try
         withTraceNode `Elab.async (fun _ => return desc) do
-          act ()
+          act a
       catch e =>
         logError e.toMessageData
       finally
         addTraceAsMessages
       get
   let ctx ← read
-  return do
-    match (← t.toBaseIO) with
+  return fun a => do
+    match (← (f a).toBaseIO) with
     | .ok (output, st) =>
       let mut msgs := st.messages
       if !output.isEmpty then
@@ -353,6 +356,7 @@ def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit) (cancelTk? : Option I
 def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CommandElabM Unit :=
   modify fun s => { s with snapshotTasks := s.snapshotTasks.push task }
 
+open Language in
 def runLintersAsync (stx : Syntax) : CommandElabM Unit := do
   if !Elab.async.get (← getOptions) then
     withoutModifyingEnv do
@@ -362,8 +366,13 @@ def runLintersAsync (stx : Syntax) : CommandElabM Unit := do
   -- We only start one task for all linters for now as most linters are fast and we simply want
   -- to unblock elaboration of the next command
   let cancelTk ← IO.CancelToken.new
-  let lintAct ← wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun _ => runLinters stx
-  logSnapshotTask { stx? := none, task := (← BaseIO.asTask lintAct), cancelTk? := cancelTk }
+  let lintAct ← wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun infoSt => do
+    modifyInfoState fun _ => infoSt
+    runLinters stx
+
+  -- linters should have access to the complete info tree
+  let task ← BaseIO.mapTask (t := (← getInfoState).substituteLazy) lintAct
+  logSnapshotTask { stx? := none, task, cancelTk? := cancelTk }
 
 protected def getCurrMacroScope : CommandElabM Nat  := do pure (← read).currMacroScope
 protected def getMainModule     : CommandElabM Name := do pure (← getEnv).mainModule
@@ -579,11 +588,7 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
     if let some snap := (← read).snap? then
       snap.new.resolve default
 
-    -- note the order: first process current messages & info trees, then add back old messages & trees,
-    -- then convert new traces to messages
-    let mut msgs := (← get).messages
-    for tree in (← getInfoTrees) do
-      trace[Elab.info] (← tree.format)
+    let msgs := (← get).messages
     modify fun st => { st with
       messages := initMsgs ++ msgs
       infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees }
diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
index 99b177799a..6e6d5ff85c 100644
--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -112,9 +112,9 @@ where
         |>.foldl (· ++ ·) {}
       -- In contrast to messages, we should collect info trees only from the top-level command
       -- snapshots as they subsume any info trees reported incrementally by their children.
-      let trees := commands.map (·.finishedSnap.get.infoTree?) |>.filterMap id |>.toPArray'
+      let trees := commands.map (·.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray'
       return {
-        commandState := { snap.finishedSnap.get.cmdState with messages, infoState.trees := trees }
+        commandState := { snap.resultSnap.get.cmdState with messages, infoState.trees := trees }
         parserState := snap.parserState
         cmdPos := snap.parserState.pos
         commands := commands.map (·.stx)
diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean
index 2069c7138a..04af8563cc 100644
--- a/src/Lean/Elab/InfoTree/Main.lean
+++ b/src/Lean/Elab/InfoTree/Main.lean
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
+import Init.Task
 import Lean.Meta.PPGoal
 import Lean.ReservedNameAction
 
@@ -95,6 +96,13 @@ partial def InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMa
     | none      => hole id
     | some tree => substitute tree assignment
 
+/-- Applies `s.lazyAssignment` to `s.trees`, asynchronously. -/
+def InfoState.substituteLazy (s : InfoState) : Task InfoState :=
+  Task.mapList (tasks := s.lazyAssignment.toList.map (·.2)) fun _ => { s with
+    trees := s.trees.map (·.substitute <| s.lazyAssignment.map (·.get))
+    lazyAssignment := {}
+  }
+
 /-- Embeds a `CoreM` action in `IO` by supplying the information stored in `info`. -/
 def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
   /-
diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean
index dd22148866..8f54b3dc78 100644
--- a/src/Lean/Elab/InfoTree/Types.lean
+++ b/src/Lean/Elab/InfoTree/Types.lean
@@ -255,6 +255,11 @@ structure InfoState where
   enabled    : Bool := true
   /-- Map from holes in the infotree to child infotrees. -/
   assignment : PersistentHashMap MVarId InfoTree := {}
+  /--
+  Assignments fulfilled by other elaboration tasks. We substitute them only just before reporting
+  the info tree via a snapshot to avoid premature blocking.
+  -/
+  lazyAssignment : PersistentHashMap MVarId (Task InfoTree) := {}
   /-- Pending child trees of a node. -/
   trees      : PersistentArray InfoTree := {}
   deriving Inhabited
diff --git a/src/Lean/Elab/InfoTrees.lean b/src/Lean/Elab/InfoTrees.lean
index 82c5128581..dfcfeaed9a 100644
--- a/src/Lean/Elab/InfoTrees.lean
+++ b/src/Lean/Elab/InfoTrees.lean
@@ -17,7 +17,7 @@ def elabInfoTrees : CommandElab
       logError "Info trees are disabled, can not use `#info_trees`."
     else
       elabCommand cmd
-      let infoTrees ← getInfoTrees
+      let infoTrees := (← getInfoState).substituteLazy.get.trees
       for t in infoTrees do
         logInfoAt tk (← t.format)
   | _ => throwUnsupportedSyntax
diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index 9200aa518e..288913eb27 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -524,12 +524,12 @@ where
       if let some oldNext := old.nextCmdSnap? then do
         let newProm ← IO.Promise.new
         -- can reuse range, syntax unchanged
-        BaseIO.chainTask (sync := true) old.finishedSnap.task fun oldFinished =>
+        BaseIO.chainTask (sync := true) old.resultSnap.task fun oldResult =>
           -- also wait on old command parse snapshot as parsing is cheap and may allow for
           -- elaboration reuse
           BaseIO.chainTask (sync := true) oldNext.task fun oldNext => do
             let cancelTk ← IO.CancelToken.new
-            parseCmd oldNext newParserState oldFinished.cmdState newProm sync cancelTk ctx
+            parseCmd oldNext newParserState oldResult.cmdState newProm sync cancelTk ctx
         prom.resolve <| { old with nextCmdSnap? := some {
           stx? := none
           reportingRange? := some ⟨newParserState.pos, ctx.input.endPos⟩
@@ -582,7 +582,8 @@ where
       prom.resolve <| {
         diagnostics := .empty, stx := .missing, parserState
         elabSnap := default
-        finishedSnap := .finished none { diagnostics := .empty, cmdState }
+        resultSnap := .finished none { diagnostics := .empty, cmdState }
+        infoTreeSnap := .finished none { diagnostics := .empty }
         reportSnap := default
         nextCmdSnap? := none
       }
@@ -592,6 +593,7 @@ where
     let _ ← (if sync then BaseIO.asTask else (.pure <$> ·)) do
       -- definitely resolved in `doElab` task
       let elabPromise ← IO.Promise.new
+      let resultPromise ← IO.Promise.new
       let finishedPromise ← IO.Promise.new
       let reportPromise ← IO.Promise.new
       let minimalSnapshots := internal.cmdlineSnapshots.get cmdState.scopes.head!.opts
@@ -602,11 +604,6 @@ where
       -- report terminal tasks on first line of decl such as not to hide incremental tactics'
       -- progress
       let initRange? := getNiceCommandStartPos? stx |>.map fun pos => ⟨pos, pos⟩
-      let finishedSnap := {
-        stx? := stx'
-        reportingRange? := initRange?
-        task := finishedPromise.result!
-      }
       let next? ← if Parser.isTerminalCommand stx then pure none
         -- for now, wait on "command finished" snapshot before parsing next command
         else some <$> IO.Promise.new
@@ -621,21 +618,55 @@ where
       -- use per-command cancellation token for elaboration so that
       let elabCmdCancelTk ← IO.CancelToken.new
       prom.resolve {
-        diagnostics, finishedSnap, nextCmdSnap?
+        diagnostics, nextCmdSnap?
         stx := stx', parserState := parserState'
         elabSnap := { stx? := stx', task := elabPromise.result!, cancelTk? := some elabCmdCancelTk }
+        resultSnap := { stx? := stx', reportingRange? := initRange?, task := resultPromise.result! }
+        infoTreeSnap := { stx? := stx', reportingRange? := initRange?, task := finishedPromise.result! }
         reportSnap := { stx? := none, reportingRange? := initRange?, task := reportPromise.result! }
       }
       let cmdState ← doElab stx cmdState beginPos
         { old? := old?.map fun old => ⟨old.stx, old.elabSnap⟩, new := elabPromise }
-        finishedPromise elabCmdCancelTk ctx
+        elabCmdCancelTk ctx
+
+      let mut reportedCmdState := cmdState
+      let cmdline := internal.cmdlineSnapshots.get scope.opts && !Parser.isTerminalCommand stx
+      if cmdline then
+        -- discard all metadata apart from the environment; see `internal.cmdlineSnapshots`
+        reportedCmdState := { env := reportedCmdState.env, maxRecDepth := 0 }
+      resultPromise.resolve {
+        diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages)
+        traces := cmdState.traceState
+        cmdState := reportedCmdState
+      }
+
+      -- report info tree when relevant tasks are finished
+      BaseIO.chainTask (sync := true) (t := cmdState.infoState.substituteLazy) fun infoSt => do
+        let infoTree := infoSt.trees[0]!
+        let opts := cmdState.scopes.head!.opts
+        let mut msgLog := MessageLog.empty
+        if (← isTracingEnabledForCore `Elab.info opts) then
+          if let .ok msg ← infoTree.format.toBaseIO then
+            let data := .tagged `trace <| .trace { cls := `Elab.info } .nil #[msg]
+            msgLog := msgLog.add {
+              fileName := ctx.fileName
+              severity := MessageSeverity.information
+              pos      := ctx.fileMap.toPosition beginPos
+              data     := data
+            }
+        finishedPromise.resolve {
+          diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
+          infoTree? := infoTree
+        }
+
+      -- report traces when *all* tasks are finished
       let traceTask ←
         if (← isTracingEnabledForCore `Elab.snapshotTree cmdState.scopes.head!.opts) then
           -- We want to trace all of `CommandParsedSnapshot` but `traceTask` is part of it, so let's
           -- create a temporary snapshot tree containing all tasks but it
           let snaps := #[
             { stx? := stx', task := elabPromise.result!.map (sync := true) toSnapshotTree },
-            { stx? := stx', task := finishedPromise.result!.map (sync := true) toSnapshotTree }] ++
+            { stx? := stx', task := resultPromise.result!.map (sync := true) toSnapshotTree }] ++
             cmdState.snapshotTasks
           let tree := SnapshotTree.mk { diagnostics := .empty } snaps
           BaseIO.bindTask (← tree.waitAll) fun _ => do
@@ -665,8 +696,8 @@ where
         parseCmd none parserState cmdState next (sync := false) elabCmdCancelTk ctx
 
   doElab (stx : Syntax) (cmdState : Command.State) (beginPos : String.Pos)
-      (snap : SnapshotBundle DynamicSnapshot) (finishedPromise : IO.Promise CommandFinishedSnapshot)
-      (cancelTk : IO.CancelToken) : LeanProcessingM Command.State := do
+      (snap : SnapshotBundle DynamicSnapshot) (cancelTk : IO.CancelToken) :
+      LeanProcessingM Command.State := do
     let ctx ← read
     let scope := cmdState.scopes.head!
     -- reset per-command state
@@ -693,21 +724,9 @@ where
         data     := output
       }
     let cmdState : Command.State := { cmdState with messages }
-    let mut reportedCmdState := cmdState
     -- definitely resolve eventually
     snap.new.resolve <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
 
-    let infoTree : InfoTree := cmdState.infoState.trees[0]!
-    let cmdline := internal.cmdlineSnapshots.get scope.opts && !Parser.isTerminalCommand stx
-    if cmdline then
-      -- discard all metadata apart from the environment; see `internal.cmdlineSnapshots`
-      reportedCmdState := { env := reportedCmdState.env, maxRecDepth := 0 }
-    finishedPromise.resolve {
-      diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages)
-      infoTree? := infoTree
-      traces := cmdState.traceState
-      cmdState := reportedCmdState
-    }
     -- The reported `cmdState` in the snapshot may be minimized as seen above, so we return the full
     -- state here for further processing on the same thread
     return cmdState
@@ -735,6 +754,6 @@ where goCmd snap :=
   if let some next := snap.nextCmdSnap? then
     goCmd next.get
   else
-    snap.finishedSnap.get.cmdState
+    snap.resultSnap.get.cmdState
 
 end Lean
diff --git a/src/Lean/Language/Lean/Types.lean b/src/Lean/Language/Lean/Types.lean
index 7aa3b02658..5462d18e9e 100644
--- a/src/Lean/Language/Lean/Types.lean
+++ b/src/Lean/Language/Lean/Types.lean
@@ -25,12 +25,15 @@ private def pushOpt (a? : Option α) (as : Array α) : Array α :=
 
 /-! The hierarchy of Lean snapshot types -/
 
-/-- Snapshot after elaboration of the entire command. -/
-structure CommandFinishedSnapshot extends Language.Snapshot where
+/--
+Snapshot after command elaborator has returned. Also contains diagnostics from the elaborator's main
+task. Asynchronous elaboration tasks may not yet be finished.
+-/
+structure CommandResultSnapshot extends Language.Snapshot where
   /-- Resulting elaboration state. -/
   cmdState : Command.State
 deriving Nonempty
-instance : ToSnapshotTree CommandFinishedSnapshot where
+instance : ToSnapshotTree CommandResultSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
 
 /-- State after a command has been parsed. -/
@@ -44,8 +47,12 @@ structure CommandParsedSnapshot extends Snapshot where
   elaborator.
    -/
   elabSnap : SnapshotTask DynamicSnapshot
-  /-- State after processing is finished. -/
-  finishedSnap : SnapshotTask CommandFinishedSnapshot
+  /-- State after command elaborator has returned. -/
+  resultSnap : SnapshotTask CommandResultSnapshot
+  /--
+  State after all elaborator tasks are finished. In particular, contains the complete info tree.
+  -/
+  infoTreeSnap : SnapshotTask SnapshotLeaf
   /-- Additional, untyped snapshots used for reporting, not reuse. -/
   reportSnap : SnapshotTask SnapshotTree
   /-- Next command, unless this is a terminal command. -/
@@ -55,7 +62,8 @@ partial instance : ToSnapshotTree CommandParsedSnapshot where
   toSnapshotTree := go where
     go s := ⟨s.toSnapshot,
       #[s.elabSnap.map (sync := true) toSnapshotTree,
-        s.finishedSnap.map (sync := true) toSnapshotTree,
+        s.resultSnap.map (sync := true) toSnapshotTree,
+        s.infoTreeSnap.map (sync := true) toSnapshotTree,
         s.reportSnap] |>
         pushOpt (s.nextCmdSnap?.map (·.map (sync := true) go))⟩
 
diff --git a/src/Lean/Server/FileWorker/Utils.lean b/src/Lean/Server/FileWorker/Utils.lean
index 49fc89a549..539f639cfa 100644
--- a/src/Lean/Server/FileWorker/Utils.lean
+++ b/src/Lean/Server/FileWorker/Utils.lean
@@ -28,11 +28,11 @@ private partial def mkCmdSnaps (initSnap : Language.Lean.InitialSnapshot) :
     } <| .delayed <| headerSuccess.firstCmdSnap.task.asServerTask.bindCheap go
 where
   go cmdParsed :=
-    cmdParsed.finishedSnap.task.asServerTask.mapCheap fun finished =>
+    cmdParsed.resultSnap.task.asServerTask.mapCheap fun result =>
       .ok <| .cons {
         stx := cmdParsed.stx
         mpState := cmdParsed.parserState
-        cmdState := finished.cmdState
+        cmdState := result.cmdState
       } (match cmdParsed.nextCmdSnap? with
         | some next => .delayed <| next.task.asServerTask.bindCheap go
         | none => .nil)
diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean
index 223dde1dfd..41817245a4 100644
--- a/src/Lean/Server/Requests.lean
+++ b/src/Lean/Server/Requests.lean
@@ -304,10 +304,9 @@ def findCmdDataAtPos
   findCmdParsedSnap doc hoverPos |>.bindCheap fun
     | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos doc.meta.text hoverPos includeStop |>.bindCheap fun
       | some infoTree => .pure <| some (cmdParsed.stx, infoTree)
-      | none          => cmdParsed.finishedSnap.task.asServerTask.mapCheap fun s =>
-        -- the parser returns exactly one command per snapshot, and the elaborator creates exactly one node per command
-        assert! s.cmdState.infoState.trees.size == 1
-        some (cmdParsed.stx, s.cmdState.infoState.trees[0]!)
+      | none          => cmdParsed.infoTreeSnap.task.asServerTask.mapCheap fun s =>
+        assert! s.infoTree?.isSome
+        some (cmdParsed.stx, s.infoTree?.get!)
     | none => .pure none
 
 open Language in
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index a8d098c0f2..b8b4c7ade5 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -39,9 +39,11 @@ def msgLog (s : Snapshot) : MessageLog :=
   s.cmdState.messages
 
 def infoTree (s : Snapshot) : InfoTree :=
+  -- TODO: we should not block here!
+  let infoState := s.cmdState.infoState.substituteLazy.get
   -- the parser returns exactly one command per snapshot, and the elaborator creates exactly one node per command
-  assert! s.cmdState.infoState.trees.size == 1
-  s.cmdState.infoState.trees[0]!
+  assert! infoState.trees.size == 1
+  infoState.trees[0]!
 
 def isAtEnd (s : Snapshot) : Bool :=
   Parser.isTerminalCommand s.stx
diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
index 22ad57e8dd..f56dd99011 100644
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/tests/lean/1018unknowMVarIssue.lean.expected.out
@@ -1,6 +1,7 @@
-[Elab.info] • command @ ⟨6, 0⟩-⟨6, 31⟩ @ Lean.Elab.Command.elabSetOption
-      • [.] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨6, 0⟩-⟨6, 26⟩
-      • option trace.Elab.info @ ⟨6, 11⟩-⟨6, 26⟩
+[Elab.info] 
+  • command @ ⟨6, 0⟩-⟨6, 31⟩ @ Lean.Elab.Command.elabSetOption
+    • [.] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨6, 0⟩-⟨6, 26⟩
+    • option trace.Elab.info @ ⟨6, 11⟩-⟨6, 26⟩
 1018unknowMVarIssue.lean:9:18-9:19: error: don't know how to synthesize placeholder
 context:
 α✝ β : Type
@@ -8,75 +9,77 @@ x : Fam2 α✝ β
 α : Type
 a : α
 ⊢ α
-[Elab.info] • command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
-      • α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
-        • [.] α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
-        • α : Type @ ⟨7, 13⟩-⟨7, 14⟩
-      • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
-      • Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
-        • [.] Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩
-        • Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
-        • α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
-          • [.] α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
-          • α : Type @ ⟨7, 26⟩-⟨7, 27⟩
-        • β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent
-          • [.] β : some Type @ ⟨7, 28⟩-⟨7, 29⟩
-          • β : Type @ ⟨7, 28⟩-⟨7, 29⟩
-      • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
-      • β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
-        • [.] β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩
-        • β : Type @ ⟨7, 33⟩-⟨7, 34⟩
-      • CustomInfo(Lean.Elab.InlayHint)
-      • _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†!-⟨7, 7⟩†!
-      • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
-      • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
-      • CustomInfo(Lean.Elab.Term.BodyInfo)
-        • Partial term @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.Quotation.elabMatchSyntax
-        • match α, β, x, a with
-          | α_1, .(α_1), Fam2.any, a => ?m x α_1 a
-          | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
-          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
-            • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
-            • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
-          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
-            • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
-            • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
-          • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-          • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-          • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-          • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
-          • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
-          • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
-          • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-          • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-          • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-          • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
-          • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
-            • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
-          • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.592 -> _uniq.319
-          • FVarAlias α: _uniq.591 -> _uniq.317
-          • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
-          • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
-          • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
-          • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
-          • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
-          • [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
-          • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
-            • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
-          • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.623 -> _uniq.319
-          • FVarAlias n: _uniq.622 -> _uniq.317
-          • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
-            • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
-            • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
-      • @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
-[Elab.info] • command @ ⟨11, 0⟩-⟨11, 0⟩ @ Lean.Elab.Command.elabEoi
+[Elab.info] 
+  • command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
+    • α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
+      • [.] α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
+      • α : Type @ ⟨7, 13⟩-⟨7, 14⟩
+    • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
+    • Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
+      • [.] Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩
+      • Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
+      • α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
+        • [.] α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
+        • α : Type @ ⟨7, 26⟩-⟨7, 27⟩
+      • β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent
+        • [.] β : some Type @ ⟨7, 28⟩-⟨7, 29⟩
+        • β : Type @ ⟨7, 28⟩-⟨7, 29⟩
+    • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
+    • β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
+      • [.] β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩
+      • β : Type @ ⟨7, 33⟩-⟨7, 34⟩
+    • CustomInfo(Lean.Elab.InlayHint)
+    • _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†!-⟨7, 7⟩†!
+    • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
+    • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
+    • CustomInfo(Lean.Elab.Term.BodyInfo)
+      • Partial term @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.Quotation.elabMatchSyntax
+      • match α, β, x, a with
+        | α_1, .(α_1), Fam2.any, a => ?m x α_1 a
+        | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
+        • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
+          • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
+          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
+        • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
+          • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
+          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
+        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+        • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
+        • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
+        • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
+        • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
+        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+        • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
+        • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
+        • [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
+        • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
+        • α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+        • α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+        • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
+          • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
+        • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
+        • FVarAlias a: _uniq.592 -> _uniq.319
+        • FVarAlias α: _uniq.591 -> _uniq.317
+        • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
+        • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
+        • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
+        • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
+        • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
+        • [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
+        • [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
+        • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
+        • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+        • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+        • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
+          • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
+        • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
+        • FVarAlias a: _uniq.623 -> _uniq.319
+        • FVarAlias n: _uniq.622 -> _uniq.317
+        • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
+          • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
+          • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
+    • @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
+[Elab.info] 
+  • command @ ⟨11, 0⟩-⟨11, 0⟩ @ Lean.Elab.Command.elabEoi
diff --git a/tests/lean/binopInfoTree.lean.expected.out b/tests/lean/binopInfoTree.lean.expected.out
index fe614bbbd9..4872b7485a 100644
--- a/tests/lean/binopInfoTree.lean.expected.out
+++ b/tests/lean/binopInfoTree.lean.expected.out
@@ -1,76 +1,80 @@
-[Elab.info] • command @ ⟨3, 0⟩-⟨3, 31⟩ @ Lean.Elab.Command.elabSetOption
-      • [.] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨3, 0⟩-⟨3, 26⟩
-      • option trace.Elab.info @ ⟨3, 11⟩-⟨3, 26⟩
+[Elab.info] 
+  • command @ ⟨3, 0⟩-⟨3, 31⟩ @ Lean.Elab.Command.elabSetOption
+    • [.] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨3, 0⟩-⟨3, 26⟩
+    • option trace.Elab.info @ ⟨3, 11⟩-⟨3, 26⟩
 1 + 2 + 3 : Nat
-[Elab.info] • command @ ⟨5, 0⟩-⟨5, 16⟩ @ Lean.Elab.Command.elabCheck
-      • 1 + 2 + 3 : Nat @ ⟨5, 7⟩-⟨5, 16⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
-        • Macro expansion
-          1 + 2 +
-            3
-              -- should propagate through multiple macro expansions
-          ===>
-          binop% HAdd.hAdd✝ (1 + 2)
-            3
-              -- should propagate through multiple macro expansions
-          • 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩† @ Lean.Elab.Term.Op.elabBinOp
-            • 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩†
-              • 1 + 2 : Nat @ ⟨5, 7⟩-⟨5, 12⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
-                • Macro expansion
-                  1 + 2
-                  ===>
-                  binop% HAdd.hAdd✝ 1 2
-                  • 1 + 2 : Nat @ ⟨5, 7⟩†-⟨5, 12⟩†
-                    • [.] HAdd.hAdd✝ : none @ ⟨5, 7⟩†-⟨5, 16⟩†
-                    • [.] HAdd.hAdd✝ : none @ ⟨5, 7⟩†-⟨5, 12⟩†
-                    • 1 : Nat @ ⟨5, 7⟩-⟨5, 8⟩ @ Lean.Elab.Term.elabNumLit
-                    • 2 : Nat @ ⟨5, 11⟩-⟨5, 12⟩ @ Lean.Elab.Term.elabNumLit
-              • 3 : Nat @ ⟨5, 15⟩-⟨5, 16⟩ @ Lean.Elab.Term.elabNumLit
+[Elab.info] 
+  • command @ ⟨5, 0⟩-⟨5, 16⟩ @ Lean.Elab.Command.elabCheck
+    • 1 + 2 + 3 : Nat @ ⟨5, 7⟩-⟨5, 16⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
+      • Macro expansion
+        1 + 2 +
+          3
+            -- should propagate through multiple macro expansions
+        ===>
+        binop% HAdd.hAdd✝ (1 + 2)
+          3
+            -- should propagate through multiple macro expansions
+        • 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩† @ Lean.Elab.Term.Op.elabBinOp
+          • 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩†
+            • 1 + 2 : Nat @ ⟨5, 7⟩-⟨5, 12⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
+              • Macro expansion
+                1 + 2
+                ===>
+                binop% HAdd.hAdd✝ 1 2
+                • 1 + 2 : Nat @ ⟨5, 7⟩†-⟨5, 12⟩†
+                  • [.] HAdd.hAdd✝ : none @ ⟨5, 7⟩†-⟨5, 16⟩†
+                  • [.] HAdd.hAdd✝ : none @ ⟨5, 7⟩†-⟨5, 12⟩†
+                  • 1 : Nat @ ⟨5, 7⟩-⟨5, 8⟩ @ Lean.Elab.Term.elabNumLit
+                  • 2 : Nat @ ⟨5, 11⟩-⟨5, 12⟩ @ Lean.Elab.Term.elabNumLit
+            • 3 : Nat @ ⟨5, 15⟩-⟨5, 16⟩ @ Lean.Elab.Term.elabNumLit
 fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int
-[Elab.info] • command @ ⟨7, 0⟩-⟨7, 48⟩ @ Lean.Elab.Command.elabCheck
-      • fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int @ ⟨7, 7⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabFun
-        • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent
-          • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩
-          • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩
-        • n (isBinder := true) : Nat @ ⟨7, 12⟩-⟨7, 13⟩
-        • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent
-          • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩
-          • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩
-        • m (isBinder := true) : Nat @ ⟨7, 14⟩-⟨7, 15⟩
-        • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent
-          • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩
-          • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩
-        • l (isBinder := true) : Nat @ ⟨7, 16⟩-⟨7, 17⟩
-        • ↑n + (↑m + ↑l) : Int @ ⟨7, 28⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabTypeAscription
-          • Int : Type @ ⟨7, 44⟩-⟨7, 47⟩ @ Lean.Elab.Term.elabIdent
-            • [.] Int : some Sort.{?_uniq} @ ⟨7, 44⟩-⟨7, 47⟩
-            • Int : Type @ ⟨7, 44⟩-⟨7, 47⟩
-          • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩-⟨7, 41⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
-            • Macro expansion
-              n + (m +' l)
-              ===>
-              binop% HAdd.hAdd✝ n (m +' l)
-              • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† @ Lean.Elab.Term.Op.elabBinOp
-                • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩†
-                  • [.] HAdd.hAdd✝ : none @ ⟨7, 29⟩†-⟨7, 41⟩†
-                  • n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ @ Lean.Elab.Term.elabIdent
-                    • [.] n : none @ ⟨7, 29⟩-⟨7, 30⟩
-                    • n : Nat @ ⟨7, 29⟩-⟨7, 30⟩
-                  • ↑m + ↑l : Int @ ⟨7, 34⟩-⟨7, 40⟩ @ «_aux_binopInfoTree___macroRules_term_+'__1»
-                    • Macro expansion
-                      m +' l
-                      ===>
-                      m + l
-                      • ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩† @ «_aux_Init_Notation___macroRules_term_+__2»
-                        • Macro expansion
-                          m + l
-                          ===>
-                          binop% HAdd.hAdd✝ m l
-                          • ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩†
-                            • [.] HAdd.hAdd✝ : none @ ⟨7, 34⟩†-⟨7, 40⟩†
-                            • m : Nat @ ⟨7, 34⟩-⟨7, 35⟩ @ Lean.Elab.Term.elabIdent
-                              • [.] m : none @ ⟨7, 34⟩-⟨7, 35⟩
-                              • m : Nat @ ⟨7, 34⟩-⟨7, 35⟩
-                            • l : Nat @ ⟨7, 39⟩-⟨7, 40⟩ @ Lean.Elab.Term.elabIdent
-                              • [.] l : none @ ⟨7, 39⟩-⟨7, 40⟩
-                              • l : Nat @ ⟨7, 39⟩-⟨7, 40⟩
-[Elab.info] • command @ ⟨8, 0⟩-⟨8, 0⟩ @ Lean.Elab.Command.elabEoi
+[Elab.info] 
+  • command @ ⟨7, 0⟩-⟨7, 48⟩ @ Lean.Elab.Command.elabCheck
+    • fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int @ ⟨7, 7⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabFun
+      • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent
+        • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩
+        • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩
+      • n (isBinder := true) : Nat @ ⟨7, 12⟩-⟨7, 13⟩
+      • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent
+        • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩
+        • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩
+      • m (isBinder := true) : Nat @ ⟨7, 14⟩-⟨7, 15⟩
+      • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent
+        • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩
+        • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩
+      • l (isBinder := true) : Nat @ ⟨7, 16⟩-⟨7, 17⟩
+      • ↑n + (↑m + ↑l) : Int @ ⟨7, 28⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabTypeAscription
+        • Int : Type @ ⟨7, 44⟩-⟨7, 47⟩ @ Lean.Elab.Term.elabIdent
+          • [.] Int : some Sort.{?_uniq} @ ⟨7, 44⟩-⟨7, 47⟩
+          • Int : Type @ ⟨7, 44⟩-⟨7, 47⟩
+        • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩-⟨7, 41⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
+          • Macro expansion
+            n + (m +' l)
+            ===>
+            binop% HAdd.hAdd✝ n (m +' l)
+            • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† @ Lean.Elab.Term.Op.elabBinOp
+              • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩†
+                • [.] HAdd.hAdd✝ : none @ ⟨7, 29⟩†-⟨7, 41⟩†
+                • n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ @ Lean.Elab.Term.elabIdent
+                  • [.] n : none @ ⟨7, 29⟩-⟨7, 30⟩
+                  • n : Nat @ ⟨7, 29⟩-⟨7, 30⟩
+                • ↑m + ↑l : Int @ ⟨7, 34⟩-⟨7, 40⟩ @ «_aux_binopInfoTree___macroRules_term_+'__1»
+                  • Macro expansion
+                    m +' l
+                    ===>
+                    m + l
+                    • ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩† @ «_aux_Init_Notation___macroRules_term_+__2»
+                      • Macro expansion
+                        m + l
+                        ===>
+                        binop% HAdd.hAdd✝ m l
+                        • ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩†
+                          • [.] HAdd.hAdd✝ : none @ ⟨7, 34⟩†-⟨7, 40⟩†
+                          • m : Nat @ ⟨7, 34⟩-⟨7, 35⟩ @ Lean.Elab.Term.elabIdent
+                            • [.] m : none @ ⟨7, 34⟩-⟨7, 35⟩
+                            • m : Nat @ ⟨7, 34⟩-⟨7, 35⟩
+                          • l : Nat @ ⟨7, 39⟩-⟨7, 40⟩ @ Lean.Elab.Term.elabIdent
+                            • [.] l : none @ ⟨7, 39⟩-⟨7, 40⟩
+                            • l : Nat @ ⟨7, 39⟩-⟨7, 40⟩
+[Elab.info] 
+  • command @ ⟨8, 0⟩-⟨8, 0⟩ @ Lean.Elab.Command.elabEoi