Function extern_spec_T__slice_T_last 

pub fn extern_spec_T__slice_T_last<T>(self_: &[T]) -> Option<&T>

extern spec for slice<T>::last

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

ghost

ensures

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

ensures

self