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.

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

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

          Equations
            Instances For