Zippy.idr

sandbox.idr

module Sandbox

import Data.Vect

||| zip to Vectors of the same size
||| using a proof that n=m
||| instead of zippy: Vect n e -> Vect n a -> Vect n (e,a)
zippy :  Vect n e -> Vect m a -> (n = m)-> Vect m (e,a)
zippy [] [] Refl = []
zippy  (x :: xs) (y :: ys) Refl =  (x, y) :: zippy xs ys Refl

-- sample

e : Vect 3 String
e = ["Hello", "World", "Idris"]

a : Vect 3 Integer
a = [0,1,2]

result : Vect 3 (String, Integer)
result = zippy e a Refl