Documentation

Lean.Linter.PersistentLintLog

source
structure Lean.Linter.LintEntry :
Type
Instances For
    source
    opaque Lean.Linter.lintLogExt :
    PersistentEnvExtension LintEntry LintEntry (Array LintEntry)
    source
    def Lean.Linter.getAllLints (env : Environment) :
    Array (Name × Array LintEntry)
    Instances For
      source
      def Lean.Linter.recordLints (env : Environment) (messages : MessageLog) :
      BaseIO Environment
      Instances For