All but last element of a list

Stream: Is there code for X?

[Chris Hughes]

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

[Reid Barton]

src#list.init

[Kevin Buzzard]

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]

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

[Reid Barton]

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]

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]

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]

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.