PR #1349 feat(data/vector2): nth_map

feat(data/vector2): nth_map #1349

mergify merged 4 commits into master from ChrisHughes24-patch-2

feat(data/vector2): nth_map

8c76ac46

ChrisHughes24 requested a review 6 years ago

Update vector2.lean

2f12b597

Update vector2.lean

8f007236

robertylewis approved these changes on 2019-08-20

robertylewis added ready-to-merge

Merge branch 'master' into ChrisHughes24-patch-2

d606c6a7

mergify merged 6f747ec2 into master 6 years ago

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

Reviewers

robertylewis

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone