Stream: new members
Topic: searching theorems
ohhaimark (Mar 11 2020 at 10:37):
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 (Mar 11 2020 at 10:55):
Marc Huisinga (Mar 11 2020 at 10:57):
lastly, there's also #find
Last updated: May 13 2021 at 18:26 UTC