Documentation

Mathlib.Tactic.Linter.TacticDocumentation

The tacticDocs linter #

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

source
🔸 coverage
def tacticDocs :
Batteries.Tactic.Lint.Linter

Check that all tactics available in Mathlib have a docstring.

Equations
    Instances For