Function extern_spec_T__slice_T_split_last_mut 

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

extern spec for slice<T>::split_last_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[self@.len() - 1] && ^l == (^self)[self@.len() - 1] &&
        r@ == self@.init() && (^r)@ == (^self)@.init()
    }
    None => self@ == Seq::empty() && *self == ^self
}