Documentation

Mathlib.Tactic.Linter.DocString

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
partial 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.