Define recursive notation with two recursive variables in Coq

Question

I'd like to define a notation that looks like the following for type contexts:

{ x1 : T1, x2 : T2, x3 : T3 }

However, I can't figure out a way to define such a notation recursively. My guess would be the following:

Notation "{ x1 : T1 , .. , xn : Tn }" := (cons (x1, T1) .. (cons (xn, Tn)) ..).

I get the following error: "Cannot find where the recursive pattern starts."

Is such a recursive notation possible, and if so, how can it be done?

Answer 1

Coq doesn't seem to recognize x1 : T1 and xn : Tn as expressions, and instead parses the notation as { x1 : (T1 , .. , xn) : Tn }. This suggests to define the notation in the following two steps.

Section T. (* To see the effect of the notation after closing this section. *)

(* recursive list notation *)
Notation "{ x1 , .. , xn }" :=
  (cons x1 .. (cons xn nil) ..).

(* pair notation *)
Notation "x : T" := ((x, T))
(at level 100).

Definition z := { 3 : 4, 5 : 6, 7 : 8 }.

Print z.
(* z = {3 : 4, 5 : 6, 7 : 8} *)

End T.

Print z.
(* z = ((3, 4) :: (5, 6) :: (7, 8) :: nil)%list *)