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$
7
  • 2
    $\begingroup$ This seems to be a question for Coq support mailing lists, not a question about computer science. $\endgroup$
    – Raphael
    Commented May 7, 2014 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$ Commented May 8, 2014 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
    Commented May 8, 2014 at 17:04
  • $\begingroup$ What do you mean by “small in the memory sense”? $\endgroup$ Commented May 8, 2014 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$ Commented Aug 24, 2014 at 12:32

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.