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

def Lean.Linter.collectMacroExpansions? {m : Type → Type u_1} [Monad m] (range : String.Range) (tree : Lean.Elab.InfoTree) : m (Option (List Lean.Elab.MacroExpansionInfo))

Go upwards through the given tree starting from the smallest node that contains the given range and collect all MacroExpansionInfos on the way up. The result is some [] if no MacroExpansionInfo was found on the way and none if no InfoTree node was found that covers the given range.

Return the result reversed, s.t. the macro expansion that would be applied to the original syntax first is the first element of the returned list.

Equations

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

def Lean.Linter.collectMacroExpansions?.go {m : Type → Type u_1} [Monad m] (range : String.Range) (tree : Lean.Elab.InfoTree) : m (Option (Option (List Lean.Elab.MacroExpansionInfo)))

Equations

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