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

def Lean.Linter.getLinterAll (o : Lean.Options) (defValue : optParam Bool Lean.Linter.linter.all.defValue) : Bool

Equations

• Lean.Linter.getLinterAll o defValue = Lean.KVMap.get o Lean.Linter.linter.all.name defValue

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

Equations

• Lean.Linter.getLinterValue opt o = Lean.KVMap.get o opt.name (Lean.Linter.getLinterAll o opt.defValue)

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

Equations

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

def Lean.Linter.logLintIf {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (linterOption : Lean.Option Bool) (stx : Lean.Syntax) (msg : Lean.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, the default value determines whether or not it is enabled.

Equations

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