Commit 2019-09-24 05:46 327098b4
View on Github →feat(tactic/library_search): a more powerful library_search (#1470)
- experimental extensions to library_search
- upgrades to library_search
- remove ! for a later PR
- move
run_norm_num - oops
- Update src/tactic/library_search.lean Co-Authored-By: Floris van Doorn fpvdoorn@gmail.com
- remove run_norm_num for later