Setoid as a typeclass

Stream: mathlib4

[Yury G. Kudryashov]

Hi, I suggest that we change all Setoid _ instances to non-instances and completely migrate away from the instance API.

[Yury G. Kudryashov]

First in Mathlib, then ask core team what they think about turning it into a structure so that docs#Setoid.r works fine with dot notation and is pretty printed as Setoid.r s or s.r, not Setoid.r (no arguments).

[Yuyang Zhao]

There are some related refactoring attempts in #16210, but none of the PRs have been merged.

[Eric Wieser]

Yury G. Kudryashov said:

hen ask core team what they think about turning it into a structure so that docs#Setoid.r works fine with dot notation and is pretty printed as Setoid.r s or s.r, not Setoid.r (no arguments).

We could also use docs#Setoid.Rel, which prints in the way you want

[Yuyang Zhao]

#16254 (one of the PRs) would immediately resolve the problem of pretty-printing Setoid.r.

[Eric Wieser]

If we do that then we can probably follow on by dropping Rel

[Yury G. Kudryashov]

#16260 deprecates Rel

[Yury G. Kudryashov]

BTW, I've just delegated #16254

[Yury G. Kudryashov]

Are there other leaf PRs in this refactor?

[Yuyang Zhao]

#16256 #16258 #16260 #16267 are ready.

[Yuyang Zhao]

I'm a little hesitant to change instance parameters to implicit parameters now. If we decide to migrate to QuotLike, we may not have to change these parameters. However, the API in core has been changed and there is not much to fix in these PRs.

[Yury G. Kudryashov]

I think that cleaning up is a good thing anyway.

[Yuyang Zhao]

#16260 #17594 are ready.

[Yuyang Zhao]

#16264 #16410 #17940 #17941 are ready.

[Yuyang Zhao]

#16314 is ready.