agda/examples/tactics/ac/Vec.agda

module Vec where

import Nat
import Fin

open Nat hiding (_==_; _<_)
open Fin

data Nil : Set where
  vnil : Nil

data Cons (A As : Set) : Set where
  vcons : A -> As -> Cons A As

data Vec (n : Nat)(A : Set) : Set

Vec' : Nat -> Set -> Set
Vec' zero    A = Nil
Vec' (suc n) A = Cons A (Vec n A)

data Vec n A where
  vec : Vec' n A -> Vec n A

ε : {A : Set} -> Vec zero A
ε = vec vnil

_∷_ : {A : Set}{n : Nat} -> A -> Vec n A -> Vec (suc n) A
x ∷ xs = vec (vcons x xs)

_!_ : {n : Nat}{A : Set} -> Vec n A -> Fin n -> A
_!_ {zero}   _                 (fin ())
_!_ {suc n} (vec (vcons x xs)) (fin fz)     = x
_!_ {suc n} (vec (vcons x xs)) (fin (fs i)) = xs ! i

map : {n : Nat}{A B : Set} -> (A -> B) -> Vec n A -> Vec n B
map {zero}  f (vec vnil)         = ε
map {suc n} f (vec (vcons x xs)) = f x ∷ map f xs

fzeroToN-1 : (n : Nat) -> Vec n (Fin n)
fzeroToN-1 zero    = ε
fzeroToN-1 (suc n) = fzero ∷ map fsuc (fzeroToN-1 n)