Function extern_spec_T__slice_T_first 

pub 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.

terminates

ghost

ensures

result == None ==> self@.len() == 0

ensures

forall<x> result == Some(x) ==> self[0] == *x