mathlib

1710fd8b - feat(lint): add priority test for instances that always apply (#1625)

feat(lint): add priority test for instances that always apply (#1625) * feat(lint): add priority test for instances that always apply also move a defn from coinductive_predicates to expr also slightly refactor incorrect_def_lemma * update doc * add priorities to linters Now they are run in the order specified by the doc * always run tests in the extra set even when they are slow and is false * move some more declarations from coinductive_predicates to expr remove coinductive_predicates as import from some (but not all) files * reviewer comments * remove unsafe prefixes