def
Lean.Linter.logLint
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadLog m]
[inst : Lean.AddMessageContext m]
[inst : Lean.MonadOptions m]
(linterOption : Lean.Option Bool)
(stx : Lean.Syntax)
(msg : Lean.MessageData)
:

m Unit

## Equations

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

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

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.

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

m (Option (Option (List Lean.Elab.MacroExpansionInfo)))

## Equations

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