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(&mut self) -> (*mut T, Ghost<&mut Perm<*const [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]>>)

terminates

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

terminates

Implementations on Foreign Types

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

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

(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>

(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()

erasure

Self::as_ptr

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

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

terminates

ensures

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

ensures

&*self == result.1.val()

ensures

&^self == (^result.1).val()

erasure

Self::as_mut_ptr

Implementors