rev_itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
STRUCTURE
SYNOPSIS
Applies a binary function between adjacent elements of the reverse of a list.
DESCRIPTION
rev_itlist f [x1,...,xn] b returns f xn ( ... (f x2 (f x1 b))...). It returns b if the second argument is an empty list.
FAILURE
Fails if some application of f fails.
EXAMPLE
- rev_itlist (curry op * ) [1,2,3,4] 1;
> val it = 24 : int

SEEALSO
HOL  Kananaskis-14