prusti_std/lib.rs
1use prusti_contracts::*;
2
3#[extern_spec]
4impl<K, V, S> ::std::collections::hash_map::HashMap<K, V, S>
5where
6 K: Eq + ::core::hash::Hash,
7 S: ::std::hash::BuildHasher,
8{
9 #[pure]
10 pub fn contains_key<Q>(&self, k: &Q) -> bool
11 where
12 K: ::core::borrow::Borrow<Q>,
13 Q: ::core::hash::Hash + Eq;
14}