fix: Drop SelectOpt from MutableMap

dafny-lang · Nov 13, 2024 · 7af1ae1 · 7af1ae1
1 parent fabf44d
commit 7af1ae1
Showing 1 changed file with 0 additions and 11 deletions.
diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy
@@ -97,17 +97,6 @@ module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} DafnyLibraries
       ensures v in this.content().Values
       ensures this.content()[k] == v
 
-    function SelectOpt(k: K): (o: Option<V>)
-      reads this
-      ensures o.Some? ==> (this.HasKey(k) && o.value in this.content().Values && this.content()[k] == o.value)
-      ensures o.None? ==> !this.HasKey(k)
-    {
-      if this.HasKey(k) then
-        Some(this.Select(k))
-      else
-        None
-    }
-
     method {:extern} Remove(k: K)
       modifies this
       ensures this.content() == old(this.content()) - {k}