tactic.lint.misc

# Various linters #

This file defines several small linters:

• ge_or_gt checks that > and ≥ do not occur in the statement of theorems.
• dup_namespace checks that no declaration has a duplicated namespace such as list.list.monad.
• unused_arguments checks that definitions and theorems do not have unused arguments.
• doc_blame checks that every definition has a documentation string.
• doc_blame_thm checks that every theorem has a documentation string (not enabled by default).
• def_lemma checks that a declaration is a lemma iff its type is a proposition.
• check_type checks that the statement of a declaration is well-typed.
• check_univs checks that there are no bad max u v universe levels.
• syn_taut checks that declarations are not syntactic tautologies.
• unused_haves_suffices checks that declarations produced via term mode do not have ineffectual have or suffices statements

## Linter against use of >/≥#

meta def linter.ge_or_gt  :

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

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

meta def check_univs (d : declaration) :

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

meta def unused_have_of_decl  :

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 #

meta def unravel_explicits_of_pi  :
expr

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.

meta def explicit_vars_of_iff (d : declaration) :

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.