Documentation

Lean.Linter.Sets

source
def Lean.Linter.insertLinterSet {m : Type → Type} [MonadEnv m] (setName : Name) (linterNames : NameSet) :
m Unit

Add a new linter set that contains the given linters.

Instances For
    source
    def Lean.Linter.registerSet (setName : Name) (ref : Name := by exact decl_name%) :
    IO (Lean.Option Bool)

    registerSet wraps registerOption by setting relevant values.

    Instances For
      source
      def Lean.Linter.«command_Register_linter_set_:=_» :
      ParserDescr

      Declare a new linter set by giving the set of options that will be enabled along with the set.

      Instances For