module Control.Fold

import Data.Vect
import Data.Nat

dfoldl : {b : Nat -> Type} -> ((0 m : Nat) -> b m -> a -> b (S m)) -> b m -> Vect n a -> b (n + m)
dfoldl f z [] = z
dfoldl {n=S n} f z (x::xs) = rewrite plusSuccRightSucc n m in dfoldl f (f m z x) xs