Commit 2020-04-25 05:42 199f6fe4

refactor(tactic/suggest): call library_search and suggest with additional lemmas, better lemma caching (#2429) This PR is mainly a refactoring of suggest. The changes include:

• Removed (discharger : tactic unit := done) from library_search, suggest, suggest_scripts suggest_core, suggest_core', apply_declaration and apply_and_solve and replaced by (opt : by_elim_opt := { }) from solve_by_elim.
• Replaced all occurences of discharger by opt, opt.discharger, or ..opt.
• inserted a do block into the interactive library_search function.
• Added asms ← mk_assumption_set no_dflt hs attr_names, to the interactive suggest and library_search functions. This is so library_search and suggest don't rebuild the assumption set each time a lemma is applied.
• Added several inputs for the interactive library_search and suggest function. These parameters were lifted from the interactive solve_by_elim function and allow the user to control how solve_by_elim is utilized by library_search and suggest.
• Removed the message function (redundant code.)
• Removed several unnecessary g ← instantiate_mvars g, lines.