my exercises to learn agda

learning.agda

module vec where

open import Data.Product hiding (zip)

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data Vec (X : Set) : ℕ → Set where
  ⟨⟩  : Vec X zero
  _,_ : {n : ℕ} → X → Vec X n → Vec X (suc n)

-- -- zip : ∀ {n S T} → Vec S n → Vec T n → Vec (S × T) n
-- -- zip ⟨⟩ ⟨⟩ = ⟨⟩
-- -- zip (x , ss) (x₁ , ts) = (x , x₁) , zip ss ts

-- vec : ∀ {n X} → X → Vec X n
-- vec {zero} x = ⟨⟩
-- vec {suc n} x = x , vec x

-- vapp : ∀ {n S T} → Vec (S → T) n → Vec S n → Vec T n
-- vapp ⟨⟩ ⟨⟩ = ⟨⟩
-- vapp (x , fs) (x₁ , ss) = x x₁ , vapp fs ss

-- vmap : ∀ {n S T} → (S → T) →  Vec S n → Vec T n
-- vmap f ⟨⟩ = ⟨⟩
-- vmap f (x , ss) = f x , vmap f ss

-- zip : ∀ {n S T} → Vec S n → Vec T n → Vec (S × T) n
-- zip ⟨⟩ ⟨⟩ = ⟨⟩
-- zip (x , ss) (x₁ , ts) = (x , x₁) , zip ss ts

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc  : {n : ℕ} → Fin n → Fin (suc n)

proj : ∀ {n X} → Vec X n → Fin n → X
proj (x , xs) i = x

tabulate : ∀ {n X} → (Fin n → X) → Vec X n
tabulate {zero} f = ⟨⟩
tabulate {suc n} f = {!f Fin.zero, tabulate (f ∘ suc)!}