fix: missing type characteristic for a functions that accesses the Va…

…lues of a map
dafny-lang · Sep 19, 2023 · 73a8b37 · 73a8b37
1 parent 05beef6
commit 73a8b37
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy
@@ -95,7 +95,7 @@ module {:options "-functionSyntax:4"} Maps {
 
   /* Swaps map keys and values. Values are not required to be unique; no
   promises on which key is chosen on the intersection. */
-  ghost function {:opaque} Invert<X, Y>(m: map<X, Y>): map<Y, X>
+  ghost function {:opaque} Invert<X, Y(==)>(m: map<X, Y>): map<Y, X>
   {
     map y | y in m.Values :: var x :| x in m.Keys && m[x] == y; x
   }