def Lean.Linter.LinterSets : Type

Linter sets are represented as a map from linter name to set name, to make it easy to look up which sets to check for enabling a linter.

@[implicit_reducible]

instance Lean.Linter.instEmptyCollectionLinterSets : EmptyCollection LinterSets

@[implicit_reducible]

instance Lean.Linter.instInhabitedLinterSets : Inhabited LinterSets

def Lean.Linter.insertLinterSetEntry (map : LinterSets) (setName : Name) (options : NameSet) : LinterSets

Insert a set into a LinterSets map.

entry.1 is the name of the linter set, entry.2 contains the names of the set's linter options.

opaque Lean.Linter.linterSetsExt : SimplePersistentEnvExtension (Name × NameSet) LinterSets

structure Lean.Linter.LinterOptions : Type

The LinterOptions structure is used to determine whether given linters are enabled.

This structure contains all the data required to do so, the Options set on the command line or by the set_option command, and the LinterSets that have been declared.

A single structure holding this data is useful since we want getLinterValue to be a pure function: determining the LinterSets would otherwise require a MonadEnv instance.

• toOptions : Options
• linterSets : LinterSets

def Lean.Linter.LinterOptions.get {α : Type} [KVMap.Value α] (o : LinterOptions) (k : Name) (defVal : α) : α

def Lean.Linter.LinterOptions.get? {α : Type} [KVMap.Value α] (o : LinterOptions) (k : Name) : Option α

def Lean.Options.toLinterOptions {m : Type → Type} [Monad m] [MonadEnv m] (o : Options) : m Linter.LinterOptions

def Lean.Linter.LinterOptions.getSet {α : Type} (o : LinterOptions) (opt : Lean.Option α) : Array Name

Return the set of linter sets that this option is contained in.

def Lean.Linter.getLinterOptions {m : Type → Type} [Monad m] [MonadOptions m] [MonadEnv m] : m LinterOptions

opaque Lean.Linter.linter.all : Lean.Option Bool

opaque Lean.Linter.linter.extra : Lean.Option Bool

def Lean.Linter.getLinterAll (o : LinterOptions) (defValue : Bool := linter.all.defValue) : Bool

def Lean.Linter.getLinterExtra (o : LinterOptions) (defValue : Bool := linter.extra.defValue) : Bool

def Lean.Linter.getLinterValue (opt : Lean.Option Bool) (o : LinterOptions) : Bool

def Lean.Linter.getLinterValueExtra (opt : Lean.Option Bool) (o : LinterOptions) : Bool

Like getLinterValue, but the cross-linter fallback is linter.extra instead of linter.all.

def Lean.Linter.linterMessageTag : Name

Tag attached by logLint to every linter warning so consumers (e.g. Lean.Linter.recordLints) can distinguish linter-produced messages from other tagged messages such as named errors or unknown-identifier messages.

def Lean.Linter.logLint {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit

def Lean.MessageData.isLinterMessage (msg : MessageData) : Bool

Returns true if msg was produced by Lean.Linter.logLint (and therefore by a linter).

def Lean.Linter.logLintIf {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadEnv m] (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit

If linterOption is enabled, print a linter warning message at the position determined by stx.

Whether a linter option is enabled or not is determined by the following sequence:

1. If it is set, then the value determines whether or not it is enabled.
2. Otherwise, if linter.all is set, then its value determines whether or not the option is enabled.
3. Otherwise, if any of the linter sets containing the option is enabled, it is enabled. (Only enabled linter sets are considered: explicitly disabling a linter set will revert the linters it contains to their default behavior.)
4. Otherwise, the default value determines whether or not it is enabled.

def Lean.Linter.logLintIfExtra {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadEnv m] (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit

Like logLintIf, but uses getLinterValueExtra to gate emission on the extra fallback. Use for extra linters: emits the warning iff linterOption is on under the extra selection rules described on getLinterValueExtra.