The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I'm attempting to create a right-associative recursive notation for a 
tuple-like type, and can't get it to work.  Can someone please tell me 
what I'm doing wrong?

Inductive prod' (A B:Type) : Type :=
  pair' : A -> B -> prod' A B.

Arguments pair' {A} {B} a b.

Notation "( x ~ .. ~ y ~ z )" :=
  (pair' x .. (pair' y z) .. ) (at level 0).

Definition tuptest := ( 1 ~ 2 ~ 3 ). (*produces a syntax error*)

I've tried several different operators, including %, &, \, #, and some 
Math characters as well, but nothing worked.

-- Jonathan