data/option: add map

[semorrison]

No description provided.

[gebner]

Note that option already has a monad instance, so you can write f <$> x to map a function f over an option x.

[semorrison]

Thanks. I guess discard this or merge, depending on how much stylistic flexibility you want to encourage! (I personally like words-over-symbols, and also like the "build this thing, then process it" style that o.map(f) reads as, but of course it's not a big deal.)

…

On Sun, Sep 3, 2017 at 12:07 AM Gabriel Ebner ***@***.***> wrote: Note that option already has a monad instance, so you can write f <$> x to map a function f over an option x. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#12 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAdLBH3463_OpoSt7NbrE5NPt__6H1jlks5seWEHgaJpZM4PK5js> .

[digama0]

@gebner Actually, I thought I already added this (under the name option_map) in init/data/option/basic.lean. It is not the same as <$> because that notation only works on the same universe. Then again Scott's definition here also only works on the same universe, so I don't see any reason to accept this PR as stated.

[semorrison]

I allowed option.map to change universes.

[digama0]

Now it is the same as option_map, so I still don't see the point. I will PR lean repo to change option_map to option.map, and if that fails I will make an alias here.