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.Raw) :
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.