mathlib3 documentation

tactic.lint.misc

Various linters #

This file defines several small linters:

Linter against use of >/ #

meta def linter.ge_or_gt  :

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

Currently, the linter forbids the use of > and in definitions and statements, as they cause problems in rewrites. They are still allowed in statements such as bounded (≥) or ∀ ε > 0 or ⨆ n ≥ m, and the linter allows that. If you write a pattern where you bind two or more variables, like ∃ n m > 0, the linter will flag this as illegal, but it is also allowed. In this case, add the line

@[nolint ge_or_gt] -- see Note [nolint_ge]

Linter for duplicate namespaces #

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

Linter for unused arguments #

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.

Linter for documentation strings #

meta def linter.doc_blame  :

A linter for checking definition doc strings

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

Linter for correct usage of lemma/def #

meta def linter.def_lemma  :

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

Linter that checks whether declarations are well-typed #

meta def check_type (d : declaration) :

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

meta def linter.check_type  :

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

Linter for universe parameters #

meta def expr.univ_params_grouped (e : expr) (nm₀ : name) :

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

meta def linter.check_univs  :

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

Linter for syntactic tautologies #

meta def syn_taut (d : declaration) :

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.

meta def linter.syn_taut  :

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

Linters for ineffectual have and suffices statements in term mode #

meta def expr.has_zero_var (e : expr) :

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.

Linter for unprintable interactive tactics #

Ensures that every interactive tactic has arguments for which interactive.param_desc succeeds. This is used to generate the parser documentation that appears in hovers on interactive tactics.

A linter for checking that interactive tactics have parser documentation.

Linter for iff's #

Recursively consumes a Pi expression while accumulating names and the complement of de-Bruijn indexes of explicit variables, ultimately obtaining the remaining non-Pi expression as well.

This function works as follows:

  1. Call unravel_explicits_of_pi to obtain the names, complements of de-Bruijn indexes and the remaining non-Pi expression;
  2. Check if the remaining non-Pi expression is an iff, already obtaining the respective left and right expressions if this is the case. Returns none otherwise;
  3. Filter the explicit variables that appear on the left and right side of the iff;
  4. If no variable satisfies the condition above, return none;
  5. Return a message mentioning the variables that do, otherwise.

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