The "DocString" style linter

The "DocString" linter validates style conventions regarding doc-string formatting.

opaque Mathlib.Linter.linter.style.docString : Lean.Option Bool

The "DocString" linter validates style conventions regarding doc-string formatting.

opaque Mathlib.Linter.linter.style.docString.empty : Lean.Option Bool

The "empty doc string" warns on empty doc-strings.

@[irreducible]

def Mathlib.Linter.getDeclModifiers : Lean.Syntax → Array Lean.Syntax

Extract all declModifiers from the input syntax. We later extract the docstring from it, but we avoid extracting directly the docComment node, to skip #adaptation_notes.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Linter.getDeclModifiers x✝ = #[]