inductive Lean.Linter.EnvLinter.LintVerbosity : Type

Verbosity for the linter output.

• low : LintVerbosity

  low: only print failing checks, print nothing on success.

• medium : LintVerbosity

  medium: only print failing checks, print confirmation on success.

• high : LintVerbosity

  high: print output of every check.

@[implicit_reducible]

instance Lean.Linter.EnvLinter.instInhabitedLintVerbosity : Inhabited LintVerbosity

Equations

• Lean.Linter.EnvLinter.instInhabitedLintVerbosity = { default := Lean.Linter.EnvLinter.instInhabitedLintVerbosity.default }

@[implicit_reducible]

instance Lean.Linter.EnvLinter.instDecidableEqLintVerbosity : DecidableEq LintVerbosity

Equations

• Lean.Linter.EnvLinter.instDecidableEqLintVerbosity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lean.Linter.EnvLinter.instReprLintVerbosity.repr : LintVerbosity → Nat → Format

Equations

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

@[implicit_reducible]

instance Lean.Linter.EnvLinter.instReprLintVerbosity : Repr LintVerbosity

Equations

• Lean.Linter.EnvLinter.instReprLintVerbosity = { reprPrec := Lean.Linter.EnvLinter.instReprLintVerbosity.repr }

def Lean.Linter.EnvLinter.getEnvLinters (opts? : Option LinterOptions := none) : CoreM (Array NamedEnvLinter)

Getter for the registered environment linters. The result is sorted by the linter option name.

Equations

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

def Lean.Linter.EnvLinter.isLinterEnabledFor (env : Environment) (linter : NamedEnvLinter) (decl : Name) : Bool

Queries the envLinterSnapshotExt to see if a given environment linter is enabled for the given declaration.

Equations

• Lean.Linter.EnvLinter.isLinterEnabledFor env linter decl = match Lean.Linter.getEnvLinterSnapshotEntry? env decl linter.optName with | some b => b | none => false

def Lean.Linter.EnvLinter.lintCore (decls : Array Name) (linters : Array NamedEnvLinter) : CoreM (Array (NamedEnvLinter × Std.HashMap Name MessageData))

Runs all the specified linters on all the specified declarations in parallel, producing a list of results.

Equations

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

def Lean.Linter.EnvLinter.sortResults {α : Type} (results : Std.HashMap Name α) : CoreM (Array (Name × α))

Sorts a map with declaration keys as names by line number.

Equations

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

def Lean.Linter.EnvLinter.printWarning (declName : Name) (warning : MessageData) (useErrorFormat : Bool := false) (filePath : System.FilePath := default) : CoreM MessageData

Formats a linter warning as #check command with comment.

Equations

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

def Lean.Linter.EnvLinter.printWarnings (results : Std.HashMap Name MessageData) (filePath : System.FilePath := default) (useErrorFormat : Bool := false) : CoreM MessageData

Formats a map of linter warnings using printWarning, sorted by line number.

Equations

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

def Lean.Linter.EnvLinter.groupedByFilename (results : Std.HashMap Name MessageData) (useErrorFormat : Bool := false) : CoreM MessageData

Formats a map of linter warnings grouped by filename with -- filename comments.

Equations

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

def Lean.Linter.EnvLinter.formatLinterResults (results : Array (NamedEnvLinter × Std.HashMap Name MessageData)) (decls : Array Name) (groupByFilename : Bool) (whereDesc : String) (verbose : LintVerbosity) (numLinters : Nat) (useErrorFormat : Bool := false) : CoreM MessageData

Formats the linter results as Lean code with comments and #check commands.

Equations

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

def Lean.Linter.EnvLinter.getDeclsInCurrModule : CoreM (Array Name)

Get the list of declarations in the current module.

Equations

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

def Lean.Linter.EnvLinter.getAllDecls : CoreM (Array Name)

Get the list of all declarations in the environment.

Equations

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

def Lean.Linter.EnvLinter.getDeclsInPackage (pkg : Name) : CoreM (Array Name)

Get the list of all declarations in the specified package.

Equations

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