From d0dc10d7430cad39f338efa04b5762fe21fbee59 Mon Sep 17 00:00:00 2001
From: Samuel Chassot <samuel.chassot@epfl.ch>
Date: Mon, 14 Oct 2024 15:32:28 +0200
Subject: [PATCH] update set

---
 frontends/library/stainless/lang/Set.scala | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/frontends/library/stainless/lang/Set.scala b/frontends/library/stainless/lang/Set.scala
index f9e491621..a7fbc75e4 100644
--- 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)
 }