Trait RCClone Copy item path

pub trait RCClone: Sized {
    // Required methods
    spec fn clone_requires(self, perm: MetaRegionOwners) -> bool;
    spec fn clone_ensures(
        self,
        old_perm: MetaRegionOwners,
        new_perm: MetaRegionOwners,
        res: Self,
    ) -> bool;
    exec fn clone(&self, Tracked(perm): Tracked<&mut MetaRegionOwners>) -> res : Self;
}

Required Methods§

self.clone_requires(*old(perm)),

res == *self,

self.clone_ensures(*old(perm), *final(perm), res),

final(perm).inv(),

final(perm).slots =~= old(perm).slots,

final(perm).slot_owners.dom() =~= old(perm).slot_owners.dom(),

Dyn Compatibility§

Implementors§