Function extern_spec_T__slice_T_split_at 

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

extern spec for slice<T>::split_at

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

ghost

requires

self

ensures

self

ensures

self