Function extern_spec_T__slice_T_get_unchecked_mut 

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

extern spec for slice<T>::get_unchecked_mut<I>

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

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()