Skip to content

[Merged by Bors] - feat: port Data.List.Zip#1416

Closed
zeramorphic wants to merge 19 commits intomasterfrom
port/Data.List.Zip
Closed

[Merged by Bors] - feat: port Data.List.Zip#1416
zeramorphic wants to merge 19 commits intomasterfrom
port/Data.List.Zip

Conversation

@zeramorphic
Copy link
Copy Markdown
Collaborator

@zeramorphic zeramorphic commented Jan 7, 2023 •
edited by jcommelin
Loading

@zeramorphic zeramorphic added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Jan 7, 2023
@kim-em kim-em added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 7, 2023
@zeramorphic
File compiles
532767f 
Signed-off-by: zeramorphic <zeramorphic@proton.me>
@zeramorphic
Naming fixes
301ccad 
Signed-off-by: zeramorphic <zeramorphic@proton.me>
@zeramorphic
Copy link
Copy Markdown
Collaborator Author

zeramorphic commented Jan 7, 2023

Porting note: length_zipWith wasalready in Std, so was removed.

@zeramorphic zeramorphic removed the WIP Work in progress label Jan 7, 2023
@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 10, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jan 10, 2023

This PR/issue depends on:

@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 10, 2023
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 10, 2023
jcommelin
jcommelin approved these changes Jan 10, 2023
View reviewed changes
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 10, 2023
bors bot pushed a commit that referenced this pull request Jan 10, 2023
@jcommelin @ChrisHughes24
@kim-em @zeramorphic
feat: port Data.List.Zip (#1416)
4f6d3be 
- [x] depends on: #1380

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: thirdsgames <thirdsgames2018@gmail.com>
Co-authored-by: zeramorphic <zeramorphic@proton.me>
@bors
Copy link
Copy Markdown

bors bot commented Jan 10, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Data.List.Zip [Merged by Bors] - feat: port Data.List.Zip Jan 10, 2023
@bors bors bot closed this Jan 10, 2023
@bors bors bot deleted the port/Data.List.Zip branch January 10, 2023 08:32
jcommelin added a commit that referenced this pull request Jan 23, 2023
@jcommelin @ChrisHughes24
@kim-em @zeramorphic
feat: port Data.List.Zip (#1416)
6cab0da 
- [x] depends on: #1380

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: thirdsgames <thirdsgames2018@gmail.com>
Co-authored-by: zeramorphic <zeramorphic@proton.me>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees

No one assigned

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

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@zeramorphic @kim-em @jcommelin @ChrisHughes24