src/Pure/library.ML
changeset 4713 bea2ab2e360b
parent 4692 748f4e365d14
child 4792 8e3c2dddb9c8
     1.1 --- a/src/Pure/library.ML	Tue Mar 10 13:23:35 1998 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Mar 10 13:24:11 1998 +0100
     1.3 @@ -76,6 +76,7 @@
     1.4    val length: 'a list -> int
     1.5    val take: int * 'a list -> 'a list
     1.6    val drop: int * 'a list -> 'a list
     1.7 +  val dropwhile: ('a -> bool) -> 'a list -> 'a list
     1.8    val nth_elem: int * 'a list -> 'a
     1.9    val last_elem: 'a list -> 'a
    1.10    val split_last: 'a list -> 'a list * 'a
    1.11 @@ -424,6 +425,9 @@
    1.12    | drop (n, x :: xs) =
    1.13        if n > 0 then drop (n - 1, xs) else x :: xs;
    1.14  
    1.15 +fun dropwhile P [] = []
    1.16 +  | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
    1.17 +
    1.18  (*return nth element of a list, where 0 designates the first element;
    1.19    raise EXCEPTION if list too short*)
    1.20  fun nth_elem NL =