This file contains functions that are used by multiple linters.

def Mathlib.Linter.getNamesFrom {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadFileMap m] (pos : String.Pos) : m (Array Lean.Syntax)

If pos is a String.Pos, then getNamesFrom pos returns the array of identifiers for the names of the declarations whose syntax begins in position at least pos.

def Mathlib.Linter.getAliasSyntax {m : Type → Type} [Monad m] [Lean.MonadResolveName m] (stx : Lean.Syntax) : m (Array Lean.Syntax)

If stx is a syntax node for an export statement, then getAliasSyntax stx returns the array of identifiers with the "exported" names.

def Mathlib.Linter.logLint0Disable {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (linterOption : Lean.Option Nat) (stx : Lean.Syntax) (msg : Lean.MessageData) : m Unit

Used for linters which use 0 instead of false for disabling.