Skip to main content

RangeBoundsSpecImpl

vstd::std_specs::range

Trait RangeBoundsSpecImpl

pub trait RangeBoundsSpecImpl<T: ?Sized>: RangeBounds<T> {
    // Required methods
    exec fn spec_start_bound(&self) -> SpecBound<&T>;
    exec fn spec_end_bound(&self) -> SpecBound<&T>;
}

Required Methods§

exec fn spec_start_bound(&self) -> SpecBound<&T>

exec fn spec_end_bound(&self) -> SpecBound<&T>

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementations on Foreign Types§

impl<'a, T: ?Sized + 'a> RangeBoundsSpecImpl<T> for (Bound<&'a T>, Bound<&'a T>)

open spec fn spec_start_bound(&self) -> SpecBound<&T>

{
    match self.0 {
        Bound::Included(start) => SpecBound::Included(start),
        Bound::Excluded(start) => SpecBound::Excluded(start),
        Bound::Unbounded => SpecBound::Unbounded,
    }
}

open spec fn spec_end_bound(&self) -> SpecBound<&T>

{
    match self.1 {
        Bound::Included(end) => SpecBound::Included(end),
        Bound::Excluded(end) => SpecBound::Excluded(end),
        Bound::Unbounded => SpecBound::Unbounded,
    }
}

impl<T> RangeBoundsSpecImpl<T> for (Bound<T>, Bound<T>)

open spec fn spec_start_bound(&self) -> SpecBound<&T>

{ spec_bound_ref(&self.0) }

open spec fn spec_end_bound(&self) -> SpecBound<&T>

{ spec_bound_ref(&self.1) }

impl<T> RangeBoundsSpecImpl<T> for Range<&T>

open spec fn spec_start_bound(&self) -> SpecBound<&T>

{ SpecBound::Included(self.start) }

open spec fn spec_end_bound(&self) -> SpecBound<&T>

{ SpecBound::Excluded(self.end) }

impl<T> RangeBoundsSpecImpl<T> for Range<T>

open spec fn spec_start_bound(&self) -> SpecBound<&T>

{ SpecBound::Included(&self.start) }

open spec fn spec_end_bound(&self) -> SpecBound<&T>

{ SpecBound::Excluded(&self.end) }

impl<T> RangeBoundsSpecImpl<T> for RangeFrom<&T>

open spec fn spec_start_bound(&self) -> SpecBound<&T>

{ SpecBound::Included(self.start) }

open spec fn spec_end_bound(&self) -> SpecBound<&T>

{ SpecBound::Unbounded }

impl<T> RangeBoundsSpecImpl<T> for RangeFrom<T>

open spec fn spec_start_bound(&self) -> SpecBound<&T>

{ SpecBound::Included(&self.start) }

open spec fn spec_end_bound(&self) -> SpecBound<&T>

{ SpecBound::Unbounded }

impl<T> RangeBoundsSpecImpl<T> for RangeInclusive<&T>

open spec fn spec_start_bound(&self) -> SpecBound<&T>

{ SpecBound::Included(self@.start) }

open spec fn spec_end_bound(&self) -> SpecBound<&T>

{ SpecBound::Included(self@.end) }

impl<T> RangeBoundsSpecImpl<T> for RangeInclusive<T>

open spec fn spec_start_bound(&self) -> SpecBound<&T>

{ SpecBound::Included(&self@.start) }

open spec fn spec_end_bound(&self) -> SpecBound<&T>

{ SpecBound::Included(&self@.end) }

impl<T> RangeBoundsSpecImpl<T> for RangeTo<&T>

open spec fn spec_start_bound(&self) -> SpecBound<&T>

{ SpecBound::Unbounded }

open spec fn spec_end_bound(&self) -> SpecBound<&T>

{ SpecBound::Excluded(self.end) }

impl<T> RangeBoundsSpecImpl<T> for RangeTo<T>

open spec fn spec_start_bound(&self) -> SpecBound<&T>

{ SpecBound::Unbounded }

open spec fn spec_end_bound(&self) -> SpecBound<&T>

{ SpecBound::Excluded(&self.end) }

impl<T> RangeBoundsSpecImpl<T> for RangeToInclusive<&T>

open spec fn spec_start_bound(&self) -> SpecBound<&T>

{ SpecBound::Unbounded }

open spec fn spec_end_bound(&self) -> SpecBound<&T>

{ SpecBound::Included(self.end) }

impl<T> RangeBoundsSpecImpl<T> for RangeToInclusive<T>

open spec fn spec_start_bound(&self) -> SpecBound<&T>

{ SpecBound::Unbounded }

open spec fn spec_end_bound(&self) -> SpecBound<&T>

{ SpecBound::Included(&self.end) }

impl<T: ?Sized> RangeBoundsSpecImpl<T> for RangeFull

open spec fn spec_start_bound(&self) -> SpecBound<&T>

{ SpecBound::Unbounded }

open spec fn spec_end_bound(&self) -> SpecBound<&T>

{ SpecBound::Unbounded }

Implementors§