Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC