SignType.sign vs Real.sign

Stream: mathlib4

[Yury G. Kudryashov]

We have docs#SignType.sign and docs#Real.sign. Should we deduplicate?

[Yury G. Kudryashov]

(and expand API about SignType.sign if needed)

[Yaël Dillies]

and docs#Int.sign

[Yaël Dillies]

And yes please do! I tried deduplicating SignType.sign and Int.sign before but didn't get to the end.

[Yury G. Kudryashov]

I'll open an issue for now.

[Eric Wieser]

Yaël Dillies said:

And yes please do! I tried deduplicating SignType.sign and Int.sign before but didn't get to the end.

This is now much harder because the latter is in Std and the former in mathlib

[Eric Wieser]

But we can at least lose Real.sign without that problem

[Scott Morrison]

Yes, we won't be able to get rid of Int.sign because it is extensively used in programming and so needs to be there directly, not mediated by a typeclass.

[Eric Wieser]

If we relaxed PreOrder to LT on docs#SignType.sign then I don't see the typeclasses being an obstacle for Std