Trait Inv 

pub trait Inv {
    // Required method
    spec fn inv(self) -> bool;
}

Required Methods

spec fn inv(self) -> bool

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl<T: Inv> Inv for Option<T>

open spec fn inv(self) -> bool

{
    match self {
        Some(t) => t.inv(),
        None => true,
    }
}

Implementors

impl Inv for RcuDomainAuth

impl<'a, T> Inv for BoxPointsToRef<'a, T>

impl<L: Inv, R: Inv> Inv for Sum<L, R>

impl<T, O> Inv for RcuOwnedObject<T, O>

impl<T> Inv for ArcPointsTo<T>

impl<T> Inv for BoxPointsTo<T>

impl<T> Inv for PointsTowithDealloc<T>

impl<T> Inv for RcuBaseRetirePerm<T>

impl<T> Inv for RcuBlockInfo<T>

impl<V, I: SimpleResourceInvariant<V>> Inv for AtomicDataWithOwner<V, I>