-
Notifications
You must be signed in to change notification settings - Fork 323
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
chore: redefine Nat.bit
Nat.div2
Nat.bodd
#13649
base: master
Are you sure you want to change the base?
Conversation
Nat.binaryRec
Nat.div2
Nat.bodd
PR summary 7e64fc89b0Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit> The doc-module for |
Please describe how and why did you change the definition(s) in the commit message. |
/-- `bit b` appends the digit `b` to the little end of the binary representation of | ||
its natural number input. -/ | ||
def bit (b : Bool) (n : Nat) : Nat := | ||
cond b (n <<< 1 + 1) (n <<< 1) |
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.
Presumably | 1
is also faster than + 1
, if you're really micro-optimizing?
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.
It's not faster in my tests. Also it would make proofs much more complicated.
Nat.binaryRec
Nat.div2
Nat.bodd
Nat.bit
Nat.div2
Nat.bodd
This is #13649 with fewer definition changes.
This PR/issue depends on: |
@FR-vdash-bot, please solve the merge conflicts. |
The new definitions are faster than the old ones.
Nat.binaryRec
will be moved to batteries (leanprover-community/batteries#799) or core (leanprover/lean4#3756), so relevant contents are moved to a new file temporarily.Nat
into a new file #15567