OwnerOf

vstd_extra::ownership

Trait OwnerOf 

Source 
pub trait OwnerOf
where
    <Self::Owner as View>::V: Inv,
{
    type Owner: InvView + Sized;

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

Required Associated Types§

Source

type Owner: InvView + Sized

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

Required Methods§

Source

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

recommends
owner.inv(),

Implementors§