pub trait BTreeMapAdditionalSpecFns<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
recommends
self@.contains_key(k),Implementations on Foreign Types§
Source§impl<Key, Value, A: Allocator + Clone> BTreeMapAdditionalSpecFns<Key, Value> for BTreeMap<Key, Value, A>
impl<Key, Value, A: Allocator + Clone> BTreeMapAdditionalSpecFns<Key, Value> for BTreeMap<Key, Value, A>
Source§open spec fn spec_index(&self, k: Key) -> Value
open spec fn spec_index(&self, k: Key) -> Value
{ self@.index(k) }