Skip to main content

_verus_external_fn_specification_13__60__32__91_T_93__32__62__32__58__58__32_is__empty

vstd::slice

Function _verus_external_fn_specification_13__60__32__91_T_93__32__62__32__58__58__32_is__empty 

Source 
pub unsafe exec fn _verus_external_fn_specification_13__60__32__91_T_93__32__62__32__58__58__32_is__empty<T>(
    slice: &[T],
) -> b : bool
Expand description
ensures
b <==> slice@.len() == 0,

Specification for [<[T]>::is_empty]