The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

This is a nice improvement, as I just discovered with the following  
example:

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

Definition vhead (A:Set) (n:nat) (v:vec A (S n)) : A :=
  match v with
  | vnil => 0 (* never happen -- can return anything!!! *)
  | vcons _ b _ => b
  end.

My question is: how does this work? I tried to look in the manual but  
couldn't find any documentation for this behavior. It seems like you  
can put any return value in the vnil case and it infers a dependent  
return type; but it used to be you had to use some messy reasoning  
about absurdity of equalities or something to get the match expression  
to typecheck with all the cases...

This new feature is pleasantly surprising, but it would be even nicer  
now to be able to just not have to list that case in the matching at  
all, as in:

Definition vhead (A:Set) (n:nat) (v:vec A (S n)) : A :=
  match v with
  | vcons _ b _ => b
  end.

I know, you try to make people happy and they only ask for more...

Thanks, :-)
--- nadeem