Skip to main content

range_usize_len

vstd_extra::external::range

Function range_usize_len 

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

Exec-mode len for a Range<usize>: use in place of r.len() which is an ExactSizeIterator provided method and can’t be specced with assume_specification.