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)?