Missing Lean 4 defs

Stream: mathlib4

[Arien Malec]

After some digging, I'm dependent on a notation for $> that used to be in Lean 3, tagged to functor.map_const_rev that used to be in init.control.functor & this is used all over the place in mathlib

[Mario Carneiro]

ok so add it like infix " $> " => Functor.mapConstRev

[Arien Malec]

which is also missing.

[Arien Malec]

pretty trivial to def tho.

[Arien Malec]

Should we add it to mathlib, or upstream?

[Arien Malec]

Looks like @Ruben Van de Velde did this in place.

[Ruben Van de Velde]

Yeah, should still move it somewhere, probably. Let's keep it in mathlib, though

[Arien Malec]

Probably should move to Control.Functor, yeah?

[Arien Malec]

I think we also want the notation, or else lots of downstream stuff in mathlib will break.

[Arien Malec]

I'll do a mini-PR for this...

[Ruben Van de Velde]

I also moved it in mathlib4#803, but feel free to do it separately if you prefer

[Arien Malec]

easier your way...