Finished task025 #16
Finished task025 #16
Conversation
tasks/human_eval_025.rs
Outdated
|
|
||
| pub fn factorize(n: u8) -> (factorization: Vec<u8>) | ||
| requires | ||
| 1 < n < 255, |
There was a problem hiding this comment.
Why do we need to exclude 0 and 255?
There was a problem hiding this comment.
And would the proofs change significantly for u32 or u64?
There was a problem hiding this comment.
We need to exclude 0 and 1 since they don't have prime factorizations. 255 needs to be excluded otherwise there will be an overflow on the last iteration of the loop. The proofs won't change for u32 or u64
There was a problem hiding this comment.
It seems like the suggested Python solution will return an empty list if n is 0 or 1. I guess that's one way of signaling that there is no prime factorization.
255 needs to be excluded otherwise there will be an overflow on the last iteration of the loop.
Could we address that by making m a u16?
There was a problem hiding this comment.
Could we address that by making m a u16?
Yes, done!
It seems like the suggested Python solution will return an empty list if n is 0 or 1. I guess that's one way of signaling that there is no prime factorization.
Sure, I've extended it to include 1. I don't including 0 makes sense here: technically any prime number is a "factor" of 0, so it doesn't make sense to return the empty list. Similarly, I don't think defining this on negative numbers makes sense.
There was a problem hiding this comment.
Okay, sounds reasonable to me. Thanks for making the changes!
|
I have made all of the changes requested or replied to your where I haven't. Yes, there are no new changes to 015. I forgot to sync my fork. Sorry about that! |
Finished task 025. I have not run verusfmt yet, will wait for your ok so that you can see the changes.
Specification uses Seq instead of Seq. This is to avoid the sequence conversion issue we discussed on Slack. Happy to discuss further!