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