Function vstd::std_specs::range::axiom_spec_range_next_u16

source ·

pub broadcast proof fn axiom_spec_range_next_u16(range: Range<u16>)

Expand description

ensures

range.start.spec_is_lt(range.end)
    ==> (if let Some(n) = range.start.spec_forward_checked(1) {
        spec_range_next(range) == (Range { start: n, ..range }, Some(range.start))
    } else {
        true
    }),

!range.start.spec_is_lt(range.end)
    ==> #[trigger] spec_range_next(range) == (range, None::<u16>),