@@ -47,9 +47,13 @@ deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
4747deleteAt _ [] impossible
4848
4949replaceAt : Fin n -> t -> Vect n t -> Vect n t
50−replaceAt fZ y (x::xs) = y::xs
50+replaceAt fZ y (x::xs) = y :: xs
5151replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs
5252
53+updateAt : Fin n -> (t -> t) -> Vect n t -> Vect n t
54+updateAt fZ f (x::xs) = f x :: xs
55+updateAt (fS k) f (x::xs) = x :: updateAt k f xs
56+
5357--------------------------------------------------------------------------------
5458-- Subvectors
5559--------------------------------------------------------------------------------