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.
Equations
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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: determinining the LinterSets
would otherwise require a MonadEnv
instance.
- toOptions : Options
- linterSets : LinterSets
Instances For
Equations
- o.get = Lean.KVMap.get o.toOptions
Instances For
Equations
Instances For
Equations
- o.toLinterOptions = do let __do_lift ← Lean.getEnv let linterSets : Lean.Linter.LinterSets := Lean.Linter.linterSetsExt.getState __do_lift pure { toOptions := o, linterSets := linterSets }
Instances For
Return the set of linter sets that this option is contained in.
Equations
- o.getSet opt = Lean.RBMap.findD o.linterSets opt.name #[]
Instances For
Equations
- Lean.Linter.getLinterOptions = do let __do_lift ← Lean.getOptions __do_lift.toLinterOptions
Instances For
Equations
- Lean.Linter.getLinterAll o defValue = o.get Lean.Linter.linter.all.name defValue
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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:
- If it is set, then the value determines whether or not it is enabled.
- Otherwise, if
linter.all
is set, then its value determines whether or not the option is enabled. - 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.)
- Otherwise, the default value determines whether or not it is enabled.
Equations
- One or more equations did not get rendered due to their size.