Trait vstd::pervasive::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§