Trait IndexSetTrustedSpecCopy item path

pub trait IndexSetTrustedSpec<Idx>: IndexMut<Idx> + TrustedSpecSealed {
    // Required methods
    spec fn spec_index_set_requires(&self, index: Idx) -> bool;
    spec fn spec_index_set_ensures(
        &self,
        new_container: &Self,
        index: Idx,
        val: Self::Output,
    ) -> bool
       where Self::Output: Sized;
}

Required Methods§

Dyn Compatibility§

Implementations on Foreign Types§

{ 0 <= index < self@.len() }

{ new_container@ == self@.update(index as int, val) }

{ 0 <= index < self.len() }

{ new_container@ === self@.update(index as int, val) }

{ 0 <= index < N }

{ new_container@ === self@.update(index as int, val) }

Implementors§