The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> Cedric Auger 
>>>>> <sedrikov AT gmail.com>
>>>>>  writes:

> Still if you prefer to do induction on n, I would rather recommand the
> following definition of vector:

> Definition vector (A:Type) : nat -> Type :=
> fix vec n := match n with O => Empty_set | S n => prod A (vec n) end.

> This way dependant types will be less annoying to deal with.
> The reason is that inductive types have two kind of arguments:
> - parameters (left of the :) which are not to be pattern matched
> - indices (right of the :) which are to be pattern matched

Thank you, Cedric, this is excellent information, and clarifying on a few
levels of difficulties I've been facing with these vectors.

Your definition above also makes the ssreflect "seqn" type make more sense, as
to why it was coded the way it is:

  Fixpoint seqn_type n := if n is n'.+1 then T -> seqn_type n' else seq T.

  Fixpoint seqn_rec f n : seqn_type n :=
    if n is n'.+1 return seqn_type n then
      fun x => seqn_rec (fun s => f (x :: s)) n'
    else f [::].
  Definition seqn := seqn_rec id.

Since my use of vectors is fairly limited so far, I'll see if switching to
this representation is simpler.

John