Data.Vec.Functional operations and properties

[calintat]

I added a bunch of new functions in Data.Vec.Functional and also made a Data.Vec.Functional.Properties module. This is mostly stuff that I needed in one of my projects, but I'm happy to add more stuff if people are interested (either in this PR or a future one).

I think Data.Vec and Data.Vec.Functional should ideally have the same functions, so people can swap one module for the other easily (like I needed to do in my project). However, some existing functions in Data.Vec.Functional have slightly different types compared to their analogues in Data.Vec. For example, the order of arguments of remove is different:

-- Data.Vec.Base:
remove : ∀ {n} → Vec A (suc n) → Fin (suc n) → Vec A n

-- Data.Vec.Functional:
remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n

and foldr/foldl in Data.Vec take a dependent function, whereas foldr/foldl in Data.Vec.Functional take a non-dependent function. I think these functions in Data.Vec.Functional should be changed to match the ones in Data.Vec, but such changes would break backwards-compatibility. What do you think?

[JacquesCarette]

Wonderful additions. I only saw a few things that should be revisited.

[gallais]

Standardisation of folds is a long standing issue (#278).
I agree that all of the discrepancies between the order of arguments should
be solved. Could you document the one you found by opening an issue?