Skip to content

[Merged by Bors] - Feat: Port/data.vector.basic#1633

Closed
arienmalec wants to merge 67 commits intomasterfrom
port/Data.Vector.Basic
Closed

[Merged by Bors] - Feat: Port/data.vector.basic#1633
arienmalec wants to merge 67 commits intomasterfrom
port/Data.Vector.Basic

Conversation

@arienmalec
Copy link
Copy Markdown
Contributor

@arienmalec arienmalec commented Jan 17, 2023

Port of data.vector.basic

Does a realignment of Vector functions to mirror the List equivalents, particularly for nth which has been replaced by get


Open in Gitpod

@arienmalec arienmalec added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Jan 17, 2023
@arienmalec arienmalec added help-wanted The author needs attention to resolve issues and removed WIP Work in progress labels Jan 18, 2023
@ChrisHughes24 ChrisHughes24 added awaiting-review and removed help-wanted The author needs attention to resolve issues labels Jan 19, 2023
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@kim-em kim-em added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jan 19, 2023
bors bot pushed a commit that referenced this pull request Jan 19, 2023
Port of data.vector.basic

Does a realignment of `Vector` functions to mirror the `List` equivalents, particularly for `nth` which has been replaced by `get`
@bors
Copy link
Copy Markdown

bors bot commented Jan 19, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title Feat: Port/data.vector.basic [Merged by Bors] - Feat: Port/data.vector.basic Jan 19, 2023
@bors bors bot closed this Jan 19, 2023
@bors bors bot deleted the port/Data.Vector.Basic branch January 19, 2023 10:21
jcommelin pushed a commit that referenced this pull request Jan 23, 2023
Port of data.vector.basic

Does a realignment of `Vector` functions to mirror the `List` equivalents, particularly for `nth` which has been replaced by `get`
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants