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.
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.