wrote some programs #9
Conversation
tasks/human_eval_055.rs
Outdated
There was a problem hiding this comment.
This is a reasonable solution in that it follows the Python version. It might be nice to include a variant of this file (as we've done for a few other challenges) that demonstrates a non-recursive solution as well.
tasks/human_eval_056.rs
Outdated
| fn correct_bracketing(brackets: &str) -> (ret: bool) | ||
| requires | ||
| [email protected]() <= i32::MAX | ||
| [email protected]() >= i32::MIN |
There was a problem hiding this comment.
Why is this condition required? brackets@ should give you a Seq, and then len() should give you a nat.
There was a problem hiding this comment.
Its to prevent overflow of the stack size local variable.
[email protected]() >= i32::MIN isn't strictly necessary, but in my case stack_size keeps decrementing if there are lots of >. I thought its nicer to keep it symmetric.
|
Also feel free to comment here on the programs verified except for a few |
|
As a side note, I just migrated the contents of |
Hi I translated some of the benchmark programs. Please let me know if there's something else to do to merge my PR