update set

epfl-lara · Oct 14, 2024 · d0dc10d · d0dc10d
1 parent ff2043d
commit d0dc10d
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/frontends/library/stainless/lang/Set.scala b/frontends/library/stainless/lang/Set.scala
@@ -57,7 +57,7 @@ object Set {
     }
 
     @extern @pure
-    def flatMapPost[B](f: A => B)(b: B) = {
+    def flatMapPost[B](f: A => Set[B])(b: B) = {
       (??? : A)
     }.ensuring { _ =>
       flatMap(f).contains(b) == set.exists(a => f(a).contains(b))
@@ -126,4 +126,7 @@ sealed case class Set[T](theSet: scala.collection.immutable.Set[T]) {
 
   def contains(a: T): Boolean = theSet.contains(a)
   def subsetOf(b: Set[T]): Boolean = theSet.subsetOf(b.theSet)
+
+  def exists(p: T => Boolean): Boolean = theSet.exists(p)
+  def forall(p: T => Boolean): Boolean = theSet.forall(p)
 }