mathlib3
fix(tactic/transport): make `to_additive` copy `protected`status
#2212

Merged

fix(tactic/transport): make `to_additive` copy `protected`status #2212

mergify merged 7 commits into master from to-additive-protected

fix(tactic/transport): make `to_additive` copy `protected`status

47f453cb

urkud added WIP

Fix compile (protected `finset.sum`)

79e727ca

Fix usage of `finset.sum`

f035fb29

gebner commented on 2020-03-22

Update src/tactic/transport.lean

9e1ef2ae

urkud marked this pull request as ready for review 6 years ago

urkud removed WIP

urkud added awaiting-review

bryangingechen commented on 2020-03-22

fix build

67cb2024

gebner approved these changes on 2020-03-22

gebner removed awaiting-review

gebner added ready-to-merge

Merge branch 'master' into to-additive-protected

a53fda72

Merge branch 'master' into to-additive-protected

2a8f90fb

mergify merged 7f103fd3 into master 6 years ago

urkud deleted the to-additive-protected branch 6 years ago

Reviewers

gebner

bryangingechen

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone