vstd::std_specs::hash

Trait HashMapAdditionalSpecFns

Source 
pub trait HashMapAdditionalSpecFns<Key, Value>: View<V = Map<Key, Value>> {
    // Required method
    spec fn spec_index(&self, k: Key) -> Value;
}

Required Methods§

Source

spec fn spec_index(&self, k: Key) -> Value

recommends
self@.contains_key(k),

Implementations on Foreign Types§

Source§

impl<Key, Value, S> HashMapAdditionalSpecFns<Key, Value> for HashMap<Key, Value, S>

Source§

open spec fn spec_index(&self, k: Key) -> Value

{ self@.index(k) }

Implementors§