vstd/
predicate.rs

1#![allow(unused_imports)]
2
3use super::pervasive::*;
4use super::prelude::*;
5
6verus! {
7
8pub trait Predicate<V> {
9    spec fn predicate(&self, v: V) -> bool;
10}
11
12impl<V> Predicate<V> for spec_fn(V) -> bool {
13    open spec fn predicate(&self, v: V) -> bool {
14        self(v)
15    }
16}
17
18} // verus!