PR #1370 feat(data/option/basic): eq_some_iff_get_eq

feat(data/option/basic): eq_some_iff_get_eq #1370

mergify merged 3 commits into master from ChrisHughes24-patch-1

feat(data/option/basic): eq_some_iff_get_eq

0d6d4ca2

ChrisHughes24 requested a review 6 years ago

Update basic.lean

87bf7e90

jcommelin approved these changes on 2019-08-31

jcommelin added ready-to-merge

Merge branch 'master' into ChrisHughes24-patch-1

cae1c1c7

mergify merged df65dde5 into master 6 years ago

mergify deleted the ChrisHughes24-patch-1 branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone