Default linters #
User commands to spot common mistakes in the code
#lint: check all declarations in the current file
#lint_mathlib: check all declarations in mathlib (so excluding core or other projects, and also excluding the current file)
#lint_all: check all declarations in the environment (the current file and all imported files)
The following linters are run by default:
unused_argumentschecks for unused arguments in declarations.
def_lemmachecks whether a declaration is incorrectly marked as a def/lemma.
dup_namespcechecks whether a namespace is duplicated in the name of a declaration.
ge_or_gtchecks whether ≥/> is used in the declaration.
instance_prioritychecks that instances that always apply have priority below default.
doc_blamechecks for missing doc strings on definitions and constants.
has_nonempty_instancechecks whether every type has an associated
impossible_instancechecks for instances that can never fire.
incorrect_type_class_argumentchecks for arguments in [square brackets] that are not classes.
dangerous_instancechecks for instances that generate type-class problems with metavariables.
fails_quicklytests that type-class inference ends (relatively) quickly when applied to variables.
has_coe_variabletests that there are no instances of type
has_coe α tfor a variable
inhabitedinstance arguments that should be changed to
simp_nfchecks that the left-hand side of simp lemmas is in simp-normal form.
simp_var_headchecks that there are no variables as head symbol of left-hand sides of simp lemmas.
simp_commchecks that no commutativity lemmas (such as
add_comm) are marked simp.
decidablehypotheses that are used in the proof of a proposition but not in the statement, and could be removed using
classical. Theorems in the
decidablenamespace are exempt.
has_coe_to_funchecks that every type that coerces to a function has a direct
check_typechecks that the statement of a declaration is well-typed.
check_univschecks that there are no bad
max u vuniverse levels.
syn_tautchecks that declarations are not syntactic tautologies.
check_reducibilitychecks whether non-instances with a class as type are reducible.
unprintable_interactivechecks that interactive tactics have parser documentation.
to_additive_docchecks if additive versions of lemmas have documentation.
The following linters are not run by default:
doc_blame_thm, checks for missing doc strings on lemmas and theorems.
explicit_vars_of_iffchecks if there are explicit variables used on both sides of an iff.
#list_linters prints a list of the names of all available linters.
You can append a
* to any command (e.g.
#lint_mathlib*) to omit the slow tests (4).
You can append a
- to any command (e.g.
#lint_mathlib-) to run a silent lint
that suppresses the output if all checks pass.
A silent lint will fail if any test fails.
You can append a
+ to any command (e.g.
#lint_mathlib+) to run a verbose lint
that reports the result of each linter, including the successes.
You can append a sequence of linter names to any command to run extra tests, in addition to the
default ones. e.g.
#lint doc_blame_thm will run all default tests and
You can append
only name1 name2 ... to any command to run a subset of linters, e.g.
#lint only unused_arguments
You can add custom linters by defining a term of type
linter in the
A linter defined with the name
linter.my_new_check can be run with
lint only my_new_check.
If you add the attribute
linter.my_new_check it will run by default.
Adding the attribute
@[nolint doc_blame unused_arguments] to a declaration
omits it from only the specified linter checks.