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

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 " "

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.