Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Re: [Coq-Club] R�f. : Re: [Coq-Club] prod list

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: [Coq-Club] R�f. : Re: [Coq-Club] prod list


chronological Thread 
  • From: Benjamin Werner <benjamin.werner AT inria.fr>
  • To: vincent.chatel AT transport.alstom.com
  • Cc: Venanzio Capretta <venanzio AT site.uottawa.ca>, coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] Re: [Coq-Club] Réf. : Re: [Coq-Club] prod list
  • Date: Fri, 7 Oct 2005 16:11:54 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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






Archive powered by MhonArc 2.6.16.

Top of Page