ptr_ref_at

vstd_extra::array_ptr

Function ptr_ref_at 

Source 
pub exec fn ptr_ref_at<V, const N: usize>(
    ptr: *mut [V; N],
    verus_tmp_perm: Tracked<&PointsToArray<V, N>>,
    index: usize,
) -> res : &V
Expand description
requires
perm.ptr() == ptr,
perm.is_init(index as int),
ensures
res == perm.opt_value()[index as int].value(),

Get the immutable reference of the value at the index