Topic: lower instance priority
Yuyang Zhao (Nov 16 2022 at 12:29):
Why docs#ordered_cancel_comm_monoid.to_contravariant_class_le_left has priority 200 but docs#ordered_cancel_comm_monoid.to_contravariant_class_left and docs#ordered_cancel_comm_monoid.to_contravariant_class_right has normal priority?
Yaël Dillies (Nov 16 2022 at 13:11):
git blaming will probably give you the answer
Yuyang Zhao (Nov 16 2022 at 17:41):
#17571 Seems it can have the normal priority.
Sebastien Gouezel (Nov 16 2022 at 17:50):
Do you have a good reason for this change? I mean, there is probably a (at least heuristic) performance reason if the priority is not standard, so one should check throughly that the change does not have a performance penalty
Yuyang Zhao (Nov 16 2022 at 18:14):
This instance is added in PR #16445. Seems there is no reason to make its priority different from the other 2.
Yaël Dillies (Nov 16 2022 at 18:15):
I remember following the priority from another instance.
Yuyang Zhao (Nov 16 2022 at 18:17):
Maybe the priority of the other two instances should be lowered too?
Last updated: Aug 03 2023 at 10:10 UTC