Function extern_spec_T_I_IndexMut_I__slice_T_index_mut 

pub fn extern_spec_T_I_IndexMut_I__slice_T_index_mut<T, I: SliceIndexSpec<[T]>>(
    self_: &mut [T],
    ix: I,
) -> &mut <[T] as Index<I>>::Output 

extern spec for [slice<T>::index_mut]

This is not a real function: its only use is for documentation.

terminates

ghost

requires

ix.in_bounds(self@)

ensures

ix.has_value(self@, *result)

ensures

ix.has_value((&^self)@, ^result)

ensures

ix.resolve_elswhere(self@, (&^self)@)

ensures

(&^self)@.len() == self@.len()