The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

Le 7 oct. 05 à 09:38, 
vincent.chatel AT transport.alstom.com
 a écrit :

> 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

Technically that is due to the fact that Coq has no "universe  
polymorphism".

But the main point is that when you have a list of objects who can be  
of any type,
like in these examples, you cannot do much with it. Basically, you  
can just apply the
elements of the list to a polymorphic function (I.e. which takes  
arguments of any
type). So these definitions are rarely used in practice, as far as I  
can think.


Cheers,


Benjamin


> 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.
>
> --------------------------------------------------------
> 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