In Lean vectors are implemented using
def Vec (a : Type u) (n : Nat) :=
{ l : List a // l.length = n}
I think there is another way to do this without lists:
def Vec (α : Type u) (n : Nat) :=
match n with
| 0 => unit
| 1 => α
| Nat.succ k => α × (Vec α k)
Why were vectors implemented in the first way instead of the second way I wrote?
Implementing vectors as a subtype on lists allows the developers to reuse the large body of existing definitions and lemmas pertaining to lists when developing and working with vectors. This kind of reuse ends up being very important for building a coherent and somewhat manageable ecosystem, especially when proofs are thrown into the mix.
Additionally, Lean 4 compiles lists to native arrays, so the subtype implementation is preferable from a performance perspective. The subtype implementation was used in Lean 3 as well, so I don't think performance was a motivating factor in this particular case, but it's something to think about.
Scott Morrison correctly points out Lists don't compile to native arrays.
unitnotalpha, and then you don't need your definition for n=1. There are tons of ways to implement vectors though. What the best implementation is will depend on what you want to use them for. Perhaps one answer is: lists have got a huge API already, so why not just define vectors using them? $\endgroup$