Various linters #
This file defines several small linters:
≥do not occur in the statement of theorems.
dup_namespacechecks that no declaration has a duplicated namespace such as
unused_argumentschecks that definitions and theorems do not have unused arguments.
doc_blamechecks that every definition has a documentation string.
doc_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.
check_typechecks that the statement of a declaration is well-typed.
Linter against use of
Linter for duplicate namespaces #
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).