# The "DocString" style linter #

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

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

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

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

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

source
@[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_note`s.

Equations

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

Instances For

source
def Mathlib.Linter.deindentString (currIndent : Nat) (docString : String) :
String

Currently, this function simply removes `currIndent` spaces after each `\n` in the input string `docString`.

If/when the `docString` linter expands, it may take on more string processing.

Equations

- Mathlib.Linter.deindentString currIndent docString = docString.replace ('\n' :: List.replicate currIndent ' ').asString " "

Instances For

source
def Mathlib.Linter.Style.docStringLinter :
Lean.Linter

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

Equations

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

Instances For