mathlib3 documentation

meta def linter.ge_or_gt :

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

def library_note.nolint_ge :

unit

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 #

meta def linter.dup_namespace :

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

Linter for unused arguments #

meta def check_unused_arguments (d : declaration) :

option (list ℕ)

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

meta def linter.unused_arguments :

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

meta def linter.doc_blame_thm :

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) :

native.rb_set (list 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.

meta def bad_params :

native.rb_set (list name) → list name

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) :

bool

Check if an expression contains var 0 by folding over the expression and matching the binder depth

meta def find_unused_have_suffices_macros :

expr → tactic (list string)

Return a list of unused have and suffices terms in an expression

meta def unused_have_of_decl :

declaration → tactic (list string)

Return a list of unused have and suffices terms in a declaration

meta def has_unused_haves_suffices (d : declaration) :

Checks whether a declaration contains term mode have statements that have no effect on the resulting term.

meta def linter.unused_haves_suffices :

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 #

meta def unprintable_interactive (d : declaration) :

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.

meta def linter.unprintable_interactive :

A linter for checking that interactive tactics have parser documentation.

Linter for iff's #

meta def unravel_explicits_of_pi :

expr → ℕ → list name → list ℕ → list name × list ℕ × 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:

Call unravel_explicits_of_pi to obtain the names, complements of de-Bruijn indexes and the remaining non-Pi expression;
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;
Filter the explicit variables that appear on the left and right side of the iff;
If no variable satisfies the condition above, return none;
Return a message mentioning the variables that do, otherwise.

meta def linter.explicit_vars_of_iff :