@@ -70,9 +70,9 @@ index fZ [] impossible
71||| Insert an element at a particular index
71||| Insert an element at a particular index
72insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a
72insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a
73−insertAt fZ y [] = [y]
73+insertAt fZ y xs = y :: xs
74−insertAt (fS k) y (x::xs) = x :: insertAt k y xs
74+insertAt (fS k) y (x::xs) = x :: insertAt k y xs
75−insertAt k y xs = y :: xs
75+insertAt (fS k) y [] = absurd k
77||| Construct a new vector consisting of all but the indicated element
77||| Construct a new vector consisting of all but the indicated element
78deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
78deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a