mathlib3
fix(tactic/refine_struct): don't add unnecessary `eq.mpr` or `id`
#2319
Merged
Merged
fix(tactic/refine_struct): don't add unnecessary `eq.mpr` or `id` #2319
mergify
merged
14 commits into
master
from
refine-struct
fix(tactic/interactive): don't unfold non-Prop goals
c394815b
add a test file
4113461b
bryangingechen
commented
on 2020-04-03
move test
b3b9572b
kim-em
changed the title
actually move test
cab90dbb
Merge branch 'master' into refine-struct
5874739b
bryangingechen
commented
on 2020-04-03
Update test/refine_struct.lean
61b55345
test: fix compile
85c2d0dc
Apply suggestions from code review
6a516503
Merge branch 'refine-struct' of git://github.com/leanprover-community…
45d98f8b
urkud
commented
on 2020-04-05
Try a fix by @gebner and @cipher1024
09f97418
Update test/refine_struct.lean
a5962c77
apply Gabriel's suggestion
c138bb14
urkud
changed the title
kim-em
approved these changes
on 2020-04-07
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into refine-struct
4f5741c4
Merge branch 'master' into refine-struct
beefe9a4
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
t-meta
Milestone
No milestone
Login to write a write a comment.
Login via GitHub