The Coq mailing list

[jean-francois.monin AT imag.fr]

In the same vein, see also Appendix B in the PhD of Pierre Corbineau: 
he proves that given the inductive Type entry := 
mkE : forall X : set, X -> entry,
there is no coerce function of type forall X:Set, X -> option X 
such that (coerce X (mkE X x)) reduces to (Some x).

  JF

Benjamin Werner a ecrit :
 > 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
 > >
 > 
 > --------------------------------------------------------
 > 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
 > 
 >