Function extern_spec_T__slice_T_split_off_last_mut 

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

extern spec for slice<T>::split_off_last_mut

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

ghost

ensures

(^*self)@.len() == (**self)@.len()

ensures

(^^self)@.len() == (*^self)@.len()

ensures

match result {
    Some(r) => {
        (**self)@.len() > 0 &&
        r == &mut (**self)[(**self)@.len()-1] &&
        (^self).to_mut_seq() == (*self).to_mut_seq().subsequence(0, (*self).to_mut_seq().len()-1)
    }
    None => resolve(self) && (^*self)@ == Seq::empty() && (**self)@ == Seq::empty()
}