Trait vstd::std_specs::hash::HashMapAdditionalSpecFns
source · pub trait HashMapAdditionalSpecFns<Key, Value>: View<V = Map<Key, Value>> {
// Required method
spec fn spec_index(&self, k: Key) -> Value;
}Required Methods§
sourcespec fn spec_index(&self, k: Key) -> Value
spec fn spec_index(&self, k: Key) -> Value
Implementations on Foreign Types§
source§impl<Key, Value, S> HashMapAdditionalSpecFns<Key, Value> for HashMap<Key, Value, S>
impl<Key, Value, S> HashMapAdditionalSpecFns<Key, Value> for HashMap<Key, Value, S>
source§open spec fn spec_index(&self, k: Key) -> Value
open spec fn spec_index(&self, k: Key) -> Value
{ self@.index(k) }