axiom_hashmap_decreases

vstd::std_specs::hash

Function axiom_hashmap_decreases 

Source 
pub broadcast proof fn axiom_hashmap_decreases<Key, Value, S>(m: HashMap<Key, Value, S>)
Expand description
ensures
#[trigger] (decreases_to!(m => m @)),