structure Lean.Linter.LintEntry : Type

• linter : Name
• message : SerialMessage

opaque Lean.Linter.lintLogExt : PersistentEnvExtension LintEntry LintEntry (Array LintEntry)

def Lean.Linter.getAllLints (env : Environment) : Array (Name × Array LintEntry)

Equations

• Lean.Linter.getAllLints env = Array.mapIdx (fun (i : Nat) (mod : Lean.Name) => (mod, Lean.Linter.lintLogExt.getModuleEntries env i)) env.header.moduleNames

def Lean.Linter.recordLints (env : Environment) (messages : MessageLog) : BaseIO Environment

Equations

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