vstd_extra/external/
range.rs

1use vstd::{
2    prelude::*,
3    std_specs::cmp::{PartialOrdIs, PartialOrdSpec},
4};
5
6use core::ops::{Range, RangeInclusive};
7
8verus! {
9
10/// `Range::clone` clones each field via `Idx::clone`.
11pub assume_specification<Idx: Clone>[ Range::<Idx>::clone ](range: &Range<Idx>) -> (res: Range<Idx>)
12    ensures
13        cloned::<Idx>(range.start, res.start),
14        cloned::<Idx>(range.end, res.end),
15;
16
17/// See [`Range::is_empty`](https://doc.rust-lang.org/std/ops/struct.Range.html#method.is_empty).
18pub assume_specification<Idx: PartialOrd<Idx>>[ Range::<Idx>::is_empty ](r: &Range<Idx>) -> (res:
19    bool) where Idx: PartialOrd<Idx>
20    ensures
21        <Idx as PartialOrdSpec<Idx>>::obeys_partial_cmp_spec() ==> res == !r.start.is_lt(&r.end),
22;
23
24pub assume_specification<Idx>[ RangeInclusive::start ](r: &RangeInclusive<Idx>) -> (ret: &Idx)
25    ensures
26        *ret == r@.start,
27;
28
29pub assume_specification<Idx>[ RangeInclusive::end ](r: &RangeInclusive<Idx>) -> (ret: &Idx)
30    ensures
31        *ret == r@.end,
32;
33
34} // verus!
vstd_extra/external/range.rs

vstd_extra/external/
range.rs
