coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: Problems with Fixpoint termination and Universe inconsistency.

From: Adam Koprowski <adam.koprowski AT gmail.com>
To: Adam Chlipala <adam AT chlipala.net>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Re: Problems with Fixpoint termination and Universe inconsistency.
Date: Thu, 18 Feb 2010 22:26:34 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=fZXawnoq3ao144tB2vc8ryelJtLdjRW8xcajAyeuZlonr4U7DITKA+rIZg2xhyUgnF aPSDfFGOPqPpom4AMAbUIfAtJ6TJlvIFTTPZmZYCOX+Bx3q002JAgzN+4f+yd/lRucyR Kjwby7EHwJjhfkt4cRqqCyribfjCnnJmW0EJ8=

First, a simple type annotation gets Coq to accept your definition of [hlist_combine], with no need for [Program]. �[...]
Finally, here's a (probable) definition of your final [hlist_prod_tuple]. �[...]

��Thank you very much! That's been�immensely�helpful!

�� Adam

--
Adam Koprowski � [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate � �[http://mlstate.com, 15 rue Berlier, 75013 Paris, France]

[Coq-Club] Problems with Fixpoint termination and Universe inconsistency., Adam Koprowski
- [Coq-Club] Re: Problems with Fixpoint termination and Universe inconsistency., Adam Koprowski
  - Re: [Coq-Club] Re: Problems with Fixpoint termination and Universe inconsistency., Adam Chlipala
    - Re: [Coq-Club] Re: Problems with Fixpoint termination and Universe inconsistency., Adam Koprowski
- Re: [Coq-Club] Problems with Fixpoint termination and Universe inconsistency., Bruno Barras