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
@[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
    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
        Instances For
          source
          def Mathlib.Linter.Style.docStringLinter :
          Lean.Linter

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

          Equations
            Instances For