Function extern_spec_T__slice_T_split_first 

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

extern spec for slice<T>::split_first

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

ghost

ensures

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