Added Data.Vec.updateAt and its properties.

[andreasabel]

Generalized Data.Vec._[_]:=_ (update) to updateAt which applies a function to the vector element pointed to by the index. I generalized all existing laws for update to updateAt.

Possible bikeshedding:

• name of updateAt

We should have a uniform name for updating a point in a collection (list, vector, finite map) by a function which modifies its value. The updateAt operation is more general than overwriting an element (which is a trivial special case of updateAt).

[MatthewDaggitt]

@andreasabel sorry it's taken me so long to look at this. It all looks good! My only comment is that I don't find the _≡_↾¹_ relations very intuitive to read. I think it would be much clearer if it was written out longhand. Would you mind if I changed it?

[andreasabel]

@MatthewDaggitt
Sorry, I myself also did not look at my PR (was busy teaching).

don't find the ≡_↾¹ relations very intuitive to read
Ah, too bad, I thought it was a natural step there from the function restriction notation ↾ of set theory.

I removed the notation in 0156aee, for comparison. If you find that easier to read, please go ahead an merge (unless you have other concerns). Otherwise you can revert that commit.

[MatthewDaggitt]

Thanks, merging in. Will fix the uncomment typo.

[andreasabel]

Thanks for merging!