Fold.agda

module Fold where

open import Data.Nat.Base using (ℕ; suc)

data List {l} (A : Set l) : Set l where
  [] : List A
  _::_ : (x : A) → List A → List A
infixr 6 _::_


length : ∀ {l} {A : Set l} → List A → ℕ
length [] = 0
length (x :: xs) = suc (length xs)

fold : {A : Set} (P : List A → Set) → (∀ {a l} → A → P l → P (a :: l)) → P [] → (l : List A) → P l
fold p f init []  = init
fold p f init (x :: xs) = f x (fold p f init xs)