add flatMap to the set

epfl-lara · Oct 11, 2024 · d8939b6 · d8939b6
1 parent fbdd54b
commit d8939b6
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git 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 = {
       ()

diff --git a/inox b/inox