Trait vstd::array::ArrayAdditionalExecFns

source · 
pub trait ArrayAdditionalExecFns<T> {
    // Required method
    fn set(&mut self, idx: usize, t: T);
}

Required Methods§

source

exec fn set(&mut self, idx: usize, t: T)

Implementations on Foreign Types§

source§

impl<T, const N: usize> ArrayAdditionalExecFns<T> for [T; N]

source§

exec fn set(&mut self, idx: usize, t: T)

requires
0 <= idx < N,
ensures
self@ == old(self)@.update(idx as int, t),

Implementors§