Add extend to HashMap and StringHashMap (#1295)

verus-lang · Oct 17, 2024 · aa8b423 · aa8b423
1 parent e4c33bf
commit aa8b423
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/source/vstd/hash_map.rs b/source/vstd/hash_map.rs
@@ -110,6 +110,14 @@ impl<Key, Value> HashMapWithView<Key, Value> where Key: View + Eq + Hash {
     {
         self.m.clear()
     }
+
+    #[verifier::external_body]
+    pub fn union_prefer_right(&mut self, other: Self)
+        ensures
+            self@ == old(self)@.union_prefer_right(other@),
+    {
+        self.m.extend(other.m)
+    }
 }
 
 pub broadcast proof fn axiom_hash_map_with_view_spec_len<Key, Value>(
@@ -211,6 +219,14 @@ impl<Value> StringHashMap<Value> {
     {
         self.m.clear()
     }
+
+    #[verifier::external_body]
+    pub fn union_prefer_right(&mut self, other: Self)
+        ensures
+            self@ == old(self)@.union_prefer_right(other@),
+    {
+        self.m.extend(other.m)
+    }
 }
 
 pub broadcast proof fn axiom_string_hash_map_spec_len<Value>(m: &StringHashMap<Value>)