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
feat: port Data.Nat.Bits #1075
feat: port Data.Nat.Bits #1075
Conversation
…Mathlib.Data.Nat.Bits
Please reopen this as a PR from a branch on this repository, so that CI can run. |
mathlib3port_commit.txt
Outdated
@@ -0,0 +1 @@ | |||
d012cd09a9b256d870751284dd6a29882b0be105 |
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.
I don't think this file was intended to be committed.
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.
Yeah sorry. I shall remove it
Hi @semorrison Is there a way to move this PR as required? |
New Pull Request for data.nat.bits Reasons for opening: 1. #1075 (comment) 2. https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/data.2Enat.2Ebits/near/316544221 Co-authored-by: ART0 <18333981+0Art0@users.noreply.github.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
First PR for
data.nat.bits
. Copied file Data/Nat/Bits.lean from mathlib3port as is.Mathlib commit : d012cd09a9b256d870751284dd6a29882b0be105