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.
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
[Merged by Bors] - refactor(data/fintype/basic): split file #17578
Conversation
semorrison
commented
Nov 17, 2022
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
LGTM bors d+ |
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
Oh I had an almost ready split. |
/-! | ||
# fintype instances for sigma types | ||
-/ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There's an argument that those structure files should be merged with the corresponding ones under finset
. The ones under finset
are basically only imported by the fintype
ones, and they are a continuation of each other.
I've now run the linter and tests locally, so let's try: bors merge |
bors merge |
👎 Rejected by label |
bors merge |
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |