Trait SimpleResourceInvariant 

pub trait SimpleResourceInvariant<V> {
    type Resource;

    // Required method
    spec fn inv(value: V, resource: Self::Resource) -> bool;
}

A resource invariant that does not need a constant.

Required Associated Types

type Resource

A tracked resource associated with the value and transferred linearly between owners.

Required Methods

spec fn inv(value: V, resource: Self::Resource) -> bool

Dyn Compatibility

This trait is not dyn compatible.

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

Implementors

impl<V, T: ValueInvariant<V>> SimpleResourceInvariant<V> for T

type Resource = ()