The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Hi all,

I don't mean to start any kind of controversial discussion but I can't
stop wondering about:

a) whether "Vector" and "Fin" are really usable libraries

b) if it is OK that Coq proposes it as the standard solution for sized
   lists and bounded integers to newcomers

IMHO, having to learn ultra-advanced pattern matching patterns in order
to manipulate vectors and ordinals seems a bit of a too step learning
curve, specially for such pervasive structures.

An even so, learning all that may not be enough, for example, try to
prove the following lemma:

 `∀ x, Vector.rev (Vector.rev x) = x`.

Unless I am missing something, it seems like a fun proof to.

I wonder, what do others think?

Best,
E.