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
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.
Instances For