Function spec_slice_getCopy item path

pub uninterp fn spec_slice_get<T: ?Sized, I: SliceIndex<T>>(
    val: &T,
    idx: I,
) -> Option<&<I as SliceIndex<T>>::Output>