Trait OwnerOf 

pub trait OwnerOf {
    type Owner: Inv + Sized;

    // Required method
    spec fn wf(self, owner: Self::Owner) -> bool;
}

Required Associated Types

type Owner: Inv + Sized

The owner of the concrete type. The Owner must implement Inv, indicating that it must has a consistent state.

Required Methods

spec fn wf(self, owner: Self::Owner) -> bool

recommends

owner.inv(),

Dyn Compatibility

This trait is dyn compatible.

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

Implementors