Skip to main content

VacantEntrySpecFns

vstd::std_specs::hash

Trait VacantEntrySpecFns 

Source 
pub trait VacantEntrySpecFns<K, V, A>: Sized {
    // Required methods
    spec fn spec_key(self) -> K;
    spec fn final_value(self) -> Option<V>;
}
Expand description

Specification for a VacantEntry. Contains the current key for the entry, and prophesies the final value after this instantiation of the entry API is complete. The final value is optional, since the user may or may not choose to insert a value.

Required Methods§

Source

spec fn spec_key(self) -> K

Source

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> VacantEntrySpecFns<K, V, A> for VacantEntry<'a, K, V, A>

Source§

uninterp spec fn spec_key(self) -> K

Source§

uninterp spec fn final_value(self) -> Option<V>

Implementors§