From d7f8c8b0cdf60d6241990a083861a7dfb9bdf8cb Mon Sep 17 00:00:00 2001
From: Samuel Chassot <samuel.chassot@epfl.ch>
Date: Fri, 11 Oct 2024 16:09:14 +0200
Subject: [PATCH] add flatmap to set

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

diff --git a/frontends/library/stainless/lang/Set.scala b/frontends/library/stainless/lang/Set.scala
index a299eecf7..8da2ba422 100644
--- a/frontends/library/stainless/lang/Set.scala
+++ b/frontends/library/stainless/lang/Set.scala
@@ -36,6 +36,11 @@ object Set {
       new Set(set.theSet.map(f))
     }
 
+    @extern @pure
+    def flatMap[B](f: A => Set[B]): Set[B] = {
+      new Set(set.theSet.flatMap(f(_).theSet))
+    }
+
     @extern @pure
     def mapPost1[B](f: A => B)(a: A): Unit = {
       ()