Skip to main content

extern_spec_T__slice_T_is_empty

creusot_std::std::slice

Function extern_spec_T__slice_T_is_empty 

Source 
pub fn extern_spec_T__slice_T_is_empty<T>(self_: &[T]) -> bool
Expand description

extern spec for slice<T>::is_empty

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

ghost

ensures 

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