The tacticDocs linter

The tacticDocs environment linter checks that all tactics defined in a module come with a (nonempty) docstring.

def tacticDocs : Batteries.Tactic.Lint.Linter

Check that all tactics available in Mathlib have a docstring.

Equations

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