searching by type

Stream: Is there code for X?

[Miroslav Olšák]

As I was pointed to this stream, I would like to ask a meta question :smile: . Is there a code for searching for functions by their type? library_search works great for theorems but not really for general functions. I imagine something like Hoogle. It doesn't feel too different from the library_search tactic but there are a few differences

• I would like to see all the all the options, and not just one,
• library_search doesn't really work for meta definitions (try that :grinning:, the result is cute ),
• library_search sometimes does too fancy rearrangements (as it is "trying to prove a theorem")

[Kevin Buzzard]

#find has limited functionality in this direction, although I could never really figure out how to use it to search for a dependent type.

[Eric Wieser]

Does suggest do anything useful for functions?

[Miroslav Olšák]

I tried suggest, and it actually looks reasonable from the perspective it is showing multiple suggestions

def my_option_map : (ℕ → option ℕ) → list ℕ → list ℕ
:= by suggest
-- Try this: exact list.lookmap
-- Try this: exact list.filter_map

On the other hand, I still have no idea how to search for let's say list.mmap tactic

#check @list.mmap tactic (by apply_instance) ℕ ℕ
-- mmap : (ℕ → tactic ℕ) → list ℕ → tactic (list ℕ)

#find (ℕ → tactic ℕ) → list ℕ → tactic (list ℕ)
-- thinking for some time, and then no result
meta def my_mmap : (ℕ → tactic ℕ) → list ℕ → tactic (list ℕ)
:= by library_search
-- Try this: exact my_mmap
meta def my_mmap : (ℕ → tactic ℕ) → list ℕ → tactic (list ℕ)
:= by suggest
-- Try this: exact my_mmap

[Miroslav Olšák]

But for non-meta definitions, suggest looks relatively usable

def test : (ℕ → ℕ → ℕ) → list ℕ → list ℕ → list ℕ
:= by suggest
Try this: exact list.map₂
Try this: exact list.zip_with
Try this: exact tactic.merge_list
Try this: exact list.func.pointwise

(seeing the proper types of the found functions would be even better but I can always #check)