Trait creusot_contracts::std::slice::SliceExt

pub trait SliceExt<T> {
    // Required methods
    fn to_mut_seq(&mut self) -> Seq<&mut T>;
    fn to_ref_seq(&self) -> Seq<&T>;
}

Required Methods

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

logic

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

logic

Implementations on Foreign Types

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

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

logic

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

ensures

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

ensures

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

Implementors