added fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b;
authorwenzelm
Sun Jul 11 20:35:23 2004 +0200 (2004-07-11 ago)
changeset 150358c57751cd43f
parent 15034 e1282c4b39be
child 15036 cab1c1fc1851
added fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Sun Jul 11 20:34:50 2004 +0200
     1.2 +++ b/src/Pure/library.ML	Sun Jul 11 20:35:23 2004 +0200
     1.3 @@ -92,6 +92,7 @@
     1.4    val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
     1.5    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
     1.6    val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.7 +  val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.8    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
     1.9    val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.10    val length: 'a list -> int
    1.11 @@ -486,6 +487,7 @@
    1.12    in  itr l  end;
    1.13  
    1.14  fun fold f xs y = foldl (fn (y', x) => f x y') (y, xs);
    1.15 +fun fold_rev f xs y = foldr (fn (x, y') => f x y') (xs, y);
    1.16  
    1.17  fun foldl_map _ (x, []) = (x, [])
    1.18    | foldl_map f (x, y :: ys) =