argument order of Or.elim

Stream: mathlib4

[David Renshaw]

@Mario Carneiro is there a reason that Or.elim in mathlib4 changes the argument order compared to Lean 3?

https://github.com/leanprover-community/mathlib4/blob/7822926636f86c197bf3b9d14b4ad3b4a34701a1/Mathlib/Logic/Basic.lean#L59
vs
https://github.com/leanprover-community/lean/blob/737ec95b34cbff36e49ac76a61b44f314bd57bd1/library/init/logic.lean#L205

[Jakob von Raumer]

Shouldn't the one with the order of the lean3 one be called elim_on/elimOn?

[David Renshaw]

by analogy to rec?

[David Renshaw]

that makes sense to me

[Mario Carneiro]

I don't have any memory of that, but it seems worth a backport if it's not too terrible

[Mario Carneiro]

but if the fallout is too much a forward port would also be fine