Modernise Data.Vec(.Properties)

[MatthewDaggitt]

While working on #1668 with @jamesmckinna I noticed that some of the code in Data.Vec(.Properties) is pretty ancient by the library standards. I've tried to modernise the code by:

• introducing variables for sizes/elements/vectors as now allowed by the style guide
• importing Relation.Binary.PropositionalEquality unqualified
• using new combinators in propositional reasoning
• reorganising the file slightly to match the layout of Base

Should be a very nearly a no-op, modulo the movement of a couple of implicit arguments due to variables, a breakage which is acceptable in v2.0 I think.

[jamesmckinna]

What is the corresponding situation ('modernised', or otherwise) for Data.List?
Is it ('simply'?) the case that this latter (set of) module(s) get(s) much more attention than that/those for Data.Vec?

[gallais]

It's kind of strange to be insisting on f being commutative as opposed to
the more general constraint ∀ x y → f x y ≡ g y x.

[MatthewDaggitt]

Generalised. At the time I was trying to lift algebraic structures over vectors, so I wasn't thinking in more general terms.

[gallais]

Makes sense. I guess now that we're not insisting on commutativity, we can also relax the type and have:

f : A → B → C
g : B → A → C

[MatthewDaggitt]

Generalised further!

[MatthewDaggitt]

What is the corresponding situation ('modernised', or otherwise) for Data.List?
Is it ('simply'?) the case that this latter (set of) module(s) get(s) much more attention than that/those for Data.Vec?

Better, as they do get more attention. You could definitely go through Data.List.Properties and add variables for x y xs ys though.