Example for Dependent Types in Agda

vectors.agda

data Vec (A : Set) : Nat -> Set where
  [] : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (succ n)




head : {A : Set} {n : Nat} -> Vec A (succ n) -> A
head (x :: _) = x




zip : {A B : Set} {n : Nat} -> Vec A n -> Vec B n -> Vec (A X B) n
zip [] [] = []
zip (x :: xs) (y :: ys) = < x , y > :: zip xs ys