The Coq mailing list

[vincent.chatel AT transport.alstom.com]

Thanks, but in this case I cannot construct a poly_list of poly_list.

And when I assume that X : Type, I have a Universe Inconsistency

Regards

Vincent






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


--------------------------------------------------------
Bug reports: http://coq.inria.fr/bin/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club




:._______________
CONFIDENTIALITE : Ce message et les éventuelles pièces attachées sont
confidentiels. Si vous n'êtes pas dans la liste des destinataires, veuillez
informer l'expéditeur immédiatement et ne pas divulguer le contenu à une
tierce personne, ne pas l'utiliser pour quelque raison que ce soit, ne pas
stocker ou copier l'information qu'il contient sur un quelconque support.
CONFIDENTIALITY : This  e-mail  and  any attachments are confidential and
may be privileged. If  you are not a named recipient, please notify the
sender immediately and do not disclose the contents to another person, use
it for any purpose or store or copy the information in any medium.