The Coq mailing list

["Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>]

Hi,

In the second branch of the match statement below, I expected f to be of type 
Fin (S m) -> A. However, it’s reported to be of type Fin n -> A.

Inductive Fin : nat -> Set :=
  fzero : forall n : nat, Fin (S n) |
  fsuc : forall n : nat, Fin n -> Fin (S n).

Inductive Vec (A : Set) : nat -> Set :=
  vzero : Vec A 0 |
  vcons : forall n : nat, A -> Vec A n -> Vec A (S n).

Fixpoint tabulate (n : nat) (A : Set) (f : Fin n -> A) : Vec A n :=
  match n as n0 return (Vec A n0) with |
    0 => vzero A |
    S m => vcons A m (f (fzero m)) ...
  end.

From a purely syntactic point of view, I can see why this is the case. 
However, I’m not sure how to obtain a function of the required type to apply 
to (fzero m).

Regards,
Jeff.