Search for theorems/uses of definitions

Stream: new members

[Josh Cohen]

Hello, is there a way to search in Lean for all theorems and definitions in the context that use a particular type? In Rocq, for example, I can use Search list to find all definitions that involve lists. I have explored Loogle a bit but that does not include any user-created functions, I believe.

[Ruben Van de Velde]

Loogle covers mathlib as well, but I guess not your own code

[Josh Cohen]

Relatedly, is there a way to see the un-elaborated/hand-written definition of a function? For example, if I want to see how Nat.add is defined, #print shows me the version defined in terms of Nat.brecOn, which is harder to read than the version defined by pattern matching.

[Aaron Liu]

you can go to the definition

[Aaron Liu]

or look at Nat.add.eq_def

[Josh Cohen]

How do I go to the definition (in VSCode, for example)? And does every function foo create a foo_eq_def rewrite lemma?

[Aaron Liu]

Josh Cohen said:

How do I go to the definition (in VSCode, for example)?

do #check foo and right-click the foo and do "go to definition"

[Aaron Liu]

Josh Cohen said:

And does every function foo create a foo_eq_def rewrite lemma?

every definition foo should either create a foo.eq_def or throw an error saying it had a problem creating the equational theorem

[Josh Cohen]

Thank you! Those both certainly make it easier to inspect definitions. I am still curious if there are any other search facilities in Lean if I don't already know the definition name.

[Jakub Nowak]

Just learned there's #find command. It looks similar to loogle, but I think it works for all user-code too?

[Josh Cohen]

Thanks, that looks like what I was looking for. It looks like it does not come with Lean by default. How can I use it? Do I need to import mathlib or something?

[Kevin Buzzard]

From the link given above, looks like you need to import Mathlib.Tactic.Find (at the very least).

[Josh Cohen]

Thank you, this functionality is very useful and very close to what I was hoping for. Are there any plans to include this in Lean by default to be usable in non-mathlib projects?

[Dan Abramov]

Note VS Code also has "Go to References" for any symbol.

Screenshot 2025-09-06 at 04.49.02.png
Screenshot 2025-09-06 at 04.49.12.png

[Dan Abramov]

And there's also Cmd+Click (Ctrl+Click on windows?) shortcut for Go to Definition.

[Marc Huisinga]

BTW, "Show Call Hierarchy" is very similar to "Go to References" and "Find All References" in Lean, but I think the UI is nicer in most cases (e.g. since you can quickly navigate recursively)