[isabelle-dev] "canonical" left-fold combinator for lists

Tjark Weber webertj at in.tum.de
Sat Jan 14 17:17:10 CET 2012


On Sat, 2012-01-14 at 14:34 +0100, Tobias Nipkow wrote:
> - If one of them is singled out as "fold", then it should be foldr,
> not foldl [...]

This is correct, of course; also because foldr can be generalized to
catamorphisms on arbitrary algebraic data types.  In other words, foldr
is the canonical fold. ;-)

However, for clarity I would suggest to go with foldl/foldr rather than
foldl/fold.

Kind regards,
Tjark





More information about the isabelle-dev mailing list