Skip to content

[Merged by Bors] - feat: port Data.List.Join#1395

Closed
zeramorphic wants to merge 20 commits intomasterfrom
port/Data.List.Join
Closed

[Merged by Bors] - feat: port Data.List.Join#1395
zeramorphic wants to merge 20 commits intomasterfrom
port/Data.List.Join

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
93c09ad 
Signed-off-by: zeramorphic <zeramorphic@proton.me>
@zeramorphic
Fix deprecations
63ddb20 
Signed-off-by: zeramorphic <zeramorphic@proton.me>
@zeramorphic
Naming fixes
7c58142 
Signed-off-by: zeramorphic <zeramorphic@proton.me>
@zeramorphic
Revert BigOperators/Basic.lean to match PR branch
4409f49 
Signed-off-by: zeramorphic <zeramorphic@proton.me>
@zeramorphic
Copy link
Copy Markdown
Collaborator Author

zeramorphic commented Jan 7, 2023

Following Mario's advice, I modified the proof of eq_iff_join_eq to avoid using nthLe at all. This duplicates a couple of lemmas, so they now have nthLe and get variants. The nthLe variants are marked as deprecated.

@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 reviewed Jan 10, 2023
View reviewed changes
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jan 10, 2023
@zeramorphic
Align List.isEmpty
0e48dc0 
Signed-off-by: zeramorphic <zeramorphic@proton.me>
@zeramorphic
Copy link
Copy Markdown
Collaborator Author

zeramorphic commented Jan 10, 2023 •
edited
Loading

I think I've put the align in the right place. I'm still not sure about the correct spelling of join_filter_isEmpty_eq_false.

@jcommelin jcommelin added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 10, 2023
jcommelin
jcommelin reviewed Jan 10, 2023
View reviewed changes
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Jan 10, 2023

Thanks 🎉

bors merge

@github-actions github-actions bot 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 @zeramorphic
feat: port Data.List.Join (#1395)
0c18be9 
- [x] depends on: #1380

Co-authored-by: ChrisHughes24 <chrishughes24@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

Canceled.

@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Jan 10, 2023

bors merge

bors bot pushed a commit that referenced this pull request Jan 10, 2023
@jcommelin @ChrisHughes24 @zeramorphic
feat: port Data.List.Join (#1395)
07eef42 
- [x] depends on: #1380

Co-authored-by: ChrisHughes24 <chrishughes24@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.Join [Merged by Bors] - feat: port Data.List.Join Jan 10, 2023
@bors bors bot closed this Jan 10, 2023
@bors bors bot deleted the port/Data.List.Join branch January 10, 2023 12:24
jcommelin added a commit that referenced this pull request Jan 23, 2023
@jcommelin @ChrisHughes24 @zeramorphic
feat: port Data.List.Join (#1395)
61f6e81 
- [x] depends on: #1380

Co-authored-by: ChrisHughes24 <chrishughes24@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 left review comments

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