## Stream: Is there code for X?

### Topic: list (option α) → list α

#### Johan Commelin (Jul 07 2020 at 14:06):

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

#### Simon Hudon (Jul 07 2020 at 14:07):

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

Ok, I'll try

#### 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.

#### 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.)

#### Rob Lewis (Jul 07 2020 at 19:04):

This is docs#list.reduce_option

#### 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.)

#### 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 _


#### Kyle Miller (Jul 07 2020 at 19:13):

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

#### 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?

#### 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.

#### Rob Lewis (Jul 07 2020 at 19:16):

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

#### 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.

#### Patrick Massot (Jul 07 2020 at 19:17):

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

#### Simon Hudon (Jul 07 2020 at 19:17):

Definitely not a good idea, you're right

Can you?

#### Patrick Massot (Jul 07 2020 at 19:17):

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

#### Rob Lewis (Jul 07 2020 at 19:18):

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

#### 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

#### Rob Lewis (Jul 07 2020 at 19:20):

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

#### 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.

#### Simon Hudon (Jul 07 2020 at 19:21):

I wouldn't put that as part of find

#### 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

#### 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!

Exactly

#### 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...

#### Johan Commelin (Jul 07 2020 at 19:47):

Btw, thanks for finding this for me.

Last updated: May 17 2021 at 15:13 UTC