Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: minimal port of Fintype (Fin n) #433

Closed
wants to merge 29 commits into from
Closed

[Merged by Bors] - feat: minimal port of Fintype (Fin n) #433

wants to merge 29 commits into from

Conversation

semorrison
Copy link
Contributor

@semorrison semorrison commented Sep 21, 2022 •
edited

@semorrison semorrison added WIP Work in progress blocked-by-other-PR This PR depends on another PR which is still in the queue. labels Sep 21, 2022
@semorrison semorrison mentioned this pull request Sep 23, 2022
Closed
@semorrison semorrison removed the WIP Work in progress label Sep 23, 2022
@semorrison semorrison added awaiting-review The author would like community review of the PR and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. labels Sep 23, 2022
@semorrison semorrison marked this pull request as ready for review September 23, 2022 02:59
@semorrison
Copy link
Contributor Author

@digama0, I've hopefully followed the style corrections you made on #433 here.

This PR is not strictly necessary for #437, just for the tests. If you think it's best to avoid porting too much stuff by hand at this point, we can probably get by without this and defer having proper tests for fin_cases until later.

@digama0
Copy link
Member

digama0 commented Sep 23, 2022

I don't think we have to be super surgical about porting only the bare minimum here; I generally port entire files when it seems like I might need some part of them (although possibly we can make an exception for the really large files). Most of this stuff is destined for std4 anyway.

@digama0
Copy link
Member

digama0 commented Oct 7, 2022

bors r+

bors bot pushed a commit that referenced this pull request Oct 7, 2022
@semorrison
feat: minimal port of Fintype (Fin n) (#433)
3c481ef 
- [x] depends on: #429

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Oct 7, 2022

Build failed:

@semorrison
Copy link
Contributor Author

bors merge

bors bot pushed a commit that referenced this pull request Oct 8, 2022
@semorrison
feat: minimal port of Fintype (Fin n) (#433)
089576b 
- [x] depends on: #429

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Oct 8, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: minimal port of Fintype (Fin n) [Merged by Bors] - feat: minimal port of Fintype (Fin n) Oct 8, 2022
@bors bors bot closed this Oct 8, 2022
@bors bors bot deleted the semorrison/fintype_fin branch October 8, 2022 09:27
bors bot pushed a commit that referenced this pull request Oct 18, 2022
@semorrison
feat: port fin_cases (#437)
6fb0ab0 
This is a port of `fin_cases`. It doesn't yet support the `with` or `using` clauses from mathlib3.

I could remove the dependence on #433, but would have to (temporarily) remove all the tests to do so.

* depends on: #433

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
bors bot pushed a commit that referenced this pull request Oct 20, 2022
@semorrison
feat: port fin_cases (#437)
c41ef59 
This is a port of `fin_cases`. It doesn't yet support the `with` or `using` clauses from mathlib3.

I could remove the dependence on #433, but would have to (temporarily) remove all the tests to do so.

* depends on: #433

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

@digama0 digama0 Awaiting requested review from digama0

Assignees
No one assigned
Labels
awaiting-review The author would like community review of the PR
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@semorrison @digama0