## Stream: general

### Topic: duplicate instance linter

#### Kenny Lau (Jul 14 2020 at 04:03):

Do we need a duplicate instance linter or is the linter sufficiently slow already?

#### Kenny Lau (Jul 14 2020 at 04:03):

Because this happened in data.polynomial:

 instance algebra_of_algebra : algebra R (polynomial A) := add_monoid_algebra.algebra

[...]

instance algebra' (R : Type u) [comm_semiring R] (A : Type v) [semiring A] [algebra R A] :
algebra R (polynomial A) :=
{ smul := λ r p, algebra_map R A r • p,
commutes' := λ c p, ext \$ λ n,
show (C (algebra_map R A c) * p).coeff n = (p * C (algebra_map R A c)).coeff n,
by rw [coeff_C_mul, coeff_mul_C, algebra.commutes],
smul_def' := λ c p, (C_mul' _ _).symm,
.. C.comp (algebra_map R A) }


#### Johan Commelin (Jul 14 2020 at 04:35):

Good catch! I think we can run another linter. When you lint 1 file, it takes a noticeable amount of seconds, but it's not too bad. When you lint the entire project, in CI, this is something you can parallelize, so adding an extra linter doesn't hurt.

Last updated: May 12 2021 at 03:23 UTC