## Stream: new members

### Topic: Equivalent Lean command for Coq's Search?

#### Agnishom Chattopadhyay (Jan 10 2020 at 17:05):

Coq has the Search command which lets you look for theorems relevant to a particular term or a pattern or a string. For example one could run "Search list." and it would let you find the theorems available which involve "list".

What is the Lean equivalent of this?

#### Johan Commelin (Jan 10 2020 at 18:36):

There is find which seems to be less than optimal and doesn't get much love. Then there are the tactics suggest and library_search which might be more helpful if you are searching for one specific theorem (you know the type, but not the name).
For a list of theorems involving list, I guess currently your best option is generic search tools like grep.

#### Bryan Gin-ge Chen (Jan 10 2020 at 18:41):

If you're using VS Code, you can access the Lean server's search feature by hiting ctrl (or cmd if on a mac) + p and then typing the # character before your search string. I think this searches all declarations either imported or in open files? Presumably the Emacs mode has access to this as well.

#### Johan Commelin (Jan 10 2020 at 18:52):

That's an or not an either .. or

#### Chris B (Jan 11 2020 at 18:19):

You can also get an output of all of the definitions (including theorems) associated with list (or any other type) by using #print prefix list

#### Agnishom Chattopadhyay (Jan 12 2020 at 05:21):

Yeah, these are great options. The VS code trick seems to work very well.

Where can I find documentation on find?

#### Alex J. Best (Jan 12 2020 at 05:58):

https://leanprover-community.github.io/mathlib_docs/commands.html#find

#### Alex J. Best (Jan 12 2020 at 05:59):

But there isn't a lot there, the source is at https://github.com/leanprover-community/mathlib/blob/master/src/tactic/find.lean

Last updated: May 14 2021 at 03:27 UTC