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)
Instances For
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 }
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.