Documentation

Mathlib.Tactic.Linter.DocString

The "DocString" style linter #

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

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

@[irreducible]

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
      def Mathlib.Linter.deindentString (currIndent : Nat) (docString : 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

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

          Equations
            Instances For