From 7a46bba4c08b589a9b828c84dce86fe775231f4b Mon Sep 17 00:00:00 2001 From: Stevan Date: Thu, 13 Aug 2020 11:23:23 +0200 Subject: [PATCH] Fix some more foralls. --- frontends/library/stainless/collection/List.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/library/stainless/collection/List.scala b/frontends/library/stainless/collection/List.scala index 1c9e7cd004..e3bd259c15 100644 --- a/frontends/library/stainless/collection/List.scala +++ b/frontends/library/stainless/collection/List.scala @@ -1300,7 +1300,7 @@ object ListSpecs { val intersection = first & second intersection.forall(first.contains) && intersection.forall(second.contains) && - forall((elem: T) => intersection.contains(elem) == (first.contains(elem) && second.contains(elem))) + intersection.forall(value => first.contains(value) && second.contains(value)) } @opaque