mathlib3
feat(tactic/squeeze): improve suggestion of `cases x; squeeze_simp`
#2218
Merged
Merged
feat(tactic/squeeze): improve suggestion of `cases x; squeeze_simp` #2218
mergify
merged
16 commits into
master
from
squeeze_args
feat(tactic/squeeze): improve produced argument list and format
0c99126e
feat(tactic/squeeze): combine suggestions of repeated executions
d2207475
add documentation
bf98e2f1
remove dead code
6bd339b2
suggestion from reviewers
95bfa747
Apply suggestions from code review
59080af1
cipher1024
changed the title
Update squeeze.lean
1526fad1
bryangingechen
commented
on 2020-03-23
bryangingechen
commented
on 2020-03-23
bryangingechen
commented
on 2020-03-23
bryangingechen
commented
on 2020-03-23
bryangingechen
commented
on 2020-03-23
bryangingechen
commented
on 2020-03-23
bryangingechen
commented
on 2020-03-23
Apply suggestions from code review
debe8b29
simplify and remove comparison of proof terms
68e5469b
simplify goal comparison data structure
9e2239a1
bryangingechen
commented
on 2020-03-24
add documentation and fix meta-variable handling
a784fc0d
bryangingechen
commented
on 2020-03-25
add example
078ca909
gebner
commented
on 2020-03-25
fix tests
e1152541
move tests
a3a18cb9
use binders with trivial names to abstract meta variables
637d1af9
gebner
approved these changes
on 2020-03-25
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into squeeze_args
aaa449c7
Login to write a write a comment.
Login via GitHub