changeset 37042 | 4834c3112788 |
parent 37029 | 39f4cce5a22c |
child 37055 | d014976dd690 |
1.1 --- a/src/Pure/library.scala Fri May 21 11:16:01 2010 +0200 1.2 +++ b/src/Pure/library.scala Fri May 21 11:50:19 2010 +0200 1.3 @@ -17,6 +17,14 @@ 1.4 1.5 object Library 1.6 { 1.7 + /* partial functions */ 1.8 + 1.9 + def undefined[A, B] = new PartialFunction[A, B] { 1.10 + def apply(x: A): B = throw new NoSuchElementException("undefined") 1.11 + def isDefinedAt(x: A) = false 1.12 + } 1.13 + 1.14 + 1.15 /* separate */ 1.16 1.17 def separate[A](s: A, list: List[A]): List[A] =