Function vstd::std_specs::range::ex_range_next

source · 
pub exec fn ex_range_next<A: Step>(range: &mut Range<A>) -> r : Option<A>
Expand description
ensures
(*range, r) == spec_range_next(*old(range)),