vstd
In vstd::
std_
specs::
hash
Structs
ExDefaultHasher
ExHashMap
ExHashSet
ExKeys
ExMapIter
ExRandomState
ExSetIter
ExValues
KeysGhostIterator
MapIterGhostIterator
SetIterGhostIterator
ValuesGhostIterator
Traits
DefaultHasherAdditionalSpecFns
ExBuildHasher
ExHasher
HashMapAdditionalSpecFns
KeysAdditionalSpecFns
MapIterAdditionalSpecFns
SetIterAdditionalSpecFns
ValuesAdditionalSpecFns
Functions
_verus_external_fn_specification_204_DefaultHasher_32__58__58__32_new
_verus_external_fn_specification_205_DefaultHasher_32__58__58__32_write
_verus_external_fn_specification_206_DefaultHasher_32__58__58__32_finish
_verus_external_fn_specification_207_Keys_32__58__58__32__60__32__39_a_44__32_Key_44__32_Value_32__62__32__58__58__32_next
_verus_external_fn_specification_208_Values_32__58__58__32__60__32__39_a_44__32_Key_44__32_Value_32__62__32__58__58__32_next
_verus_external_fn_specification_209_hash__map_32__58__58__32_Iter_32__58__58__32__60__32__39_a_44__32_Key_44__32_Value_32__62__32__58__58__32_next
_verus_external_fn_specification_210_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_iter
_verus_external_fn_specification_211_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_len
_verus_external_fn_specification_212_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_is__empty
_verus_external_fn_specification_213__60__32_HashMap_32__58__58__32__60__32_K_44__32_V_44__32_S_32__62__32_as_32_Clone_32__62__32__58__58__32_clone
_verus_external_fn_specification_214_HashMap_32__58__58__32__60__32_Key_44__32_Value_32__62__32__58__58__32_new
_verus_external_fn_specification_215_HashMap_32__58__58__32__60__32_Key_44__32_Value_32__62__32__58__58__32_with__capacity
_verus_external_fn_specification_216_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_44__32__62__32__58__58__32_reserve
_verus_external_fn_specification_217_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_insert
_verus_external_fn_specification_218_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_contains__key_32__58__58__32__60__32_Q_32__62_
_verus_external_fn_specification_219_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_get_32__58__58__32__60__32_Q_32__62_
_verus_external_fn_specification_220_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_remove_32__58__58__32__60__32_Q_32__62_
_verus_external_fn_specification_221_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_clear
_verus_external_fn_specification_222_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_keys
_verus_external_fn_specification_223_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_values
_verus_external_fn_specification_224_hash__set_32__58__58__32_Iter_32__58__58__32__60__32__39_a_44__32_Key_32__62__32__58__58__32_next
_verus_external_fn_specification_225_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_len
_verus_external_fn_specification_226_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_is__empty
_verus_external_fn_specification_227_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__32_new
_verus_external_fn_specification_228_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__32_with__capacity
_verus_external_fn_specification_229_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_reserve
_verus_external_fn_specification_230_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_insert
_verus_external_fn_specification_231_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_contains
_verus_external_fn_specification_232_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_get_32__58__58__32__60__32_Q_32__62_
_verus_external_fn_specification_233_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_remove_32__58__58__32__60__32_Q_32__62_
_verus_external_fn_specification_234_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_clear
_verus_external_fn_specification_235_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_iter
axiom_bool_obeys_hash_table_key_model
axiom_box_bool_obeys_hash_table_key_model
axiom_box_integer_type_obeys_hash_table_key_model
axiom_box_key_removed
axiom_contains_box
axiom_contains_deref_key
axiom_deref_key_removed
axiom_hashmap_decreases
axiom_hashmap_deepview_borrow
axiom_hashmap_view_finite_dom
axiom_hashset_decreases
axiom_i128_obeys_hash_table_key_model
axiom_i164_obeys_hash_table_key_model
axiom_i16_obeys_hash_table_key_model
axiom_i32_obeys_hash_table_key_model
axiom_i8_obeys_hash_table_key_model
axiom_isize_obeys_hash_table_key_model
axiom_maps_box_key_to_value
axiom_maps_deref_key_to_value
axiom_random_state_builds_valid_hashers
axiom_set_box_key_removed
axiom_set_box_key_to_value
axiom_set_contains_box
axiom_set_contains_deref_key
axiom_set_deref_key_removed
axiom_set_deref_key_to_value
axiom_spec_hash_map_iter
axiom_spec_hash_map_len
axiom_spec_hash_set_len
axiom_u128_obeys_hash_table_key_model
axiom_u16_obeys_hash_table_key_model
axiom_u32_obeys_hash_table_key_model
axiom_u64_obeys_hash_table_key_model
axiom_u8_obeys_hash_table_key_model
axiom_usize_obeys_hash_table_key_model
borrowed_key_removed
builds_valid_hashers
contains_borrowed_key
group_hash_axioms
hash_map_deep_view_impl
lemma_hashmap_deepview_dom
lemma_hashmap_deepview_properties
lemma_hashmap_deepview_values
maps_borrowed_key_to_value
obeys_key_model
set_contains_borrowed_key
sets_borrowed_key_to_key
sets_differ_by_borrowed_key
spec_hash_map_iter
spec_hash_map_len
spec_hash_set_len
vstd
::
std_specs
::
hash
Function
set_contains_borrowed_key
Copy item path
Settings
Help
Summary
Source
pub
uninterp
fn set_contains_borrowed_key<Key, Q: ?
Sized
>(m:
Set
<Key>, k:
&Q
) ->
bool
Expand description