Documentation

Lean.Linter.Sets

def Lean.Linter.insertLinterSet {m : TypeType} [MonadEnv m] (setName : Name) (linterNames : NameSet) :

Add a new linter set that contains the given linters.

Equations
Instances For
    def Lean.Linter.registerSet (setName : Name) (ref : Name := by exact decl_name%) :

    registerSet wraps registerOption by setting relevant values.

    Equations
    Instances For

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

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