gistfile1.txt

Inductive vector (A:Set) :  nat -> Type :=
| vnil : vector A 0
| vcons : forall n, A -> vector A n -> vector A (S n).

Implicit Arguments vector [A].
Implicit Arguments vcons [A n].
Implicit Arguments vnil [A].

Fixpoint vecfold (A:Set) B n (f : A -> B -> B) (c:B) (l:vector n) :=
  match l with
    | vnil => c
    | vcons n0 x xs => f x (vecfold A B n0 f c xs)
  end.

Implicit Arguments vecfold [A B n].
Set Implicit Arguments.
Print vecfold.
Eval compute in (vecfold (fun x y => x  + y) 0 (vcons 1 (vcons 2 vnil))).