mathlib

74bed0c9 - feat(tactic/suggest): generalize and reimplement library_search (#1552)

feat(tactic/suggest): generalize and reimplement library_search (#1552) * Create refine_list.lean The refine_list tactic. * Create refine_list.lean The refine_list.lean file * Update tactics.md Added refine_list docs. * Update library_search.lean Added replace_mvars function * Update library_search.lean Added tactic_statement function and some code in the main library_search function which uses it. * commits * refine_list commits * Scott's work * update tactics.md * doc strings * update * Update refine_list.lean Removes stray TODO line and changed the docstring for the main refine_list function. * Update refine_list.lean Spelling... * get_state and set_state replace by read and write * Combined functions and removed run_and_save_state * removed symmetry from library_search * removing test that doesn't work without symmetry * test properly * rename `refine_list` to `suggest` * cleaning up * minor * better sorting of results * oops, turn off trace messages again * type annotation * optimisation, and simpler logic * further explanation * a little more cleanup * Update src/tactic/library_search.lean Rob Lewis's refactoring of `tactic_statement` Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com> * Update src/tactic/suggest.lean Remove `do` in line 82 Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com> * Update src/tactic/suggest.lean Rob's update of suggest in tactic.interactive. Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com> * changed interactive to tactic.interactive * used /--/ for copyright headers * adding comments explaining logic in apply_and_solve, and an optimisation * refactor no_mvars_in_target * add missing argument to interactive tactic * move all printing to the interactive tactic * refactoring * cleanup * refactoring * complete refactor; library_search is defined in terms of suggest_core now * restore protect to list.traverse and option.traverse * Update src/tactic/suggest.lean Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com> * some doc comments