max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: allow async elab tasks to contribute to info trees reported to linters and request handlers (#7457)

Browse source 
This PR ensures info tree users such as linters and request handlers
have access to info subtrees created by async elab task by introducing
API to leave holes filled by such tasks.

**Breaking change**: other metaprogramming users of
`Command.State.infoState` may need to call `InfoState.substituteLazy` on
it manually to fill all holes.
This commit is contained in:
Sebastian Ullrich 2025-03-13 16:09:00 +01:00 • committed by GitHub
parent 0f3d426591
commit 96f9ee2a41
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
16 changed files with 306 additions and 217 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init.lean
View file

@ -40,3 +40,4 @@ import Init.Syntax
import Init.Internal
import Init.Try
import Init.BinderNameHint
import Init.Task

7
src/Init/System/IO.lean
View file

@ -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

29
src/Init/Task.lean Normal file
View file

@ -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

3
src/Lean/CoreM.lean
View file

@ -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

51
src/Lean/Elab/Command.lean
View file

@ -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 }

4
src/Lean/Elab/Frontend.lean
View file

@ -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)

8
src/Lean/Elab/InfoTree/Main.lean
View file

@ -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
/-

5
src/Lean/Elab/InfoTree/Types.lean
View file

@ -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

2
src/Lean/Elab/InfoTrees.lean
View file

@ -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

71
src/Lean/Language/Lean.lean
View file

@ -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

20
src/Lean/Language/Lean/Types.lean
View file

@ -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))⟩

4
src/Lean/Server/FileWorker/Utils.lean
View file

@ -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)

7
src/Lean/Server/Requests.lean
View file

@ -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

6
src/Lean/Server/Snapshots.lean
View file

@ -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

153
tests/lean/1018unknowMVarIssue.lean.expected.out
View file

@ -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

152
tests/lean/binopInfoTree.lean.expected.out
View file

@ -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