Function extern_spec_T__slice_T_split_at_checked 

pub fn extern_spec_T__slice_T_split_at_checked<T>(
    self_: &[T],
    mid: usize,
) -> Option<(&[T], &[T])>

extern spec for slice<T>::split_at_checked

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

ghost

ensures

match result {
    Some((l, r)) => mid@ <= self@.len() && l@ == self@[..mid@] && r@ == self@[mid@..],
    None => mid@ > self@.len()
}