0
$\begingroup$

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

$\endgroup$
  • 2
    $\begingroup$ This seems to be a question for Coq support mailing lists, not a question about computer science. $\endgroup$ – Raphael May 7 '14 at 22:50
  • 2
    $\begingroup$ @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. $\endgroup$ – Gilles 'SO- stop being evil' May 8 '14 at 16:45
  • $\begingroup$ @Gilles It was the last line that pushed me to off-topic; I'm sure there is a language-design issue somewhere in there. $\endgroup$ – Raphael May 8 '14 at 17:04
  • $\begingroup$ What do you mean by “small in the memory sense”? $\endgroup$ – Gilles 'SO- stop being evil' May 8 '14 at 23:34
  • 1
    $\begingroup$ 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. $\endgroup$ – Rui Baptista Aug 24 '14 at 12:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.