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.

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

Add some traits of S18 #1151

Draft
wants to merge 2 commits into
base: main
Choose a base branch
from

Conversation

Moniker1998
Copy link
Collaborator

For now its a draft because the amount of properties that need to be added is a little overwhelming to me

@prabau
Copy link
Collaborator

prabau commented Dec 24, 2024

If it's overwhelming, PLEASE do not do a gigantic PR. It's preferable to do several smaller PRs, each adding a subset of the properties. This will allow speedier review and merging. If one depends on another, even better is to wait until the previous one is merged. This will go quickly if each is of manageable size.

@Moniker1998
Copy link
Collaborator Author

Moniker1998 commented Dec 24, 2024

If it's overwhelming, PLEASE do not do a gigantic PR. It's preferable to do several smaller PRs, each adding a subset of the properties. This will allow speedier review and merging. If one depends on another, even better is to wait until the previous one is merged. This will go quickly if each is of manageable size.

All of those changes will be me citing "this is a Komogorov quotient os S17 and S17 is ...", but it still requires me to search for those properties. That's why its overwhelming. The PR won't actually be that large/unmanageable

Other properties I'll be adding in a separate PR (or PRs)

@Moniker1998
Copy link
Collaborator Author

Moniker1998 commented Dec 24, 2024

@prabau I've tried updating my branch (double-pointed-cocountable-topology-on-R) to be up to main, but it seems like it treats this PR like this huge update now. Do you know how to fix it? Should I close this and create new pull request?

@Moniker1998
Copy link
Collaborator Author

@StevenClontz

@prabau
Copy link
Collaborator

prabau commented Dec 25, 2024

@Moniker1998 Sorry I just saw this. I think the right way was to "merge main into your branch", but I am not quite sure how to do this. @StevenClontz ?

@StevenClontz
Copy link
Member

Exploring this now. I'm pretty good at avoiding weird Git merges personally, but not so great at fixing them when they go awry. Let me see.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants