pub trait ExRangeBounds<T: ?Sized> {
type ExternalTraitSpecificationFor: RangeBounds<T>;
// Required methods
spec fn spec_start_bound(&self) -> SpecBound<&T>;
spec fn spec_end_bound(&self) -> SpecBound<&T>;
exec fn start_bound(&self) -> Bound<&T>;
exec fn end_bound(&self) -> Bound<&T>;
}Expand description
Specification for core::ops::RangeBounds, exposing spec-mode models
spec_start_bound and
spec_end_bound of the trait’s
start_bound/end_bound methods. This mirrors std’s normalization of an
arbitrary range into a pair of bounds and is the model used by
<[T]>::copy_within (see vstd::std_specs::slice).