diff --git a/doc/library.rst b/doc/library.rst index 8708e5a743fc36d4e7e52cd196c2e52bc0d09b8e..a165c0a6b0976f90e35802181f7fe433c7abef32 100644 --- a/doc/library.rst +++ b/doc/library.rst @@ -143,7 +143,7 @@ Leon Lists support a rich and strongly specified API. +---------------------------------------------------+---------------------------------------------------+ | ``lastOption: Option[T]`` | Optionally return the last element of this List. | +---------------------------------------------------+---------------------------------------------------+ -| ``firstOption: Option[T]`` | Optionally return the first element of this List. | +| ``headOption: Option[T]`` | Optionally return the first element of this List. | +---------------------------------------------------+---------------------------------------------------+ | ``unique: List[T]`` | Return this List without duplicates. | +---------------------------------------------------+---------------------------------------------------+ diff --git a/library/collection/List.scala b/library/collection/List.scala index d9031e8b7dc494e691a405cd9c32aa9e2439fbef..404c53c44596938abd9b4f7576b923f6778e86ff 100644 --- a/library/collection/List.scala +++ b/library/collection/List.scala @@ -35,17 +35,6 @@ sealed abstract class List[T] { (that != Nil[T]() || res == this) } - def headOption: Option[T] = this match { - case Nil() => None[T]() - case Cons(h, _) => Some(h) - } - - val tailOption: Option[List[T]] = this match { - case Nil() => None[List[T]]() - case Cons(_, t) => Some(t) - } - - def head: T = { require(this != Nil[T]()) val Cons(h, _) = this @@ -268,7 +257,7 @@ sealed abstract class List[T] { None[T]() }} ensuring { _.isDefined != this.isEmpty } - def firstOption: Option[T] = { this match { + def headOption: Option[T] = { this match { case Cons(h, t) => Some(h) case Nil() => @@ -550,6 +539,7 @@ case class Nil[T]() extends List[T] // 'Cons' Extractor object :: { + @library def unapply[A](l: List[A]): Option[(A, List[A])] = l match { case Nil() => None() case Cons(x, xs) => Some((x, xs))