Additional declarations related to linters

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