Skip to content

Commit

Permalink
Debug some comma issues that turned out to be a problem on the Verus
Browse files Browse the repository at this point in the history
side.
The NR projects now successfully formats and verifies.
  • Loading branch information
parno committed Dec 24, 2023
1 parent 8ed3c90 commit 4f5a7c7
Showing 1 changed file with 32 additions and 7 deletions.
39 changes: 32 additions & 7 deletions examples/wip.rs
Original file line number Diff line number Diff line change
@@ -1,13 +1,38 @@
use vstd::prelude::*;

verus! {

// TODO: Need to add support for if-let https://doc.rust-lang.org/reference/expressions/if-expr.html
fn test() {
if let Result::Ok(val) = res {
0
} else {
1
}
/*
spec fn test_rec2(x: int, y: int) -> int
decreases x, y,
{
3
}
*/

spec fn add0(a: nat, b: nat) -> nat
recommends
a > 0,
via add0_recommends,
{
a
}

#[via_fn]
proof fn add0_recommends(a: nat, b: nat) {
// proof
}

/*
spec fn rids_match(bools_start: nat) -> bool
decreases bools_start,
when 0 <= bools_start <= bools_end <= bools.len() && 0 <= rids_start <= rids_end <= rids.len()
{
true
}
*/

fn main() {}

} // verus!

Expand Down

0 comments on commit 4f5a7c7

Please sign in to comment.