Zulip Chat Archive

Stream: Is there code for X?

Topic: All but last element of a list


view this post on Zulip Chris Hughes (Jul 18 2020 at 12:28):

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

view this post on Zulip Reid Barton (Jul 18 2020 at 12:30):

src#list.init

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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