The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-11-04 17:05 GMT+01:00 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?

​No, but maybe that using other symbols than "(,)", like "⦅,⦆​" or playing with notation levels and/or scopes.

Maybe something like

Notation "'( ' x ' )'" := …

​Which would force use of spaces in parentheses and might change something on the parser (but forcing to write "f( x )" rather than "f(x)").​ Not sure on how parenthesis are parsed for now though, so it might not work either.

 

Mike