The Coq mailing list

[Robby Findler <robby AT eecs.northwestern.edu>]

Isn't that the first example in (essentially) every paper? Won't newcomers assume it is a good starting point to just play around? And won't that attitude just scare them off? Is that a good outcome? 

Robby

On Sun, Dec 17, 2017 at 9:41 AM Adam Chlipala <adamc AT csail.mit.edu> wrote:

In my opinion, it is a very handy feature to make out-of-the-box vectors
difficult to work with, since almost no one should be using dependently
typed vectors for anything.

On 12/17/2017 10:39 AM, Emilio Jesús Gallego Arias wrote:
> 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.