Various linters

This file defines several small linters.

def Batteries.Tactic.Lint.dupNamespace : Linter

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.

def Batteries.Tactic.Lint.unusedArguments : Linter

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.

def Batteries.Tactic.Lint.docBlame : Linter

A linter for checking definition doc strings.

Equations

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

def Batteries.Tactic.Lint.docBlameThm : Linter

A linter for checking theorem doc strings.

Equations

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

def Batteries.Tactic.Lint.defLemma : Linter

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.

def Batteries.Tactic.Lint.checkType : Linter

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

Equations

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

def Batteries.Tactic.Lint.checkUnivs : Linter

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.

def Batteries.Tactic.Lint.synTaut : Linter

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

def Batteries.Tactic.Lint.findUnusedHaves : Lean.Expr → Lean.MetaM (Array Lean.MessageData)

Return a list of unused let_fun terms in an expression that introduce proofs.

Equations

• Batteries.Tactic.Lint.findUnusedHaves x✝ = pure #[]

def Batteries.Tactic.Lint.unusedHavesSuffices : Linter

A linter for checking that declarations don't have unused term mode have statements.

Equations

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

def Batteries.Tactic.Lint.explicitVarsOfIff : Linter

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.