The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

On Mon, 16 May 2011 09:57:01 +0800
Frederic Blanqui 
<frederic.blanqui AT inria.fr>
 wrote:

> You can also have a look at the vector library of CoLoR. See 
> http://color.inria.fr/ and, in particular, ;
> http://color.inria.fr/doc/CoLoR.Util.Vector.VecUtil.html . Best regards, ;
> Frederic.

Thanks, I'll give it a look. I'd read about CoLoR in one of the
various coq presentations available online. The main issue I have
with that sort of approach is that it's not clear how/why any of
the particular steps were taken when reading the definitions and
proofs. I have a feeling this is something you get an intuitive
sense of after years of grappling with it.