-
Notifications
You must be signed in to change notification settings - Fork 297
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(data/num/prime): kernel-friendly decision procedure for prime #3525
Conversation
I guess |
|
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.
Should the to_num
class be added to mathlib too (in another PR, I guess)? I suppose it won't be used much by folks who don't care about computation, but it might be educational.
@bryangingechen I think it should be in a separate PR if so, and also in a locale because I think the instances might cause problems when used outside their intended use case. |
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.
Besides a bit more in the module doc ("why does this file exist?") this looks good!
src/data/num/prime.lean
Outdated
/-! | ||
# Primality for binary natural numbers | ||
|
||
Decision procedures for primality on `num`. |
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.
Could you write a bit more about the contents and intent of this file?
bors merge |
Pull request successfully merged into master. Build succeeded: |
No description provided.