Struct Array8 

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

Fields

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

Implementations

impl<T> Array8<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 length5(&self) -> DafnyInt

pub fn length5_usize(&self) -> usize

pub fn length6(&self) -> DafnyInt

pub fn length6_usize(&self) -> usize

pub fn length7(&self) -> DafnyInt

pub fn length7_usize(&self) -> usize

pub fn placebos_box_usize( length0: usize, length1: usize, length2: usize, length3: usize, length4: usize, length5: usize, length6: usize, length7: usize, ) -> Box<Array8<MaybeUninit<T>>>

pub fn placebos_usize( length0: usize, length1: usize, length2: usize, length3: usize, length4: usize, length5: usize, length6: usize, length7: usize, ) -> Ptr<Array8<MaybeUninit<T>>>

pub fn placebos_usize_object( length0: usize, length1: usize, length2: usize, length3: usize, length4: usize, length5: usize, length6: usize, length7: usize, ) -> Object<Array8<MaybeUninit<T>>>

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

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

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

impl<T: Clone> Array8<T>

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