Zulip Chat Archive

Stream: Is there code for X?

Topic: list (option α) → list α


view this post on Zulip Johan Commelin (Jul 07 2020 at 14:06):

Do we have a function with signature list (option α) → list α?

view this post on Zulip Simon Hudon (Jul 07 2020 at 14:07):

I think the usual way of doing it is list.map_filter id

view this post on Zulip Johan Commelin (Jul 07 2020 at 14:10):

Ok, I'll try

view this post on Zulip Johan Commelin (Jul 07 2020 at 14:12):

I currently have

def list.remove_none : list (option α)  list α
| []            := []
| (none :: l)   := l.remove_none
| (some a :: l) := a :: l.remove_none

but I guess there is some slick monad combinator 1-liner doing this.

view this post on Zulip Kyle Miller (Jul 07 2020 at 19:00):

@Johan Commelin

def list.remove_none {α : Type*} (m : list (option α)) : list α
:= m >>= option.to_list

(Though this might be annoying since it's the concatenation of 1-element lists.)

view this post on Zulip Rob Lewis (Jul 07 2020 at 19:04):

This is docs#list.reduce_option

view this post on Zulip Kyle Miller (Jul 07 2020 at 19:08):

(For the curious, list.reduce_option is implemented as list.filter_map id, like @Simon Hudon suggested.)

view this post on Zulip Rob Lewis (Jul 07 2020 at 19:12):

Also for the curious, #find is still a good way to answer questions like

Do we have a function with signature list (option α) → list α?

import data.list tactic.find

#find list (option _)  list _

view this post on Zulip Kyle Miller (Jul 07 2020 at 19:13):

This is extremely helpful. I've very much been wanting something like Hoogle!

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:14):

Is it doable to have import all before #find? I mean, all is generated for the linter but it gets cleared away, right?

view this post on Zulip Rob Lewis (Jul 07 2020 at 19:15):

all is generated by scripts/mk_all.sh, so if you run that yourself, you can certainly import all.

view this post on Zulip Rob Lewis (Jul 07 2020 at 19:16):

It makes #find somewhat to much slower, depending on what you're looking for.

view this post on Zulip Rob Lewis (Jul 07 2020 at 19:16):

So I'm not sure it would be good to keep all.lean around and import it from tactic.find.

view this post on Zulip Patrick Massot (Jul 07 2020 at 19:17):

Not that you can leanproject mk-all (in any project, not only mathlib).

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:17):

Definitely not a good idea, you're right

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:17):

Can you?

view this post on Zulip Patrick Massot (Jul 07 2020 at 19:17):

It will create exactly one all.lean, not a swarm of them like the mathlib script.

view this post on Zulip Rob Lewis (Jul 07 2020 at 19:18):

The script hasn't made a swarm for a while now.

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:18):

We could have a find.sh script that gets the all.lean file generated, generate a lean file that imports it with #find my stuff and then run Lean on it

view this post on Zulip Rob Lewis (Jul 07 2020 at 19:20):

Then #find is unusable anywhere except a leaf file of mathlib.

view this post on Zulip Rob Lewis (Jul 07 2020 at 19:21):

We're definitely missing proper lemma search, but I don't think hacking around #find is a reliable solution.

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:21):

I wouldn't put that as part of find

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:22):

You leave #find the way it is and, in addition to that user command, there's a shell (or python) script that you can call with your query and that will consider all your code base

view this post on Zulip Rob Lewis (Jul 07 2020 at 19:23):

Ah, I see. But you still need a fully compiled mathlib for it to be usable, or you need to be willing to wait a long time!

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:26):

Exactly

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:47):

I think we need to get used to the fact that you should always have a clean copy of mathlib next to the copy that you are hacking on...

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:47):

Btw, thanks for finding this for me.


Last updated: May 17 2021 at 15:13 UTC