# Coq: default values for vectors

Let's say there is a vector of length $n$:

Require Import Vector.
Variable T:Type.
Variable n:nat.
Variable v:t T n.


"list" gives a function "nth" that demands a default result that is returned when the list is longer than the index requested. This is convenient, and the definition is readable.

Now vector uses a definition of nth (using Fin) that assures on type level that the requested Index is smaller than the length of the vector. Confusingly, it also uses a constructor "t", just like Vector. How can I define a function that behaves the same as nth for lists? The definition of nth for vector plainly appears as unreadable to me. Should I use "to_list"?

Was this built this way to keep the type small (in the memory sense)?

• This seems to be a question for Coq support mailing lists, not a question about computer science. – Raphael May 7 '14 at 22:50
• @Raphael This question is borderline between language design (on-topic) and programming (off-topic, though we don't have a firm rule about writing constructive proofs, which isn't run-of-the-mill programming). I'm reopening it for now (to give people a chance at answering — I might do it myself); if we decide to close it here, we'll migrate to Stack Overflow. I've raised the issue on meta. – Gilles 'SO- stop being evil' May 8 '14 at 16:45
• @Gilles It was the last line that pushed me to off-topic; I'm sure there is a language-design issue somewhere in there. – Raphael May 8 '14 at 17:04
• What do you mean by “small in the memory sense”? – Gilles 'SO- stop being evil' May 8 '14 at 23:34
• This question already includes an answer. Of course you can use to_list. But, then, what's the point of using vectors? Vectors are used when we don't want to consider exception cases. – Rui Baptista Aug 24 '14 at 12:32