The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On 12/17/2017 05:21 PM, Emilio Jesús Gallego Arias wrote:
>> What should then the proper alternative recommended alternative for
>> sized lists in the standard library?
> I meant:
> What should then the proper recommended alternative be?
> [In particular in the context of Coq's standard library]

I find the following definition of vectors a lot easier to work with than the 
one that is currently in the standard library:

Fixpoint vec (A: Type) (n: nat) : Type :=
  match n with
  | O => unit
  | S m => (A * vec A m)%type
  end.

With this definition and the "convoy pattern" from CPDT you're in control!

Rooby Findler asks:

> Isn't that the first example in (essentially) every paper? Won't
> newcomers assume it is a good starting point to just play around?

"call/cc" is the first example in many papers about control operators, yet it 
is not a good starting point for Scheme newcomers to just play around with 
the language...

If you just want to get things done in Coq, I agree with Adam that the "vec" 
type is best avoided, and if you really need to use it you should use the 
definition above and not the one from the standard library.  This points to a 
problem with the standard library that should be fixed like Emilio proposes.

If you want to study GADTs, of course the inductive definition of "vec A n" 
will be one of your first examples.  But let's not put that in the face of 
newcomers.

- Xavier Leroy