vstd 0.0.0-2026-04-20-1748

Verus Standard Library: Useful specifications and lemmas for verifying Rust code
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

#![allow(unused_imports)]

use super::pervasive::*;
use super::prelude::*;

verus! {

pub trait Predicate<V> {
    spec fn predicate(&self, v: V) -> bool;
}

impl<V> Predicate<V> for spec_fn(V) -> bool {
    open spec fn predicate(&self, v: V) -> bool {
        self(v)
    }
}

} // verus!