# HG changeset patch # User wenzelm # Date 1274435419 -7200 # Node ID 4834c31127883e98e1a96ea38cf07afbebd12533 # Parent 9640f654617907e1bc85f6945dd6863a71461802 added Library.undefined (in Scala); diff -r 9640f6546179 -r 4834c3112788 src/Pure/library.scala --- a/src/Pure/library.scala Fri May 21 11:16:01 2010 +0200 +++ b/src/Pure/library.scala Fri May 21 11:50:19 2010 +0200 @@ -17,6 +17,14 @@ object Library { + /* partial functions */ + + def undefined[A, B] = new PartialFunction[A, B] { + def apply(x: A): B = throw new NoSuchElementException("undefined") + def isDefinedAt(x: A) = false + } + + /* separate */ def separate[A](s: A, list: List[A]): List[A] =