pub trait EntrySpecFns<K, V, A>: Sized {
// Required methods
spec fn spec_key(self) -> K;
spec fn value(self) -> Option<V>;
spec fn final_value(self) -> Option<V>;
}Expand description
Specification for an Entry.
Contains the current key for the entry,
and prophesies the final value after this instantiation of the entry API is complete.
Required Methods§
Sourcespec fn final_value(self) -> Option<V>
spec fn final_value(self) -> Option<V>
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<'a, K, V, A: Allocator> EntrySpecFns<K, V, A> for Entry<'a, K, V, A>
impl<'a, K, V, A: Allocator> EntrySpecFns<K, V, A> for Entry<'a, K, V, A>
Source§open spec fn spec_key(self) -> K
open spec fn spec_key(self) -> K
{
match self {
Entry::Occupied(occupied_entry) => occupied_entry.spec_key(),
Entry::Vacant(vacant_entry) => vacant_entry.spec_key(),
}
}Source§open spec fn value(self) -> Option<V>
open spec fn value(self) -> Option<V>
{
match self {
Entry::Occupied(occupied_entry) => Some(occupied_entry.value()),
Entry::Vacant(vacant_entry) => None,
}
}Source§open spec fn final_value(self) -> Option<V>
open spec fn final_value(self) -> Option<V>
{
match self {
Entry::Occupied(occupied_entry) => occupied_entry.final_value(),
Entry::Vacant(vacant_entry) => vacant_entry.final_value(),
}
}