source
def Lean.Linter.collectMacroExpansions? {m : Type → Type u_1} [Monad m] (range : String.Range) (tree : Elab.InfoTree) :
m (Option (List Elab.MacroExpansionInfo))

Go upwards through the given `tree` starting from the smallest node that contains the given `range` and collect all `MacroExpansionInfo`s on the way up. The result is `some []` if no `MacroExpansionInfo` was found on the way and `none` if no `InfoTree` node was found that covers the given `range`.

Return the result reversed, s.t. the macro expansion that would be applied to the original syntax first is the first element of the returned list.

Equations

- One or more equations did not get rendered due to their size.

Instances For