The "docPrime" linter

The "docPrime" linter emits a warning on declarations that have no doc-string and whose name ends with a '. Such declarations are expected to have a documented explanation for the presence of a ' in their name. This may consist of discussion of the difference relative to an unprimed version of that declaration, or an explanation as to why no better naming scheme is possible.

opaque Mathlib.Linter.linter.docPrime : Lean.Option Bool

The "docPrime" linter emits a warning on declarations that have no doc-string and whose name ends with a '.

The file scripts/nolints_prime_decls.txt contains a list of temporary exceptions to this linter. This list should not be appended to, and become emptied over time.

def Mathlib.Linter.DocPrime.docPrimeLinter : Lean.Linter

The "docPrime" linter emits a warning on declarations that have no doc-string and whose name ends with a '.

The file scripts/nolints_prime_decls.txt contains a list of temporary exceptions to this linter. This list should not be appended to, and become emptied over time.

Equations

• One or more equations did not get rendered due to their size.