Equivalent Lean command for Coq's Search?

Stream: new members

[Agnishom Chattopadhyay]

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]

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]

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]

That's an or not an either .. or

[Chris B]

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]

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

Where can I find documentation on find?

[Alex J. Best]

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

[Alex J. Best]

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