Function extern_spec_T__slice_T_get 

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

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

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

ensures

ix.in_bounds(self@) ==> exists<r> result == Some(r) && ix.has_value(self@, *r)

ensures

ix.in_bounds(self@) || result == None