Skip to main content

ExSliceIndex

vstd::slice

Trait ExSliceIndex 

Source 
pub trait ExSliceIndex<T>
where
    T: ?Sized,
{
    type ExternalTraitSpecificationFor: SliceIndex<T>;
    type Output: ?Sized;

    // Required methods
    spec fn in_bounds(&self, slice: &T) -> bool;
    exec fn index(self, slice: &T) -> &Self::Output;
    exec fn index_mut(self, slice: &mut T) -> &mut Self::Output;
    exec fn get(self, slice: &T) -> r : Option<&Self::Output>;
    exec fn get_mut(self, slice: &mut T) -> r : Option<&mut Self::Output>;
}

Required Associated Types§

Source

type ExternalTraitSpecificationFor: SliceIndex<T>

Source

type Output: ?Sized

Required Methods§

Source

spec fn in_bounds(&self, slice: &T) -> bool

Source

exec fn index(self, slice: &T) -> &Self::Output

requires
self.in_bounds(slice),
Source

exec fn index_mut(self, slice: &mut T) -> &mut Self::Output

requires
self.in_bounds(slice),
Source

exec fn get(self, slice: &T) -> r : Option<&Self::Output>

ensures
match r {
    None => !self.in_bounds(slice),
    Some(x) => self.in_bounds(slice) && call_ensures(Self::index, (self, slice), x),
},
Source

exec fn get_mut(self, slice: &mut T) -> r : Option<&mut Self::Output>

ensures
match r {
    None => !self.in_bounds(old(slice)) && &*final(slice) == &*old(slice),
    Some(x) => (
        &&& self.in_bounds(old(slice))
        &&& call_ensures(Self::index_mut, (self, slice), x)

    ),
},

Dyn Compatibility§

This trait is dyn compatible.

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

Implementors§