Skip to main content

ValueInvariant

vstd_extra::resource_invariant

Trait ValueInvariant 

Source 
pub trait ValueInvariant<V> {
    // Required method
    spec fn inv(value: V) -> bool;
}
Expand description

A resource invariant that only considers the value.

Required Methods§

Source

spec fn inv(value: V) -> bool

Dyn Compatibility§

This trait is not dyn compatible.

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

Implementors§