mathlib3
feat(tactic/suggest): generalize and reimplement library_search
#1552
Merged
Merged
feat(tactic/suggest): generalize and reimplement library_search #1552
mergify
merged
54 commits into
leanprover-community:master
from
refine_list
Merge pull request #1 from leanprover-community/master
4a7c517b
Merge pull request #2 from leanprover-community/master
2e124712
Merge pull request #3 from leanprover-community/master
ba6ede3a
Create refine_list.lean
cb910f42
Create refine_list.lean
276c9542
Update tactics.md
666b4e76
Update library_search.lean
95641382
Update library_search.lean
6523a85c
commits
802aacee
refine_list commits
77f21f7e
Scott's work
0d408caf
update tactics.md
3f320081
doc strings
1915d3dc
Merge branch 'refine_list' of github.com:u6338192/mathlib into refine…
8fac3012
update
8114724c
Merge branch 'refine_list' of https://github.com/u6338192/mathlib int…
9088e003
Update refine_list.lean
e0872022
Update refine_list.lean
60f883ee
get_state and set_state replace by read and write
e123afe1
Combined functions and removed run_and_save_state
404ab0b9
removed symmetry from library_search
947cc51c
removing test that doesn't work without symmetry
c9933e8a
test properly
f7baaf19
rename `refine_list` to `suggest`
2c6a9f7b
kim-em
changed the title
cleaning up
a0710a34
minor
4c7fd4cc
better sorting of results
f45f5d78
oops, turn off trace messages again
81ef2165
type annotation
79da7c1e
optimisation, and simpler logic
2970a41c
further explanation
65c1e857
a little more cleanup
7d0b82a5
Update src/tactic/library_search.lean
0d133411
Update src/tactic/suggest.lean
44a6fc5c
Update src/tactic/suggest.lean
5608117e
changed interactive to tactic.interactive
596cfb22
Merge branch 'refine_list' of https://github.com/u6338192/mathlib int…
dcb3dc89
used /--/ for copyright headers
97e8330e
Merge branch 'refine_list' of https://github.com/u6338192/mathlib int…
88ab4d1e
adding comments explaining logic in apply_and_solve, and an optimisation
a4fc85a2
Merge branch 'refine_list' of github.com:u6338192/mathlib into refine…
693c15f3
refactor no_mvars_in_target
498a5a6b
add missing argument to interactive tactic
aa6f633d
move all printing to the interactive tactic
ab5e446b
refactoring
c33d76b9
Merge branch 'master' into refine_list
e9e70910
cleanup
f415e16c
refactoring
0a98697a
complete refactor; library_search is defined in terms of suggest_core…
459613e2
Merge remote-tracking branch 'origin/master' into refine_list
c7b36c6d
restore protect to list.traverse and option.traverse
e2112e2f
robertylewis
commented
on 2019-10-19
robertylewis
changed the title
Update src/tactic/suggest.lean
21e29c96
some doc comments
dc70a09d
Merge branch 'master' into refine_list
75347713
robertylewis
approved these changes
on 2019-10-20
Reviewers
Assignees
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub