Zulip Chat Archive

Stream: new members

Topic: Combinator/Functor/? Land

view this post on Zulip Marcus Rossel (Mar 09 2021 at 20:09):

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 :)

view this post on Zulip Mario Carneiro (Mar 09 2021 at 20:16):

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

view this post on Zulip Mario Carneiro (Mar 09 2021 at 20:17):

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

view this post on Zulip Scott Morrison (Mar 09 2021 at 22:23):

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

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 22:25):

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

Last updated: May 13 2021 at 19:20 UTC