A linter for checking whether illegal constants (≥, >) appear in a declaration's type.

A linter for checking whether a declaration has a namespace twice consecutively in its name.

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.

A linter for checking definition doc strings

A linter for checking theorem doc strings. This is not in the default linter set.

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

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

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

univ_params_grouped e computes for each level u of e the parameters that occur in u, and returns the corresponding set of lists of parameters. In pseudo-mathematical form, this returns { { p : parameter | p ∈ u } | (u : level) ∈ e } We use list name instead of name_set, since name_set does not have an order. It will ignore nm₀._proof_i declarations.

The good parameters are the parameters that occur somewhere in the rb_set as a singleton or (recursively) with only other good parameters. All other parameters in the rb_set are bad.

Checks whether all universe levels u in the type of d are "good". This means that u either occurs in a level of d by itself, or (recursively) with only other good levels. When this fails, usually this means that there is a level max u v, where neither u nor v occur by themselves in a level. It is ok if one of u or v never occurs alone. For example, (α : Type u) (β : Type (max u v)) is a occasionally useful method of saying that β lives in a higher universe level than α.

A linter for checking that there are no bad max u v universe levels.

Checks whether a lemma is a declaration of the form ∀ a b ... z, e₁ = e₂ where e₁ and e₂ are identical exprs. We call declarations of this form syntactic tautologies. Such lemmas are (mostly) useless and sometimes introduced unintentionally when proving basic facts with rfl when elaboration results in a different term than the user intended.

A linter for checking that declarations aren't syntactic tautologies.

Check if an expression contains var 0 by folding over the expression and matching the binder depth

Return a list of unused have and suffices terms in an expression

Return a list of unused have and suffices terms in a declaration

Checks whether a declaration contains term mode have statements that have no effect on the resulting term.

A linter for checking that declarations don't have unused term mode have statements. We do not tag this as @[linter] so that it is not in the default linter set as it is slow and an uncommon problem.