@@ -309,13 +309,12 @@ mapMaybe f (x::xs) =
310--------------------------------------------------------------------------------
310--------------------------------------------------------------------------------
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
317instance Foldable List where
312instance 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)
317+ foldl f q (x::xs) = foldl f (f q x) xs
320--------------------------------------------------------------------------------
319--------------------------------------------------------------------------------
321-- Special folds
320-- Special folds
@@ -809,6 +808,15 @@ hasAnyByNilFalse p (x::xs) =
809hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
808hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
810hasAnyNilFalse l = ?hasAnyNilFalseBody
809hasAnyNilFalse l = ?hasAnyNilFalseBody
811+foldlAsFoldr : (b -> a -> b) -> b -> List a -> b
812+foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z
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
813--------------------------------------------------------------------------------
821--------------------------------------------------------------------------------