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, and allow arguments starting with _ to be unused.

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.

This linter is disabled by default: declarations are already type-checked when added to the environment, so re-checking every statement is redundant in normal use. As an alternative defence-in-depth measure for catching kernel/elaborator bugs, prefer running an external checker such as lean4checker or trepplein.

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.