Skip to main content

slice_range_start

vstd::std_specs::range

Function slice_range_start 

Source 
pub open spec fn slice_range_start<R: RangeBoundsSpec<usize>>(range: &R) -> int
Expand description
{
    match range.spec_start_bound() {
        SpecBound::Included(i) => *i as int,
        SpecBound::Excluded(i) => (*i as int) + 1,
        SpecBound::Unbounded => 0,
    }
}

Normalized (inclusive) start index of range, matching std’s core::slice::range: an inclusive bound i stays i, an exclusive bound i becomes i + 1, and an unbounded start is 0.