Remove bad trigger (#14)

Keeping this trigger causes profiling to fail, as the trigger cannot be found in the body of the quantifier.
viperproject · Mar 20, 2024 · 0a35a36 · 0a35a36
1 parent 0528eda
commit 0a35a36
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/dicts/dicts.gobra b/dicts/dicts.gobra
@@ -147,7 +147,7 @@ ghost
 opaque
 decreases
 pure func IsTotal(d dict[int]int) bool {
-	return forall k int :: {d[k]} {k in domain(d)} k in domain(d)
+	return forall k int :: {k in domain(d)} k in domain(d)
 }
 
 // True iff a dictionary is monotonic.