Closed pixelshot91 closed 4 months ago
The anchor is used here: https://viperproject.github.io/prusti-dev/user-guide/tour/pledges.html#writing-a-test-for-our-specification Right now the snippet only shows this:
#[cfg(prusti)]
mod prusti_tests {
use super::*;
Can we merge, @Aurel300?
The anchor is used here: [...]
Ah, my bad. Thanks!
Thanks! The changes look good, but why the new anchor? I don't see it used anywhere.