Skip to main content

borrowed_key_mutated

vstd_extra::external::btree

Function borrowed_key_mutated 

Source 
pub open spec fn borrowed_key_mutated<Key, Value, Q: ?Sized>(
    old_map: Map<Key, Value>,
    new_map: Map<Key, Value>,
    key: &Q,
    old_value: Value,
    new_value: Value,
) -> bool
Expand description
{
    &&& maps_borrowed_key_to_value(old_map, key, old_value)
    &&& maps_borrowed_key_to_value(new_map, key, new_value)
    &&& exists |remainder: Map<Key, Value>| {
        &&& borrowed_key_removed(old_map, remainder, key)
        &&& borrowed_key_removed(new_map, remainder, key)

    }

}

Relates a map before and after mutating the value selected by a borrowed key.