pub fn extern_spec_T__slice_T_first<T>(self_: &[T]) -> Option<&T>Expand description
extern spec for slice<T>::first
This is not a real function: its only use is for documentation.
ghost
ensures
selfensures
selfpub fn extern_spec_T__slice_T_first<T>(self_: &[T]) -> Option<&T>extern spec for slice<T>::first
This is not a real function: its only use is for documentation.
ghost
ensures
selfensures
self