@@ -68,6 +68,12 @@ index fZ (x::xs) = x
6868index (fS k) (x::xs) = index k xs
6969index fZ [] impossible
7070
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
76+
7177||| Construct a new vector consisting of all but the indicated element
7278deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
7379deleteAt fZ (x::xs) = xs