The Coq mailing list

[vincent.chatel AT transport.alstom.com]

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

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