Skip to main content

SliceAdditionalExecFns

vstd::slice

Trait SliceAdditionalExecFns 

Source 
pub trait SliceAdditionalExecFns<T> {
    // Required method
    exec fn set(&mut self, idx: usize, t: T);
}

Required Methods§

Source

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

👎Deprecated: use slice[i] = value instead

Implementations on Foreign Types§

Source§

impl<T> SliceAdditionalExecFns<T> for [T]

Source§

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

👎Deprecated: use slice[i] = value instead
requires
0 <= idx < old(self)@.len(),
ensures
final(self)@ == old(self)@.update(idx as int, t),

Implementors§