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.