list (option α) → list α

Stream: Is there code for X?

[Johan Commelin]

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

[Simon Hudon]

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

[Johan Commelin]

Ok, I'll try

[Johan Commelin]

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]

@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]

This is docs#list.reduce_option

[Kyle Miller]

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

[Rob Lewis]

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]

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

[Simon Hudon]

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]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Patrick Massot]

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

[Simon Hudon]

Definitely not a good idea, you're right

[Simon Hudon]

Can you?

[Patrick Massot]

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

[Rob Lewis]

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

[Simon Hudon]

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]

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

[Rob Lewis]

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

[Simon Hudon]

I wouldn't put that as part of find

[Simon Hudon]

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]

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!

[Simon Hudon]

Exactly

[Johan Commelin]

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]

Btw, thanks for finding this for me.