axiom_mem_contents_unwrap_uninit_correctness

vstd_extra::array_ptr

Function axiom_mem_contents_unwrap_uninit_correctness 

Source 
pub proof fn axiom_mem_contents_unwrap_uninit_correctness<V, const N: usize>(
    arr: [MemContents<V>; N],
    res: MemContents<[V; N]>,
)
Expand description
requires
res == mem_contents_unwrap(arr),
is_mem_contents_all_uninit(arr),
ensures
res.is_uninit(),