Trait InvView Copy item path

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

Required Methods§

self.inv(),

self.view().inv(),

Implementors§