mathlib
2c97f239 - feat(tactic/library_search): small improvements (#3037)

Commit
5 years ago
feat(tactic/library_search): small improvements (#3037) This makes the following small improvements to `library_search`: 1. ~~Don't use `*.inj` lemmas, which are rarely useful. (Cuts test file from 95 seconds to 90 seconds.)~~ 2. Some refactoring for reusability in other tactics. 3. `apply_declaration` now reports how many subgoals were successfully closed by `solve_by_elim` (for use by new tactics) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading