Function vstd::std_specs::core::index_set

source · 
pub exec fn index_set<T, Idx, E>(container: &mut T, index: Idx, val: E)
where
    T: ?Sized + IndexMut<Idx> + Index<Idx, Output = E> + IndexSetTrustedSpec<Idx>,
Expand description
requires
old(container).spec_index_set_requires(index),
ensures
old(container).spec_index_set_ensures(container, index, val),