add spec_has to Set, Multiset

source/rust_verify/example/syntax.rs

@@ -572,19 +572,15 @@ proof fn uses_arrow_matches_2(t: ThisOrThat)
     assert(t is That && t->v == 3);
 }
 
-#[verifier::external_body]
-struct Collection {}
-
-impl Collection {
-    pub spec fn spec_has(&self, v: nat) -> bool;
-}
-
-proof fn uses_spec_has(c: Collection)
+proof fn uses_spec_has(s: Set<int>, ms: vstd::multiset::Multiset<int>)
     requires
-        c has 3,
+        s has 3,
+        ms has 4,
 {
-    assert(c has 3);
-    assert(c has 3 == c has 3);
+    assert(s has 3);
+    assert(s has 3 == s has 3);
+    assert(ms has 4);
+    assert(ms has 4 == ms has 4);
 }
 
 } // verus!

source/vstd/multiset.rs

@@ -165,6 +165,12 @@ impl<V> Multiset<V> {
         self.count(v) > 0
     }
 
+    /// Predicate indicating if the set contains the given element: supports `self has a` syntax.
+    #[verifier::inline]
+    pub open spec fn spec_has(self, v: V) -> bool {
+        self.contains(v)
+    }
+
     /// Returns a multiset containing the lower count of a given element
     /// between the two sets. In other words, returns a multiset with only
     /// the elements that "overlap".

source/vstd/set.rs

@@ -50,6 +50,12 @@ impl<A> Set<A> {
     /// Predicate indicating if the set contains the given element.
     pub spec fn contains(self, a: A) -> bool;
 
+    /// Predicate indicating if the set contains the given element: supports `self has a` syntax.
+    #[verifier::inline]
+    pub open spec fn spec_has(self, a: A) -> bool {
+        self.contains(a)
+    }
+
     /// DEPRECATED: use =~= or =~~= instead.
     /// Returns `true` if for every value `a: A`, it is either in both input sets or neither.
     /// This is equivalent to the sets being actually equal