Function extern_spec_T__slice_T_split_first_mut 

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

extern spec for slice<T>::split_first_mut

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

ghost

ensures

self

ensures

match result {
    Some((l, r)) => {
        1 <= self@.len() &&
        *l == self[0] && ^l == (^self)[0] && r@ == self@[1..] && (^r)@ == (^self)@[1..]
    }
    None => self@ == Seq::empty() && *self == ^self
}