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: port Data.Nat.Nth #2297
Conversation
@mo271 Are you working on this now? If no, then I'm going to fix the rest. |
I fixed compile but I failed to stop myself from reviewing proofs/API. Now I'm going to split this PR into easily reviewable chunks. |
c776f64
to
e789cda
Compare
Could you update the SHA? |
To what? We're still waiting for #18760 |
@YaelDillies It makes no sense to update this branch because I'm going to restart it once leanprover-community/mathlib#18760 is merged. |
It makes sense to me because it was costing us one file out of 20 on our out-of-sync budget 😛 |
I'm going to rebase today. Please don't merge master. |
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
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.
Please check if you can restore push_neg
; lgtm otherwise. Could you mark as awaiting-review if you agree?
This PR/issue depends on: |
bors merge |
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Komyyy <pol_tta@outlook.jp>
push_neg
makes loose bounded variables #5257