Add post to List.withFilter

epfl-lara · Oct 3, 2019 · 5e73cf5 · 5e73cf5
1 parent 1ef5392
commit 5e73cf5
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/frontends/library/stainless/collection/List.scala b/frontends/library/stainless/collection/List.scala
@@ -481,7 +481,13 @@ sealed abstract class List[T] {
   }
 
   // In case we implement for-comprehensions
-  def withFilter(p: T => Boolean) = filter(p)
+  def withFilter(p: T => Boolean): List[T] = {
+    filter(p)
+  } ensuring { res =>
+    res.size <= this.size &&
+    res.content.subsetOf(this.content) &&
+    res.forall(p)
+  }
 
   @isabelle.function(term = "%xs P. List.list_all P xs")
   def forall(p: T => Boolean): Boolean = this match {