Various linters
This file defines several small linters:
ge_or_gtchecks that>and≥do not occur in the statement of theorems.dup_namespacechecks that no declaration has a duplicated namespace such aslist.list.monad.unused_argumentschecks that definitions and theorems do not have unused arguments.doc_blamechecks that every definition has a documentation stringdoc_blame_thmchecks that every theorem has a documentation string (not enabled by default)def_lemmachecks 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.