end_itlist : ('a -> 'a -> 'a) -> 'a list -> 'a)
STRUCTURE
Lib
SYNOPSIS
List iteration function. Applies a binary function between adjacent elements of a list.
DESCRIPTION
end_itlist f [x1,...,xn] returns f x1 ( ... (f x(n-1) xn)...). Returns x for a one-element list [x].
FAILURE
Fails if list is empty, or if an application of f raises an exception.
EXAMPLE
- end_itlist (curry op+) [1,2,3,4];
> val it = 10 : int

SEEALSO
itlist, rev_itlist, itlist2, rev_itlist2
HOL  Kananaskis-10