Stream: new members
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):
find which seems to be less than optimal and doesn't get much love. Then there are the tactics
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
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):
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
Alex J. Best (Jan 12 2020 at 05:58):
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