Commit 2022-11-01 23:28 0c6ca881
View on Github →feat: library_search using (#503)
Implement the library_search using X
clause, which only returns results for which X
appears as a subexpression.
The mathlib3 implementation is still cleverer, but would require full implementation of solveByElim
with backtracking across multiple goals. I'll get there later.