The Coq mailing list

[Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>]

> I would like to construct an inductive type like prod but such that all
> elements of this type finish by a final element.
>
> ( ) : 1
> (a,( )) : A * 1 (it's isomorph to A)
> (b,a,( )) : B *A *1
> ...
>
> It seems like a list but in a list I cannot mix elements with 
> differents
> types.

Here is an implementation that allows you to have the elements' types 
in the type of the tuple.

Set Implicit Arguments.

Inductive list (A:Type) : Type :=
| cons : A -> list A -> list A
| nil : list  A.

Inductive tuple : list Type -> Type :=
| t_cons T TS : T -> tuple TS -> tuple (cons T TS)
| t_nil : tuple (nil _).

Notation "[ x ; .. ; y ]" := (cons x .. (cons y (nil _)) ..).

Notation "( x , .. , y )" := (t_cons x .. (t_cons y t_nil) ..).

Check (1, bool , tt).

(1, bool, tt)
     : tuple [nat; Set; unit]

Roland