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

• Lean.Linter.insertLinterSet setName linterNames = Lean.modifyEnv fun (x : Lean.Environment) => Lean.PersistentEnvExtension.addEntry Lean.Linter.linterSetsExt x (setName, linterNames)

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

registerSet wraps registerOption by setting relevant values.

Equations

• Lean.Linter.registerSet setName ref = do Lean.registerOption setName { declName := ref, defValue := Lean.DataValue.ofBool false, group := "linterSet" } pure { name := setName, defValue := false }

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

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