module Basics where

open import Data.Nat public

open import Data.Vec public using (Vec; []; _∷_)
open import Data.Fin public using (Fin; zero; suc)

_!_ : ∀ {n A} → Vec A n → Fin n → A
[] ! ()
(x ∷ xs) ! zero = x
(x ∷ xs) ! suc i = xs ! i

open import Data.Function using (_∘_)

tabulate : ∀ {n A} → (Fin n → A) → Vec A n
tabulate {zero} f = []
tabulate {suc n} f = f zero ∷ tabulate (f ∘ suc)

open import Relation.Binary.PropositionalEquality

lem-tabulate-! : ∀ {n A} (f : Fin n → A) (i : Fin n) →
                 f i ≡ tabulate f ! i
lem-tabulate-! f zero    = refl
lem-tabulate-! f (suc i) = lem-tabulate-! (f ∘ suc) i

zipWith : ∀ {A B C n} → (A → B → C) →
          Vec A n → Vec B n → Vec C n
zipWith f []       []       = []
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys