andThen vs seqRight

Stream: lean4

[Eric Wieser]

Are the operations f >> g and f *> g the same? docs#AndThen doesn't seem to have many instances.

[Mario Carneiro]

cc: @Sebastian Ullrich who probably remembers the history here better than me. I believe that the fact of the matter is that they are identical in behavior, but I'm unsure if there is a preference for one over the other

[François G. Dorais]

Probably not true (nor very relevant) in practice: >> is derived from monad >>= but *> is derived from appicative <*>.

[Eric Wieser]

I don't think that's true, >> seems not to be available at all on most monads

[Sebastian Ullrich]

We rather use it when a type is not even an Applicative because e.g. it is monomorphic