Zippy2

sandbox.idr

module Sandbox

import Data.Vect

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

-- 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