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.