Skip to main content

slice_range_end

vstd::std_specs::range

Function slice_range_end 

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

Normalized (exclusive) end index of a range over a sequence of length len, matching std’s core::slice::range: an inclusive bound i becomes i + 1, an exclusive bound i stays i, and an unbounded end is len.