Combinator/Functor/? Land

Stream: new members

[Marcus Rossel]

I'm trying to prove a lemma that involves zip_with. Along the way I used list.nth_zip_with, which introduced symbols like <$>, <*>, and >>= into my goal state.
Now I'm completely unable to understand what the goal means.
Clicking the symbols tells me what they are, but looking them up in the docs did not help me understand them at all.
Is there a way to circumnavigate these kinds of expressions, or is there a resource that explains them?
Thanks :)

[Mario Carneiro]

<$> is list.map, and >>= is list.bind; <*> is another function with its own definition in terms of map and bind

[Mario Carneiro]

you can rewrite them away using list.map_eq_map and list.bind_eq_bind and (<*>) IIRC

[Scott Morrison]

Also see https://leanprover-community.github.io/extras/tactic_writing.html#marios-monadic-symbols-cheat-sheet

[Bryan Gin-ge Chen]

It doesn't always help, but you can often use something like #print notation <$> to figure out what some symbols mean.