From a4f735332669b9d4a86146ad275d38311d5358ab Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Thu, 30 Oct 2014 13:27:55 +0100
Subject: [PATCH] List.isEmpty in Leon lib
---
library/Option.scala | 1 +
library/collection/List.scala | 5 +++++
2 files changed, 6 insertions(+)
diff --git a/library/Option.scala b/library/Option.scala
index 8769f3386..ccf945eb1 100644
--- a/library/Option.scala
+++ b/library/Option.scala
@@ -32,6 +32,7 @@ sealed abstract class Option[T] {
def nonEmpty = !isEmpty
def isDefined = !isEmpty
+
}
case class Some[T](v: T) extends Option[T]
diff --git a/library/collection/List.scala b/library/collection/List.scala
index 26355f8e7..c9ebac9d3 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -285,6 +285,11 @@ sealed abstract class List[T] {
}
}
+ def isEmpty = this match {
+ case Nil() => true
+ case _ => false
+ }
+
}
@ignore
--
GitLab