The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

Hi,

Given the usual definition for lists indexed by length:

Inductive vect [A:Set] : nat -> Set :=
| nil : (vect A O)
| cons : (x:A)(n:nat)(vect A n)->(vect A (S n)).

Can anyone explain what the difference is between using terms of this type 
and 
terms of type {x:list A | length = n}, particularly in the domain of writing 
certified programs (e.g. in the specification of a head/tail/take/append 
function)? When and why would you pick one representation over the other? 

Thanks.