Trait RangeBoundsSpecImpl 

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

Required Methods

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

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

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

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) -> Bound<&T>

{ self.0 }

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

{ self.1 }

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

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

{ Bound::Unbounded }

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

{ Bound::Unbounded }

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

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

{ bound_as_ref(&self.0) }

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

{ bound_as_ref(&self.1) }

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

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

{ Bound::Included(self.start) }

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

{ Bound::Excluded(self.end) }

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

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

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

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

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

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

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

{ Bound::Included(self.start) }

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

{ Bound::Unbounded }

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

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

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

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

{ Bound::Unbounded }

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

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

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

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

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

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

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

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

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

{ spec_range_inclusive_end_bound(self) }

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

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

{ Bound::Unbounded }

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

{ Bound::Excluded(self.end) }

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

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

{ Bound::Unbounded }

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

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

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

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

{ Bound::Unbounded }

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

{ Bound::Included(self.end) }

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

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

{ Bound::Unbounded }

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

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

Implementors