[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