Well, the n must "come from" the actual data. You could not construct a vector of any other size n. It'll just be typed so as to be realized at runtime and then

Well, the n must "come from" the actual data. You could not construct a vector of any other size n. It'll just be typed so as to be realized at runtime and then maintained. The functions by-and-large do not ensure that the vector is sized for a particular n, but instead that they respect whatever n ends up being true.