The Coq mailing list

[GANGCHEN5 AT aol.com]

Hello,

Is there an easy way to do pattern matching with product type ?

Assume:
Variable A,B,C : Set.
Definition ABC := A * B * C.
Variable a : A; b : B; c : C.
Definition i := (a,(b,c)).

I would like to write something like:
Check let (x,(y,z)) = i in (x,(y,z)).

Unfortunately this is an error:
Syntax error: [Prim.name] expected after ',' (in [ne_name_comma_list])

There is a way around:
Check let (x,r1) = i in let (y,z) = r1 in (x,(y,z)).

but not so elegant.

Gang  Chen