Function extern_spec_T_I_Index_I__slice_T_index 

pub fn extern_spec_T_I_Index_I__slice_T_index<T, I: SliceIndexSpec<[T]>>(
    self_: &[T],
    ix: I,
) -> &<[T] as Index<I>>::Output 

extern spec for [slice<T>::index]

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

terminates

ghost

requires

ix.in_bounds(self@)

ensures

ix.has_value(self@, *result)