Additional utilities and boilerplate for the Linter API

@[macro_inline]

def Lean.Linter.whenLinterOption {m : Type → Type} [Monad m] [MonadOptions m] [MonadEnv m] (opt : Lean.Option Bool) (x : m Unit) : m Unit

Runs a CommandElabM action when the provided linter option is true.

This function assumes you have already called withSetOptionIn; use whenLinterActivated to do so automatically. At the start of linter code, whenLinterActivated should be preferred when possible.

Note: this definition is marked as @[macro_inline], so it is okay to supply it with a linter option which has been registered in the same module.

@[macro_inline]

def Lean.Linter.whenNotLinterOption {m : Type → Type} [Monad m] [MonadOptions m] [MonadEnv m] (opt : Lean.Option Bool) (x : m Unit) : m Unit

Runs a CommandElabM action when the provided linter option is false.

Note: this definition is marked as @[macro_inline], so it is okay to supply it with a linter option which has been registered in the same module.

@[macro_inline]

def Lean.Linter.whenLinterActivated (opt : Lean.Option Bool) (x : Elab.Command.CommandElab) (breakOnError : Bool := true) : Elab.Command.CommandElab

Processes set_option ... ins that wrap the input stx, then acts on the inner syntax with x after checking that the provided linter option is true.

If breakOnError is true (the default), avoids running the linter when errors are present.

This is typically used to start off linter code:

def myLinter : Linter where
  run := whenLinterActivated linter.myLinter fun stx ↦ do
    ...

Note: this definition is marked as @[macro_inline], so it is okay to supply it with a linter option which has been registered in the same module.