function butlast added
authorwebertj
Sat Jul 15 18:17:47 2006 +0200 (2006-07-15)
changeset 201339ee091573fa0
parent 20132 de3c295000b2
child 20134 73cb53843190
function butlast added
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Sat Jul 15 15:26:50 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Sat Jul 15 18:17:47 2006 +0200
     1.3 @@ -103,6 +103,7 @@
     1.4    val cons: 'a -> 'a list -> 'a list
     1.5    val single: 'a -> 'a list
     1.6    val singleton: ('a list -> 'b list) -> 'a -> 'b
     1.7 +  val butlast: 'a list -> 'a list
     1.8    val append: 'a list -> 'a list -> 'a list
     1.9    val apply: ('a -> 'a) list -> 'a -> 'a
    1.10    val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.11 @@ -496,6 +497,10 @@
    1.12  
    1.13  fun singleton f x = (case f [x] of [y] => y | _ => raise Empty);
    1.14  
    1.15 +fun butlast []        = raise Empty
    1.16 +  | butlast (x :: []) = []
    1.17 +  | butlast (x :: xs) = x :: butlast xs;
    1.18 +
    1.19  fun append xs ys = xs @ ys;
    1.20  
    1.21  fun apply [] x = x