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 true, print a linter warning message at the position determined by stx.

Equations

• Lean.Linter.logLintIf linterOption stx msg = do let __do_lift ← Lean.getOptions if Lean.Option.get __do_lift linterOption = true then Lean.Linter.logLint linterOption stx msg else pure PUnit.unit