Conflicting (?) Abs instances

Stream: mathlib4

[Junyan Xu]

Why are docs#Neg.toHasAbs and docs#Inv.toHasAbs both instances, and why didn't they lead to trouble for ordered fields? The multiplicative one probably shouldn't be an instance?

Does to_additive not transfer the (priority := 100) so Neg.toHasAbs gets normal priority?

[Yaël Dillies]

because @Johan Commelin asked for absolute values to be multiplicativised and we didn't have the heart to tell him it was a bad idea.

[Johan Commelin]

If I ever pushed for the multiplicative version of the instance, then I apologize.
I thought there was separate notation for multiplicative absolute values, but now I don't see it.

[Johan Commelin]

There used to be

/-- `mabs a` is the multiplicative absolute value of `a`. -/
@[to_additive abs
"`abs a` is the additive absolute value of `a`."
]
def mabs {α : Type*} [has_inv α] [lattice α] (a : α) : α := a ⊔ (a⁻¹)

And then in https://github.com/leanprover-community/mathlib/pull/9172/files#diff-3e069267e91f1c9fa57363bce4331f584ef26260c60a7801494d2889b733a866 it was turned into a notation typeclass. I merged that PR, and clearly I forgot to think about the conflict that it introduced.

[Johan Commelin]

I think mabs is not necessarily bad. But certainly it shouldn't have been turned into |.| notation.

[Yaël Dillies]

Anyway I have a full rewrite of the files in question coming up, so don't worry too much about it.

[Junyan Xu]

#7976 is generalizing some stuff about Abs.

Does to_additive not transfer the (priority := 100) so Neg.toHasAbs gets normal priority?

Returning to this question: how do I find out the priority of an instance?