Trait SliceIndexSpec 

pub trait SliceIndexSpec<T>: SliceIndex<T>
where
    T: View + ?Sized,
{
    // Required methods
    fn in_bounds(self, seq: T::ViewTy) -> bool;
    fn has_value(self, seq: T::ViewTy, out: Self::Output) -> bool;
    fn resolve_elswhere(self, old: T::ViewTy, fin: T::ViewTy) -> bool;
}

Required Methods

fn in_bounds(self, seq: T::ViewTy) -> bool

logic

fn has_value(self, seq: T::ViewTy, out: Self::Output) -> bool

logic

fn resolve_elswhere(self, old: T::ViewTy, fin: T::ViewTy) -> bool

logic

Dyn Compatibility

This trait is dyn compatible.

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

Implementations on Foreign Types

impl<T> SliceIndexSpec<[T]> for (Bound<usize>, Bound<usize>)

fn in_bounds(self, seq: Seq<T>) -> bool

logic(open)

let range = to_logic_range(self, seq.len());
pearlite! { range.start <= range.end && range.end <= seq.len() }

fn has_value(self, seq: Seq<T>, out: [T]) -> bool

logic(open)

let range = to_logic_range(self, seq.len());
pearlite! { seq.subsequence(range.start, range.end) == out@ }

fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool

logic(open)

let range = to_logic_range(self, old.len());
pearlite! {
    forall<i> 0 <= i && (i < range.start || range.end <= i) && i < old.len()
    ==> old[i] == fin[i]
}

impl<T> SliceIndexSpec<[T]> for Range<usize>

fn in_bounds(self, seq: Seq<T>) -> bool

logic(open)

self.start@ <= self.end@ && self.end@ <= seq.len()

fn has_value(self, seq: Seq<T>, out: [T]) -> bool

logic(open)

seq.subsequence(self.start@, self.end@) == out@

fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool

logic(open)

forall<i> 0 <= i && (i < self.start@ || self.end@ <= i) && i < old.len()
==> old[i] == fin[i]

impl<T> SliceIndexSpec<[T]> for RangeFrom<usize>

fn in_bounds(self, seq: Seq<T>) -> bool

logic(open)

self.start@ <= seq.len()

fn has_value(self, seq: Seq<T>, out: [T]) -> bool

logic(open)

seq.subsequence(self.start@, seq.len()) == out@

fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool

logic(open)

forall<i> 0 <= i && i < self.start@ && i < old.len() ==> old[i] == fin[i]

impl<T> SliceIndexSpec<[T]> for RangeFull

fn in_bounds(self, _seq: Seq<T>) -> bool

logic(open)

true

fn has_value(self, seq: Seq<T>, out: [T]) -> bool

logic(open)

seq == out@

fn resolve_elswhere(self, _old: Seq<T>, _fin: Seq<T>) -> bool

logic(open)

true

impl<T> SliceIndexSpec<[T]> for RangeInclusive<usize>

fn in_bounds(self, seq: Seq<T>) -> bool

logic(opaque)

ensures

self.end_log()@ < seq.len() && self.start_log()@ <= self.end_log()@+1 ==> result

ensures

self.end_log()@ >= seq.len() ==> !result

fn has_value(self, seq: Seq<T>, out: [T]) -> bool

logic(open)

if self.is_empty_log() { out@ == Seq::empty() }
else { seq.subsequence(self.start_log()@, self.end_log()@ + 1) == out@ }

fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool

logic(open)

forall<i> 0 <= i
    && (i < self.start_log()@ || self.end_log()@ < i || self.is_empty_log())
    && i < old.len()
    ==> old[i] == fin[i]

impl<T> SliceIndexSpec<[T]> for RangeTo<usize>

fn in_bounds(self, seq: Seq<T>) -> bool

logic(open)

self.end@ <= seq.len()

fn has_value(self, seq: Seq<T>, out: [T]) -> bool

logic(open)

seq.subsequence(0, self.end@) == out@

fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool

logic(open)

forall<i> self.end@ <= i && i < old.len() ==> old[i] == fin[i]

impl<T> SliceIndexSpec<[T]> for RangeToInclusive<usize>

fn in_bounds(self, seq: Seq<T>) -> bool

logic(open)

self.end@ < seq.len()

fn has_value(self, seq: Seq<T>, out: [T]) -> bool

logic(open)

seq.subsequence(0, self.end@ + 1) == out@

fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool

logic(open)

forall<i> self.end@ < i && i < old.len() ==> old[i] == fin[i]

impl<T> SliceIndexSpec<[T]> for usize

fn in_bounds(self, seq: Seq<T>) -> bool

logic(open, inline)

self@ < seq.len()

fn has_value(self, seq: Seq<T>, out: T) -> bool

logic(open, inline)

seq[self@] == out

fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool

logic(open, inline)

forall<i> 0 <= i && i != self@ && i < old.len() ==> old[i] == fin[i]

Implementors