mathlib documentation


Linters about type classes #

This file defines several linters checking the correct usage of type classes and the appropriate definition of instances:

A linter object for checking instance priorities of instances that always apply. This is in the default linter set.

A linter for missing inhabited instances.

A linter object for impossible_instance.

A linter object for incorrect_type_class_argument.

A linter object for dangerous_instance.

Applies expression e to local constants, but lifts all the arguments that are Sort-valued to Type-valued sorts.

meta def fails_quickly (max_steps : ) (d : declaration) :

Tests whether type-class inference search for a class will end quickly when applied to variables. This tactic succeeds if mk_instance succeeds quickly or fails quickly with the error message that it cannot find an instance. It fails if the tactic takes too long, or if any other error message is raised. We make sure that we apply the tactic to variables living in Type u instead of Sort u, because many instances only apply in that special case, and we do want to catch those loops.

A linter object for fails_quickly. If we want to increase the maximum number of steps type-class inference is allowed to take, we can increase the number 3000 in the definition. As of 5 Mar 2020 the longest trace (for is_add_hom) takes 2900-3000 "heartbeats".

A linter object for class_structure.

A linter object for has_coe_variable.

A linter object for inhabited_nonempty.

A linter object for decidable_classical.

Linter that checks whether has_coe_to_fun instances comply with Note [function coercion].