Trait SliceExt 

pub trait SliceExt<T> {
    // Required methods
    fn to_mut_seq(&mut self) -> Seq<&mut T>;
    fn to_ref_seq(&self) -> Seq<&T>;
    fn as_ptr_perm(&self) -> (*const T, Ghost<&Perm<*const [T]>>);
    fn as_mut_ptr_perm<'a>(
        &'a mut self,
    ) -> (*mut T, Ghost<GuardedBorrow<'a, Perm<*const [T]>>>);
}

Required Methods

fn to_mut_seq(&mut self) -> Seq<&mut T>

logic

fn to_ref_seq(&self) -> Seq<&T>

logic

fn as_ptr_perm(&self) -> (*const T, Ghost<&Perm<*const [T]>>)

terminates

fn as_mut_ptr_perm<'a>( &'a mut self, ) -> (*mut T, Ghost<GuardedBorrow<'a, Perm<*const [T]>>>)

terminates

Dyn Compatibility

This trait is dyn compatible.

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

Implementations on Foreign Types

impl<T> SliceExt<T> for [T]

fn to_mut_seq(&mut self) -> Seq<&mut T>

logic(opaque)

ensures

result.len() == self@.len()

ensures

forall<i> 0 <= i && i < result.len() ==> result[i] == &mut self[i]

fn to_ref_seq(&self) -> Seq<&T>

logic(opaque)

ensures

result.len() == self@.len()

ensures

forall<i> 0 <= i && i < result.len() ==> result[i] == &self[i]

fn as_ptr_perm(&self) -> (*const T, Ghost<&Perm<*const [T]>>)

Convert &[T] to *const T and a shared ownership token.

terminates

ensures

result.0 == *result.1.ward() as *const T

ensures

self == result.1.val_unsized()

erasure

Self::as_ptr

fn as_mut_ptr_perm<'a>( &'a mut self, ) -> (*mut T, Ghost<GuardedBorrow<'a, Perm<*const [T]>>>)

Convert &mut [T] to *mut T and a mutable ownership token.

terminates

ensures

result.1.guard() == |b: &mut Perm<*const [T]>| {
    *b.ward() as *const T == result.0 as *const T &&
    b.ward().len_logic()@ == self@.len()
 }

ensures

*self == *result.1.borrow.val_unsized()

ensures

^self == *(^result.1.borrow).val_unsized()

erasure

Self::as_mut_ptr

Implementors