From d8939b6d334d869e5888e792b2b55de22baa1758 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Fri, 11 Oct 2024 15:53:34 +0200 Subject: [PATCH] add flatMap to the set --- frontends/library/stainless/lang/Set.scala | 5 +++++ inox | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) 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 = { () diff --git a/inox b/inox index 516bf217f..6062f8f95 160000 --- a/inox +++ b/inox @@ -1 +1 @@ -Subproject commit 516bf217f053996f73a13ce1b400af4551437e12 +Subproject commit 6062f8f9552e5f71d441d7d0365bcb17e67fc224