## Stream: Is there code for X?

### Topic: All but last element of a list

#### Chris Hughes (Jul 18 2020 at 12:28):

What's the easiest way to take all but the last element of a list?

src#list.init

#### Kevin Buzzard (Jul 18 2020 at 13:49):

Is human-powered library search (i.e. this stream) the only way to search for this, if you don't know the name? Would this also be the case for Coq/Agda/IsabelleHOL etc?

#### Jalex Stark (Jul 18 2020 at 13:52):

if it had a docstring, then it would not be hard to find by reading list/basic.lean

#### Reid Barton (Jul 18 2020 at 13:52):

In this case you can go to https://hoogle.haskell.org/?hoogle=[a]%20-%3E%20[a] and see it is the second result, then guess the Lean name is the same

#### Kevin Buzzard (Jul 18 2020 at 13:56):

Right, so occasionally people come here asking for Lean's version of hoogle. It is supposed to be #find but the output of #find list _ → list _  is over 100 lines long, contains plenty of things not of type list X -> list X (e.g. list.join : list (list X) -> list X), and init is is nearly 50 lines down.

#### Kevin Buzzard (Jul 18 2020 at 13:57):

Hoogle's output is much more controlled because (if my understanding is correct) it's only giving us list X -> list X and I don't know how to restrict #find in this way.

#### Floris van Doorn (Jul 18 2020 at 18:54):

Probably sorting the output of #find using some stupid heuristics (for example: shortest type, counting the number of characters in its string when printed) would already help.

Last updated: May 07 2021 at 23:11 UTC