Various linters
This file defines several small linters:
ge_or_gt
checks that>
and≥
do not occur in the statement of theorems.dup_namespace
checks that no declaration has a duplicated namespace such aslist.list.monad
.unused_arguments
checks that definitions and theorems do not have unused arguments.doc_blame
checks that every definition has a documentation stringdoc_blame_thm
checks that every theorem has a documentation string (not enabled by default)def_lemma
checks that a declaration is a lemma iff its type is a proposition.
Linter against use of >
/≥
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 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.