Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132// ANCHOR: exampleuse vstd::contrib::exec_spec::*;use vstd::prelude::*;
verus! {
exec_spec_unverified! {
struct Point { x: i64, y: i64,}
spec fn on_line(points: Seq<Point>) -> bool { forall |i: usize| #![auto] 0 <= i < points.len() ==> points[i as int].y == points[i as int].x}
}
} // verus!// ANCHOR_END: example// ANCHOR: checkfn main() { let p1 = ExecPoint { x: 1, y: 1 }; let p2 = ExecPoint { x: 2, y: 2 }; let points = vec![p1, p2]; let b = exec_on_line(points.as_slice()); assert_eq!(b, true);}// ANCHOR_END: check