mathlib3
feat(tactic/apply'): apply without unfolding type definitions
#1234
Merged
Merged
feat(tactic/apply'): apply without unfolding type definitions
397e3bf0
Merge branch 'master' into new-apply
d81f7d80
Update src/tactic/interactive.lean
404650a4
improve doc
4b32931e
more doc
4fc20617
Update core.lean
4a513547
Merge branch 'master' into new-apply
20b30ee6
fpvandoorn
commented
on 2019-08-21
add test case
bcf83991
add test case
e6df4d45
improve treatment of type class instances for apply'
63f19577
tweak application of instance resolution
b86ca3b1
fix
875031c3
move `apply'` to its own file
7349b9f4
adjust docs
ac0e3749
import apply from tactic.default
0dff4c74
fix import in test
7661571f
robertylewis
approved these changes
on 2019-08-22
Update tactics.lean
aee5fab0
Merge branch 'master' into new-apply
1e3a1d74
Reviewers
Assignees
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub