mathlib documentation

tactic.​lint.​misc

tactic.​lint.​misc

Various linters

This file defines several small linters:

Linter against use of >/

meta def linter.​ge_or_gt  :

A linter for checking whether illegal constants (≥, >) appear in a declaration's type.

Linter for duplicate namespaces

A linter for checking whether a declaration has a namespace twice consecutively in its name.

Linter for unused arguments

Check which arguments of a declaration are not used. Prints a list of natural numbers corresponding to which arguments are not used (e.g. this outputs [1, 4] if the first and fourth arguments are unused). Checks both the type and the value of d for whether the argument is used (in rare cases an argument is used in the type but not in the value). We return [] if the declaration was automatically generated. We print arguments that are larger than the arity of the type of the declaration (without unfolding definitions).

A linter object for checking for unused arguments. This is in the default linter set.

Linter for documentation strings

A linter for checking definition doc strings

A linter for checking theorem doc strings. This is not in the default linter set.

Linter for correct usage of lemma/def

A linter for checking whether the correct declaration constructor (definition or theorem) has been used.