theorem search

Stream: lean4

[Bhakti Shah]

is there an equivalent to Coq's Search or something like hoogle that lets you look up a theorem by structure or type? Not familiar enough with conventions to know where to look in the docs / what names to expect. I saw something about library_search somewhere but I haven't been able to find anything actually documenting it.

[Ruben Van de Velde]

Library search is now called exact?; there's also apply? for theorems that make progress but don't fully solve the goal

[Bhakti Shah]

that is super helpful thank you :) is there a way i can use this outside of an active proof? like if I just want to look something up that isn't in my current goal context.

[Martin Dvořák]

You can specify arbitrary goal using have inside a proof or using example outside of a proof.

[Anand Rao Tadipatri]

There is also the #find command that allows you to look up theorems and definitions by type. Some examples of its usage are here.