add postcondition to forall and exist on Set (#1596)

Co-authored-by: Viktor Kunčak <[email protected]>
epfl-lara · Oct 27, 2024 · e2d66f5 · e2d66f5
1 parent a4cb53f
commit e2d66f5
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/frontends/library/stainless/lang/Set.scala b/frontends/library/stainless/lang/Set.scala
@@ -33,12 +33,12 @@ object Set {
     @library @extern @pure
     def exists(p: A => Boolean): Boolean = {
       set.theSet.exists(p)
-    }
+    }.ensuring(res => res == set.toList.exists(p))
 
     @library @extern @pure
     def forall(p: A => Boolean): Boolean = {
       set.theSet.forall(p)
-    }
+    }.ensuring(res => res == set.toList.forall(p))
 
     @library @extern @pure
     def map[B](f: A => B): Set[B] = {