@@ -309,13 +309,12 @@ mapMaybe f (x::xs) =
309309-- Folds
310310--------------------------------------------------------------------------------
311311
312−||| A tail recursive right fold on Lists.
313−total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> List t -> acc
314−foldrImpl f e go [] = go e
315−foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
316−
317312instance Foldable List where
318− foldr f e xs = foldrImpl f e id xs
313+ foldr c n [] = n
314+ foldr c n (x::xs) = c x (foldr c n xs)
315+
316+ foldl f q [] = q
317+ foldl f q (x::xs) = foldl f (f q x) xs
319318
320319--------------------------------------------------------------------------------
321320-- Special folds
@@ -809,6 +808,15 @@ hasAnyByNilFalse p (x::xs) =
809808hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
810809hasAnyNilFalse l = ?hasAnyNilFalseBody
811810
811+foldlAsFoldr : (b -> a -> b) -> b -> List a -> b
812+foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z
813+
814+||| The definition of foldl works the same as the default definition
815+||| in terms of foldr
816+foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q xs = foldlAsFoldr f q xs
817+foldlMatchesFoldr f q [] = Refl
818+foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs
819+
812820
813821--------------------------------------------------------------------------------
814822-- Proofs