Add padRight and truncate to Data.Vec, and prove some properties

[TOTBWF]

Patch Description

This PR adds the following functions to Data.Vec.Base

truncate : ∀ {m n} → m ≤ n → Vec A n → Vec A m
pad : ∀ {m n} → m ≤ n → A → Vec A m → Vec A n

It also proves some properties of these two functions.

[gallais]

In Bounded we have:

padRight : ∀ {n} → A → Vec≤ A n → Vec A n
padLeft : ∀ {n} → A → Vec≤ A n → Vec A n
padBoth : ∀ {n} → A → A → Vec≤ A n → Vec A n

so we should probably stick to that naming convention.

[TOTBWF]

Yeah, that seems reasonable! Should we mark this as a breaking change then? If you import Data.Vec.Bounded and Data.Vec, you could get conflicts.

[MatthewDaggitt]

Thanks for the great PR! A few minor cosmetic comments.

[MatthewDaggitt]

Should we mark this as a breaking change then? If you import Data.Vec.Bounded and Data.Vec, you could get conflicts.

It's a good thought, but we add dozens of duplicated function names throughout the library every release so we tend not to. Also recent versions of Agda tends to give reasonable error messages for clashes so it's not too hard to debug the problem.

[MatthewDaggitt]

@TOTBWF any chance you have the time to make the minor changes from the reviews and then I'll merge this in?

[TOTBWF]

Sorry, I've been quite busy recently and this fell off my radar!

[MatthewDaggitt]

Thanks @gallais!