Commit 2023-04-18 10:28 b7868532

chore: refactor of library_search, and don't timeout (#3228) This is a refactor of library_search, separating the logic of applying lemmas and flow control (i.e. stopping if we find a good one). This version has an intermediate function that returns a lazy list of candidate results, using the new ListM API. As an easy add-on, we make sure library_search never times out