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