Skip to main content

axiom_spec_range_next_usize

vstd::std_specs::range

Function axiom_spec_range_next_usize 

Source 
pub broadcast proof fn axiom_spec_range_next_usize(range: Range<usize>)
Expand description
ensures
StepSpec::spec_is_lt(range.start, range.end)
    ==> (if let Some(n) = StepSpec::spec_forward_checked(range.start, 1) {
        spec_range_next(range) == (Range { start: n, ..range }, Some(range.start))
    } else {
        true
    }),
!StepSpec::spec_is_lt(range.start, range.end)
    ==> #[trigger] spec_range_next(range) == (range, None::<usize>),