-
Notifications
You must be signed in to change notification settings - Fork 299
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] - feat(archive/imo): formalize IMO 1964 problem 1 #4935
Conversation
@lacker you're the expert here -- I tried to follow your suggestions in the other thread about sticking as closely as possible to the actual question wording, when formalising the question. Let me know if there are other IMO question conventions I should be abiding by. |
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
Looks good to me from an "imo question conventions" point of view. |
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.
LGTM.
bors d+
✌️ kbuzzard can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
This is an alternative approach to #4369, where progress seems to have stalled. I avoid integers completely by working with `nat.modeq`, and deal with the cases of n mod 3 by simply breaking into three cases. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Pull request successfully merged into master. Build succeeded: |
This is an alternative approach to #4369, where progress seems to have stalled. I avoid integers completely by working with
nat.modeq
, and deal with the cases of n mod 3 by simply breaking into three cases.