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.