hoogle/search

Stream: new members

[Nathan Ringo]

Is there a way to search for items by type?

[Alex J. Best]

There is the tactic library_search to search for anything matching the current goal, and also #find, e.g. #find (_ : nat) + _ = _ + _

[Nathan Ringo]

okay, thanks!

[Nathan Ringo]

er, do I need to do anything special for #find? I get error: command expected

[Alex J. Best]

One of the examples from hoogle is finding the map function, here is the equivalent with library search

variables (α β : Type*)
def what_is_this  : (α → β) → list α → list β := by library_search -- output: exact list.map

[Nathan Ringo]

er, I'm getting unknown identifier 'library_search' -- are we using different versions of Lean? (I'm at 3.4.2)

[Alex J. Best]

Its a mathlib function sorry, you will need to install mathlib (if you havent already) and import it into your lean file.

[Alex J. Best]

https://github.com/leanprover-community/mathlib

[Alex J. Best]

Importing library search is then import tactic.library_search

[Nathan Ringo]

okay, looks like that worked; thanks!

[Alex J. Best]

You can also set set_option trace.library_search true to see a list of all possible results, but then you get quite a few more than you want then.

[Bryan Gin-ge Chen]

#find is also part of mathlib, so you have to import tactic.find for that to work.