@@ -65,7 +65,7 @@ using (k : Nat, ts : Vect k Type)
6565 put {p = Here} y (x::xs) = y :: xs
6666 put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
6767
68− ||| Replace an element with the correct type.
68+ ||| Update an element with the correct type.
6969 update : {default tactics { search 100; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
7070 update {p = Here} f (x::xs) = f x :: xs
7171 update {p = There p'} f (x::xs) = x :: update {p = p'} f xs