The Coq mailing list

[Dimitri Hendriks <diem AT xs4all.nl>]

It helps to introduce x after the pattern matching on t, 
since its type X depends on the outcome, so:

Definition f (X : Set) (t : T X) : X -> Prop :=
  match t (* in T X return X -> Prop *) with 
    Build_T X0 => fun x => forall x0 : X0, x = x0 
  end.

Dimitri

On Aug 17, 2011, at 18:11 , Jeffrey Terrell wrote:

> In f, are X and X0 the same set?
> 
> Inductive T : Set -> Type :=
>   Build_T : forall X : Set, T X.
> 
> Definition f (X : Set) (t : T X) (x : X) :=
>   match t with Build_T X0 => forall x0 : X0, x = x0 end.
> 
> If they are, why does Coq reject the expression x = x0?
> 
> If they're not, how are they related?
> 
> Thanks. Jeff.
> 
>