From 55e0adfd8925e6217a730015bb3c407d5a553d23 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 12 May 2016 12:40:32 +0200
Subject: [PATCH] Strengthen List.apply spec
---
library/leon/collection/List.scala | 2 ++
1 file changed, 2 insertions(+)
diff --git a/library/leon/collection/List.scala b/library/leon/collection/List.scala
index a7bf09527..a4db194c3 100644
--- a/library/leon/collection/List.scala
+++ b/library/leon/collection/List.scala
@@ -62,6 +62,8 @@ sealed abstract class List[T] {
} else {
tail(index-1)
}
+ } ensuring {
+ content.contains(_)
}
@isabelle.function(term = "%xs x. x # xs")
--
GitLab