Linters about type classes #
This file defines several linters checking the correct usage of type classes and the appropriate definition of instances:
instance_priorityensures that blanket instances have low priority.
has_inhabited_instanceschecks that every type has an
impossible_instancechecks that there are no instances which can never apply.
incorrect_type_class_argumentchecks that only type classes are used in instance-implicit arguments.
dangerous_instancechecks for instances that generate subproblems with metavariables.
fails_quicklychecks that type class resolution finishes quickly.
class_structurechecks that every
classis a structure, i.e.
@[class] defis forbidden.
has_coe_variablechecks that there is no instance of type
has_coe α t.
[inhabited α]arguments could be generalized to
decidable_classicalchecks propositions for
[decidable_... p]hypotheses that are not used in the statement, and could thus be removed by using
classicalin the proof.
linter.has_coe_to_funchecks whether necessary
has_coe_to_funinstances are declared.
linter.check_reducibilitychecks whether non-instances with a class as type are reducible.