Skip to main content

range_usize_is_empty

vstd_extra::external::range

Function range_usize_is_empty 

Source 
pub exec fn range_usize_is_empty(r: &Range<usize>) -> ret : bool
Expand description
ensures
ret == range_usize_is_empty_spec(r),

Exec-mode is_empty for a Range<usize>: use in place of r.is_empty() which needs Idx: PartialOrd<Idx> bound that doesn’t round-trip cleanly through assume_specification.