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§

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§