Struct Array7 

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

Fields

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

Implementations

impl<T> Array7<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 placebos_box_usize( length0: usize, length1: usize, length2: usize, length3: usize, length4: usize, length5: usize, length6: usize, ) -> Box<Array7<MaybeUninit<T>>>

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

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

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

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

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

impl<T: Clone> Array7<T>

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