Function extern_spec_T__slice_T_split_last 

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

extern spec for slice<T>::split_last

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

ghost

ensures

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