searching theorems

Stream: new members

[ohhaimark]

Does lean or mathlib have anything to search theorems? Something like entering an expression with some metavariables and finding a definition whose type contains a subexpression that can unify with it.

[Marc Huisinga]

afaik, there's library_search, hint and suggest.

[Marc Huisinga]

lastly, there's also #find