Function extern_spec_T__slice_T_split_at_mut_checked 

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

extern spec for slice<T>::split_at_mut_checked

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

ghost

ensures

self

ensures

match result {
    Some((l, r)) => {
        mid@ <= self@.len() &&
        l@ == self@[..mid@] && r@ == self@[mid@..] &&
        (^l)@ == (^self)@[..mid@] && (^r)@ == (^self)@[mid@..]
    }
    None => mid@ > self@.len() && *self == ^self
}