Documentation

Lean.Linter.Util

opaque Lean.Linter.linter.all:

Lean.Option Bool

def Lean.Linter.getLinterAll (o : Lean.Options) :

Equations

Lean.Linter.getLinterAll o = Lean.KVMap.get o Lean.Linter.linter.all.name Lean.Linter.linter.all.defValue

def Lean.Linter.publishMessage (content : String) (range : String.Range) (severity : optParam Lean.MessageSeverity Lean.MessageSeverity.warning) :

Lean.Elab.Command.CommandElabM Unit

Equations

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

@[inline]

abbrev Lean.Linter.SyntaxStack:

Type

Equations

Lean.Linter.SyntaxStack = List (Lean.Syntax × Nat)

def Lean.Linter.findSyntaxStack? (root : Lean.Syntax) (child : Lean.Syntax) :

Option Lean.Linter.SyntaxStack

Equations

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

partial def Lean.Linter.findSyntaxStack?.go (child : Lean.Syntax) (childRange : String.Range) (stack : Lean.Linter.SyntaxStack) (stx : Lean.Syntax) :

Option Lean.Linter.SyntaxStack

def Lean.Linter.stackMatches (stack : Lean.Linter.SyntaxStack) (pattern : List (Option Lean.SyntaxNodeKind)) :

Equations

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