Commit 2023-06-10 07:04 ae75b324

View on Github →

feat: better handling of symm in library_search (#4534) Rather than separately indexing the symm version of each Eq lemma (and Iff lemma, although we were forgetting to do this at all!), we just try library_search on the goal and then on symm of the goal.

Estimated changes