idris-0.9.10: test/reg011/reg011.idr

vfoldl : (P : Nat -> Type) ->
         ((x : Nat) -> P x -> a -> P (S x)) -> P Z
       -> Vect m a -> P m
-- vfoldl P cons nil []
--     = nil
vfoldl P cons nil (x :: xs)
    = vfoldl (\k => P (S k)) (\ n => cons (S n)) (cons Z nil x) xs
-- vfoldl P cons nil (x :: xs)
--     = vfoldl (\n => P (S n)) (\ n => cons _) (cons _ nil x) xs