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§
Sourcespec fn spec_index_set_requires(&self, index: Idx) -> bool
spec fn spec_index_set_requires(&self, index: Idx) -> bool
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.
Implementations on Foreign Types§
Source§impl<T> IndexSetTrustedSpec<usize> for [T]
impl<T> IndexSetTrustedSpec<usize> for [T]
Source§open spec fn spec_index_set_requires(&self, index: usize) -> bool
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
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>
impl<T, A: Allocator> IndexSetTrustedSpec<usize> for Vec<T, A>
Source§open spec fn spec_index_set_requires(&self, index: usize) -> bool
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
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]
impl<T, const N: usize> IndexSetTrustedSpec<usize> for [T; N]
Source§open spec fn spec_index_set_requires(&self, index: usize) -> bool
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
open spec fn spec_index_set_ensures( &self, new_container: &Self, index: usize, val: T, ) -> bool
{ new_container@ === self@.update(index as int, val) }