@@ -68,6 +68,12 @@ index fZ (x::xs) = x
68index (fS k) (x::xs) = index k xs
68index (fS k) (x::xs) = index k xs
69index fZ [] impossible
69index fZ [] impossible
71+||| Insert an element at a particular index
72+insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a
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
71||| Construct a new vector consisting of all but the indicated element
77||| Construct a new vector consisting of all but the indicated element
72deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
78deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
73deleteAt fZ (x::xs) = xs
79deleteAt fZ (x::xs) = xs