Zulip Chat Archive

Stream: general

Topic: duplicate instance linter


view this post on Zulip Kenny Lau (Jul 14 2020 at 04:03):

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

view this post on Zulip 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) }

view this post on Zulip 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