# Documentation

Std.Tactic.Lint.Misc

# Various linters #

This file defines several small linters.

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

Equations
• One or more equations did not get rendered due to their size.

A linter for checking for unused arguments. We skip all declarations that contain sorry in their value.

Equations
• One or more equations did not get rendered due to their size.

A linter for checking definition doc strings.

Equations
• One or more equations did not get rendered due to their size.

A linter for checking theorem doc strings.

Equations
• One or more equations did not get rendered due to their size.

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

Equations
• One or more equations did not get rendered due to their size.

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

Equations
• One or more equations did not get rendered due to their size.

A linter for checking that there are no bad max u v universe levels. 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 α.

Equations
• One or more equations did not get rendered due to their size.

A linter for checking that declarations aren't syntactic tautologies. Checks whether a lemma is a declaration of the form ∀ a b ... z, e₁ = e₂∀ 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.

Equations
• One or more equations did not get rendered due to their size.

Return a list of unused have/suffices/let_fun terms in an expression. This actually finds all beta-redexes.

Equations
• One or more equations did not get rendered due to their size.

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

Equations
• One or more equations did not get rendered due to their size.

A linter for checking if variables appearing on both sides of an iff are explicit. Ideally, such variables should be implicit instead.

Equations
• One or more equations did not get rendered due to their size.