Zulip Chat Archive

Stream: new members

Topic: hoogle/search


view this post on Zulip Nathan Ringo (Aug 09 2019 at 03:43):

Is there a way to search for items by type?

view this post on Zulip Alex J. Best (Aug 09 2019 at 03:47):

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

view this post on Zulip Nathan Ringo (Aug 09 2019 at 03:49):

okay, thanks!

view this post on Zulip Nathan Ringo (Aug 09 2019 at 03:50):

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

view this post on Zulip Alex J. Best (Aug 09 2019 at 03:53):

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

view this post on Zulip Nathan Ringo (Aug 09 2019 at 03:55):

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

view this post on Zulip Alex J. Best (Aug 09 2019 at 03:57):

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

view this post on Zulip Alex J. Best (Aug 09 2019 at 03:57):

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

view this post on Zulip Alex J. Best (Aug 09 2019 at 03:58):

Importing library search is then import tactic.library_search

view this post on Zulip Nathan Ringo (Aug 09 2019 at 04:03):

okay, looks like that worked; thanks!

view this post on Zulip Alex J. Best (Aug 09 2019 at 04:12):

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.

view this post on Zulip Bryan Gin-ge Chen (Aug 09 2019 at 04:26):

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


Last updated: May 14 2021 at 21:11 UTC