# 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.