Re: [isabelle] argument order of List.foldr



This one is used in my ML book. It (and the corresponding foldl) work for lists of lists nested to any depth. E.g.

fun sum_of_sums xss = foldl (foldl op+) (0, xss);

Larry

On 6 Mar 2010, at 18:09, Brian Huffman wrote:

> Maybe it is based on Isabelle's Library.foldr, which has this type:
> Library.foldr : ('a * 'b -> 'b) -> 'a list * 'b -> 'b
> 
> Since it has an uncurried type, the argument order doesn't make any
> difference here as far as partial application is concerned, and I
> recognize that there is a mnemonic benefit to this argument order:
> Library.foldr (op +) ([1,2,3], 4) = 1 + (2 + (3 + 4))






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.