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.

Estimated changes