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.

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

The docStringVerso linter warns on docstrings that cannot be parsed by Verso. Since this linter only checks syntax, not semantics, it is no assurance that complying docstrings are actually accepted by Verso.

@[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✝ = #[]