The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

The subject of dependent data structures in Coq is subtle enough that I 
recommend reading an organized overview, like Chapter 9 of CPDT:
    http://adam.chlipala.net/cpdt/

On 11/09/2014 12:49 PM, John Wiegley wrote:
> Thank you, Cedric, this is excellent information, and clarifying on a 
> few levels of difficulties I've been facing with these vectors. [...] 
> Since my use of vectors is fairly limited so far, I'll see if 
> switching to this representation is simpler. John