tdd-idris

Chap8.idr

import Vector

-- 8.3

total
headUnequal : DecEq a => {xs : Vector n a} -> {ys : Vector n a} ->
    (contra : (x = y) -> Void) -> ((x::xs) = (y::ys)) -> Void
headUnequal contra Refl = contra Refl

total
tailUnequal : DecEq a => {xs : Vector n a} -> {ys : Vector n a} ->
    (contra : (xs = ys) -> Void) -> ((x::xs) = (y::ys)) -> Void
tailUnequal contra Refl = contra Refl


DecEq a => DecEq (Vector n a) where
  decEq [] [] = Yes Refl
  decEq (x :: xs) (y :: ys) =
    case decEq x y of
         Yes Refl => case decEq xs ys of
                          Yes Refl => Yes Refl
                          No contra => No (tailUnequal contra)
         No contra => No (headUnequal contra)

Vector.idr

module Vector

public export
data Vector : Nat -> Type -> Type where
  Nil : Vector Z elem
  (::) : elem -> Vector len elem -> Vector (S len) elem

%name Vector xs, ys, zs