Zulip Chat Archive
Stream: mathlib4
Topic: Duplicate algebraic instance for `Shrink`
Yury G. Kudryashov (May 01 2025 at 06:00):
We have, e.g., docs#Equiv.instOneShrink and docs#instOneShrink
Yury G. Kudryashov (May 01 2025 at 06:01):
CC: @Kim Morrison
Yury G. Kudryashov (May 01 2025 at 06:13):
(you've authored one of the copies)
Kim Morrison (May 06 2025 at 03:53):
Yes, of course we should deduplicate.
Yury G. Kudryashov (May 06 2025 at 03:54):
Do you have time to do this?
Kim Morrison (May 06 2025 at 07:37):
No. :-)
Last updated: Dec 20 2025 at 21:32 UTC