ModelOf

vstd_extra::ownership

Trait ModelOf 

Source 
pub trait ModelOf: OwnerOf + Sized {
    // Provided method
    open spec fn model(self, owner: Self::Owner) -> <Self::Owner as View>::V { ... }
}

Provided Methods§

Source

open spec fn model(self, owner: Self::Owner) -> <Self::Owner as View>::V

recommends
self.wf(owner),
{ owner.view() }

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§