vstd::pervasive

Trait VecAdditionalExecFns

Source 
pub trait VecAdditionalExecFns<T> {
    // Required methods
    exec fn set(&mut self, i: usize, value: T);
    exec fn set_and_swap(&mut self, i: usize, value: &mut T);
}

Required Methods§

Source

exec fn set(&mut self, i: usize, value: T)

Source

exec fn set_and_swap(&mut self, i: usize, value: &mut T)

Implementations on Foreign Types§

Source§

impl<T> VecAdditionalExecFns<T> for Vec<T>

Source§

exec fn set(&mut self, i: usize, value: T)

requires
i < old(self).len(),
ensures
self@ == old(self)@.update(i as int, value),

Replacement for self[i] = value; (which Verus does not support for technical reasons)

Source§

exec fn set_and_swap(&mut self, i: usize, value: &mut T)

requires
i < old(self).len(),
ensures
self@ == old(self)@.update(i as int, *old(value)),
*value == old(self)@.index(i as int),

Replacement for swap(&mut self[i], &mut value) (which Verus does not support for technical reasons)

Implementors§