Struct Array5 

pub struct Array5<T> {
    pub data: Box<[Box<[Box<[Box<[Box<[T]>]>]>]>]>,
    /* private fields */
}

Fields

data: Box<[Box<[Box<[Box<[Box<[T]>]>]>]>]>

Implementations

impl<T> Array5<T>

pub fn length0(&self) -> DafnyInt

pub fn length0_usize(&self) -> usize

pub fn length1(&self) -> DafnyInt

pub fn length1_usize(&self) -> usize

pub fn length2(&self) -> DafnyInt

pub fn length2_usize(&self) -> usize

pub fn length3(&self) -> DafnyInt

pub fn length3_usize(&self) -> usize

pub fn length4(&self) -> DafnyInt

pub fn length4_usize(&self) -> usize

pub fn placebos_box_usize( length0: usize, length1: usize, length2: usize, length3: usize, length4: usize, ) -> Box<Array5<MaybeUninit<T>>>

pub fn placebos_usize( length0: usize, length1: usize, length2: usize, length3: usize, length4: usize, ) -> Ptr<Array5<MaybeUninit<T>>>

pub fn placebos_usize_object( length0: usize, length1: usize, length2: usize, length3: usize, length4: usize, ) -> Object<Array5<MaybeUninit<T>>>

pub fn placebos( length0: &DafnyInt, length1: &DafnyInt, length2: &DafnyInt, length3: &DafnyInt, length4: &DafnyInt, ) -> Ptr<Array5<MaybeUninit<T>>>

pub fn construct(p: Ptr<Array5<MaybeUninit<T>>>) -> Ptr<Array5<T>>

pub fn construct_object(p: Object<Array5<MaybeUninit<T>>>) -> Object<Array5<T>>

impl<T: Clone> Array5<T>

pub fn to_vec(&self) -> Vec<Vec<Vec<Vec<Vec<T>>>>>