Function extern_spec_T__slice_T_get_unchecked 

pub unsafe fn extern_spec_T__slice_T_get_unchecked<T, I: SliceIndexSpec<[T]>>(
    self_: &[T],
    ix: I,
) -> &<I as SliceIndex<[T]>>::Output

extern spec for slice<T>::get_unchecked<I>

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

requires

ix.in_bounds(self@)

ensures

ix.has_value(self@, *result)