The Coq mailing list

[Venanzio Capretta <venanzio AT site.uottawa.ca>]

You can do this:

-----------------------------------------------------
Inductive poly_list: Type :=
  poly_nil: poly_list
| poly_cons: forall X:Set, X -> poly_list -> poly_list.

Implicit Arguments poly_cons [X].

Check (poly_cons true (poly_cons 3 poly_nil)).
------------------------------------------------------

In the good old days when Set was impredicative you could have defined
it in Set instead of Types.

Cheers,
  Venanzio



On Thu, 2005-06-10 at 17:11 +0200, 
vincent.chatel AT transport.alstom.com
wrote:
> Hi Coq'ers,
> 
> 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.
> 
> Thaks in advance
> 
> Vincent