Stream: Is there code for X?
Chris Hughes (Jul 18 2020 at 12:28):
What's the easiest way to take all but the last element of a list?
Reid Barton (Jul 18 2020 at 12:30):
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
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