vstd
In vstd::
std_
specs::
hash
Structs
ExDefaultHasher
ExHashMap
ExHashSet
ExIter
ExKeys
ExRandomState
ExValues
IterGhostIterator
KeysGhostIterator
ValuesGhostIterator
Traits
DefaultHasherAdditionalSpecFns
ExBuildHasher
ExHasher
HashMapAdditionalSpecFns
IterAdditionalSpecFns
KeysAdditionalSpecFns
ValuesAdditionalSpecFns
Functions
_verus_external_fn_specification_61_DefaultHasher_32__58__58__32_new
_verus_external_fn_specification_62_DefaultHasher_32__58__58__32_write
_verus_external_fn_specification_63_DefaultHasher_32__58__58__32_finish
_verus_external_fn_specification_64_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_65_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_66_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_67_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_68__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_69_HashMap_32__58__58__32__60__32_Key_44__32_Value_32__62__32__58__58__32_new
_verus_external_fn_specification_70_HashMap_32__58__58__32__60__32_Key_44__32_Value_32__62__32__58__58__32_with__capacity
_verus_external_fn_specification_71_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_72_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_73_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_74_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_75_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_76_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_77_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_78_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_79_Iter_32__58__58__32__60__32__39_a_44__32_Key_32__62__32__58__58__32_next
_verus_external_fn_specification_80_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_len
_verus_external_fn_specification_81_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_is__empty
_verus_external_fn_specification_82_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__32_new
_verus_external_fn_specification_83_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__32_with__capacity
_verus_external_fn_specification_84_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_reserve
_verus_external_fn_specification_85_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_insert
_verus_external_fn_specification_86_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_contains
_verus_external_fn_specification_87_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_88_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_89_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_clear
_verus_external_fn_specification_90_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_deepview_borrow
axiom_hashmap_view_finite_dom
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_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_len
spec_hash_set_len
vstd
::
std_specs
::
hash
Function
spec_hash_map_len
Copy item path
Settings
Help
Summary
Source
pub
uninterp
fn spec_hash_map_len<Key, Value, S>(m: &
HashMap
<Key, Value, S>) ->
usize
Expand description