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.

terminates

ghost

requires

mid@ <= self@.len()

ensures

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