Function extern_spec_T__slice_T_split_at_mut 

pub fn extern_spec_T__slice_T_split_at_mut<T>(
    self_: &mut [T],
    mid: usize,
) -> (&mut [T], &mut [T])

extern spec for slice<T>::split_at_mut

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

ghost

requires

self

ensures

self@.len();
((^self)@.len() == sl) &&
self@.subsequence(0, mid@) == l@ &&
self