vstd
In vstd::
std_
specs::
hash
Structs
ExDefaultHasher
ExHashMap
ExHashSet
ExIter
ExKeys
ExRandomState
IterGhostIterator
KeysGhostIterator
Traits
DefaultHasherAdditionalSpecFns
ExBuildHasher
ExHasher
HashMapAdditionalSpecFns
IterAdditionalSpecFns
KeysAdditionalSpecFns
Functions
_verus_external_fn_specification_57_DefaultHasher_32__58__58__32_new
_verus_external_fn_specification_58_DefaultHasher_32__58__58__32_write
_verus_external_fn_specification_59_DefaultHasher_32__58__58__32_finish
_verus_external_fn_specification_60_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_61_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_62_HashMap_32__58__58__32__60__32_Key_44__32_Value_32__62__32__58__58__32_new
_verus_external_fn_specification_63_HashMap_32__58__58__32__60__32_Key_44__32_Value_32__62__32__58__58__32_with__capacity
_verus_external_fn_specification_64_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_65_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_66_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_67_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_68_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_69_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_70_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_71_Iter_32__58__58__32__60__32__39_a_44__32_Key_32__62__32__58__58__32_next
_verus_external_fn_specification_72_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_len
_verus_external_fn_specification_73_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__32_new
_verus_external_fn_specification_74_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__32_with__capacity
_verus_external_fn_specification_75_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_reserve
_verus_external_fn_specification_76_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_insert
_verus_external_fn_specification_77_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_contains
_verus_external_fn_specification_78_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_79_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_80_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_clear
_verus_external_fn_specification_81_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_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
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
?
Settings
Function
vstd
::
std_specs
::
hash
::
spec_hash_set_len
Copy item path
source
·
[
−
]
pub
uninterp
fn spec_hash_set_len<Key, S>(m: &
HashSet
<Key, S>) ->
usize
Expand description