prusti-std 0.2.0

External specifications for items in std for Prusti
Documentation
1
2
3
4
5
6
7
8
9
10
11
12
13
14
use prusti_contracts::*;

#[extern_spec]
impl<K, V, S> ::std::collections::hash_map::HashMap<K, V, S>
where
    K: Eq + ::core::hash::Hash,
    S: ::std::hash::BuildHasher,
{
    #[pure]
    pub fn contains_key<Q>(&self, k: &Q) -> bool
    where
        K: ::core::borrow::Borrow<Q>,
        Q: ::core::hash::Hash + Eq;
}