@@ -47,9 +47,13 @@ deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
47deleteAt _ [] impossible
47deleteAt _ [] impossible
49replaceAt : Fin n -> t -> Vect n t -> Vect n t
49replaceAt : 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
51replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs
51replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs
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
53--------------------------------------------------------------------------------
57--------------------------------------------------------------------------------
54-- Subvectors
58-- Subvectors
55--------------------------------------------------------------------------------
59--------------------------------------------------------------------------------