The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

On 9 Jun 2008, at 15:25, Conor McBride wrote:

> 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.

I should add that things do seem to be getting
better, especially with what Matthieu Sozeau
has been doing. I hope it will cease to be a
fact at all.

Epigram and Agda users seem to have a marginal
preference for the inductive version of vectors,
mostly because (a) it plays better with
implicit syntax and (b) the length information
just gets handled implicitly most of the time.

The recursive construction is a nice workaround,
profiting from the fact that vectors can somehow
take their inductive structure from their
lengths.

Cheers

Conor