def Lean.Linter.collectMacroExpansions? {m : Type → Type u_1} [Monad m] (range : Syntax.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 MacroExpansionInfos 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.getDeclsByBody (t : Elab.InfoTree) : List Name

Get the parentDecls of every elaborated body in the infotree.

Equations

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

def Lean.Linter.getNewDecls (t : Elab.InfoTree) : List Name

Get the names of declarations introduced by elaborating t.

A declaration introduces a TermInfo with isBinder := true whose expr is the constant being declared. This covers def/theorem/axiom, inductive types and their constructors, and structure fields and parent projections — including mutual blocks where each member emits its own binder.

Equations

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

def Lean.Linter.findMatchingDecl? {m : Type → Type} [Monad m] [Elab.MonadInfoTree m] [MonadEnv m] [MonadFileMap m] (stx : Syntax) : m (Option Name)

Find the declaration in the current file that stx belongs to.

Searches the info trees of the current command for declarations (see getNewDecls) whose declaration range contains the range of stx, and returns the one whose range starts earliest. Returns none if stx has no position or no declaration's range contains it (e.g. for commands such as #check or open).

Equations

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

def Lean.Linter.findCodeQualitySource? {m : Type → Type} [Monad m] [Elab.MonadInfoTree m] [MonadEnv m] [MonadFileMap m] (stx : Syntax) : m (Option CodeQuality.Source)

Build a code-quality Source attributing stx to the declaration it belongs to (see findMatchingDecl?), or none if no declaration matches.

Equations

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

def Lean.Linter.findCodeQualitySource {m : Type → Type} [Monad m] [Elab.MonadInfoTree m] [MonadEnv m] [MonadFileMap m] (stx : Syntax) : m CodeQuality.Source

Build a code-quality Source attributing stx to the declaration it belongs to (see findMatchingDecl?), falling back to the current module if no declaration matches.

Equations

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