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.

def tacticAlt : Batteries.Tactic.Lint.Linter

Check tactics with the same user-facing name (usually: first syntax token) get a @[tactic_alt] attribute.

Equations

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