Commit 2019-10-20 10:46 74bed0c9

View on Github →

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