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