Function extern_spec_T__slice_T_get_mut 

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

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

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

ensures

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

ensures

ix.in_bounds(self@) ==> exists<r>
                    result == Some(r) &&
                    ix.has_value(self@, *r) &&
                    ix.has_value((^self)@, ^r) &&
                    ix.resolve_elswhere(self@, (^self)@)

ensures

ix.in_bounds(self@) || result == None