Trait vstd::invariant::InvariantPredicate

source · 
pub trait InvariantPredicate<K, V> {
    // Required method
    spec fn inv(k: K, v: V) -> bool;
}
Expand description

Trait used to specify an invariant predicate for LocalInvariant and AtomicInvariant.

Required Methods§

source

spec fn inv(k: K, v: V) -> bool

Object Safety§

This trait is not object safe.

Implementors§

source§

impl<K, G, Pred> InvariantPredicate<(K, int), (PermissionBool, G)> for AtomicPredBool<Pred>
where Pred: AtomicInvariantPredicate<K, bool, G>,

source§

impl<K, G, Pred> InvariantPredicate<(K, int), (PermissionI8, G)> for AtomicPredI8<Pred>
where Pred: AtomicInvariantPredicate<K, i8, G>,

source§

impl<K, G, Pred> InvariantPredicate<(K, int), (PermissionI16, G)> for AtomicPredI16<Pred>
where Pred: AtomicInvariantPredicate<K, i16, G>,

source§

impl<K, G, Pred> InvariantPredicate<(K, int), (PermissionI32, G)> for AtomicPredI32<Pred>
where Pred: AtomicInvariantPredicate<K, i32, G>,

source§

impl<K, G, Pred> InvariantPredicate<(K, int), (PermissionI64, G)> for AtomicPredI64<Pred>
where Pred: AtomicInvariantPredicate<K, i64, G>,

source§

impl<K, G, Pred> InvariantPredicate<(K, int), (PermissionIsize, G)> for AtomicPredIsize<Pred>
where Pred: AtomicInvariantPredicate<K, isize, G>,

source§

impl<K, G, Pred> InvariantPredicate<(K, int), (PermissionU8, G)> for AtomicPredU8<Pred>
where Pred: AtomicInvariantPredicate<K, u8, G>,

source§

impl<K, G, Pred> InvariantPredicate<(K, int), (PermissionU16, G)> for AtomicPredU16<Pred>
where Pred: AtomicInvariantPredicate<K, u16, G>,

source§

impl<K, G, Pred> InvariantPredicate<(K, int), (PermissionU32, G)> for AtomicPredU32<Pred>
where Pred: AtomicInvariantPredicate<K, u32, G>,

source§

impl<K, G, Pred> InvariantPredicate<(K, int), (PermissionU64, G)> for AtomicPredU64<Pred>
where Pred: AtomicInvariantPredicate<K, u64, G>,

source§

impl<K, G, Pred> InvariantPredicate<(K, int), (PermissionUsize, G)> for AtomicPredUsize<Pred>
where Pred: AtomicInvariantPredicate<K, usize, G>,

source§

impl<T, K, G, Pred> InvariantPredicate<(K, int), (PermissionPtr<T>, G)> for AtomicPredPtr<T, Pred>
where Pred: AtomicInvariantPredicate<K, *mut T, G>,