The Coq mailing list

[Michael Shulman <shulman AT sandiego.edu>]

On Wed, Nov 4, 2015 at 6:26 AM, Cedric Auger 
<sedrikov AT gmail.com>
 wrote:
> Inductive single (T : Type) := Single : T -> single T.
> Inductive pair (T U : Type) := Pair : T -> U -> pair T U.
> Inductive triple (T U V : Type) := Triple : T -> U -> V -> triple T U V.
>
> And so on (or even define it recursively as a "tuple : forall n, n_types n
> -> Type").
>
> And then have a (x) notation for single T type, (x, y) for pair T U type and
> so on.

I tried this, but I couldn't get it to work.

Inductive single (T : Type) := Single : T -> single T.
Notation "( x )" := (Single x).
Definition test T (f : single T -> T) (x : T) : f(x) = f(x).

(* The term "x" has type "T" while it is expected to have type "single T". *)

Did you have something different in mind?

Mike