Skip to main content

OccupiedEntrySpecFns

vstd::std_specs::hash

Trait OccupiedEntrySpecFns

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

Expand description

Specification for an OccupiedEntry. Contains the current key and value in the entry, and prophesies the final value after this instantiation of the entry API is complete. The final value is optional, since the user might choose to remove the entry.

Required Methods§

spec fn spec_key(self) -> K

spec fn value(self) -> 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§

impl<'a, K, V, A: Allocator> OccupiedEntrySpecFns<K, V, A> for OccupiedEntry<'a, K, V, A>

uninterp spec fn spec_key(self) -> K

uninterp spec fn value(self) -> V

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

Implementors§