mathlib documentation


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 #

meta def linter.doc_blame  :

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 #

meta def linter.def_lemma  :

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

meta def check_type (d : declaration) :

Checks whether the statement of a declaration is well-typed.

meta def linter.check_type  :

A linter for missing checking whether statements of declarations are well-typed.