The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I don't think Coq properly supports `x ~ .. ~ y ~ z`-like notations.  (Make a feature request?)  You can make `~` an infix notation, or you can make an "associate right" tactic or function and use that in a left-associated notation.  You might also be able to get `x ~ .. ~ y ~~ z` to work (use a distinct symbol for the last one).

-Jason

On Dec 21, 2014 2:02 PM, "Jonathan Leivent" <jonikelee AT gmail.com> wrote:

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