@mcc the foldl vs foldr thing is mostly about strict vs lazy. Foldl is better strict and foldr is better lazy. That's why foldl is better in OCaml and foldr is better in Haskell (except Haskell also has foldl' which is a strict foldl). As Idris is strict by default I believe foldl would be preferable