Trait vstd::std_specs::core::IndexSetTrustedSpec

source · 
pub trait IndexSetTrustedSpec<Idx>: IndexMut<Idx> + TrustedSpecSealed {
    // Required methods
    spec fn spec_index_set_requires(&self, index: Idx) -> bool;
    spec fn spec_index_set_ensures(
        &self,
        new_container: &Self,
        index: Idx,
        val: Self::Output,
    ) -> bool
       where Self::Output: Sized;
}

Required Methods§

source

spec fn spec_index_set_requires(&self, index: Idx) -> bool

source

spec fn spec_index_set_ensures( &self, new_container: &Self, index: Idx, val: Self::Output, ) -> bool
where Self::Output: Sized,

Object Safety§

This trait is not object safe.

Implementations on Foreign Types§

source§

impl<T> IndexSetTrustedSpec<usize> for [T]

source§

open spec fn spec_index_set_requires(&self, index: usize) -> bool

{ 0 <= index < self@.len() }
source§

open spec fn spec_index_set_ensures( &self, new_container: &Self, index: usize, val: T, ) -> bool

{ new_container@ == self@.update(index as int, val) }
source§

impl<T, A: Allocator> IndexSetTrustedSpec<usize> for Vec<T, A>

source§

open spec fn spec_index_set_requires(&self, index: usize) -> bool

{ 0 <= index < self.len() }
source§

open spec fn spec_index_set_ensures( &self, new_container: &Self, index: usize, val: T, ) -> bool

{ new_container@ === self@.update(index as int, val) }
source§

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

source§

open spec fn spec_index_set_requires(&self, index: usize) -> bool

{ 0 <= index < N }
source§

open spec fn spec_index_set_ensures( &self, new_container: &Self, index: usize, val: T, ) -> bool

{ new_container@ === self@.update(index as int, val) }

Implementors§