The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi Adam

On 9 Jun 2008, at 15:12, Adam Chlipala wrote:

> Edsko de Vries wrote:
> > I'm stuck again in trying to write some dependent code. I want to  
> > index a
> > vector:
>
> I'm sure someone else will answer your literal question, but I want  
> to offer some advice that would lead to different (easier to  
> discharge) goals.  I've found that vectors are _much_ easier to  
> work with if you define them by recursion rather than with  
> inductive types.

Let's be clear: this is a fact about Coq, not
about vectors.

All the best

Conor