Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
12345678910111213141516171819202122use vstd::prelude::*;
verus! {
spec fn min(x: int, y: int) -> int { if x <= y { x } else { y }}
fn main() { assert(min(10, 20) == 10); assert(min(-10, -20) == -20); assert(forall|i: int, j: int| min(i, j) <= i && min(i, j) <= j); assert(forall|i: int, j: int| min(i, j) == i || min(i, j) == j); assert(forall|i: int, j: int| min(i, j) == min(j, i));}
} // verus!