Trait InvView 

pub trait InvView: Inv + View
where
    <Self as View>::V: Inv,
{
    // Required method
    proof fn view_preserves_inv(self);
}

Required Methods

proof fn view_preserves_inv(self)

requires

self.inv(),

ensures

self.view().inv(),

Dyn Compatibility

This trait is dyn compatible.

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

Implementors