Documentation

Mathlib.Tactic.Linter.DocString

The "DocString" style linter #

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

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

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

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

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

source
🔸 coverage
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.

source
🔸 coverage
@[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.

Instances For