monadic pipe projection

Stream: lean4

[Scott Morrison]

Is there a monadic version of the pipe projection |>.?

e.g. if I have f : MetaM Expr, I might find myself writing pure (← f).headBeta, but would love to write e.g. f $>.headBeta.

[James Gallicchio]

I've also been wanting something along those lines. It would make some functional-but-with-effects code way more readable

[James Gallicchio]

Let's make a metaphor to C, and have |>-> as the "dereferencing" version of |>. :) [joke]

[Mario Carneiro]

you can do (·.headBeta) <$> f

[Mario Carneiro]

or f <&> (·.headBeta) if you like the argument order