coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Defining the function using refine

From: Takashi MIYAMOTO <tmiya AT bu.iij4u.or.jp>
To: Coq-Club <coq-club AT inria.fr>
Cc: Takashi MIYAMOTO <tmiya AT bu.iij4u.or.jp>
Subject: Re: [Coq-Club] Defining the function using refine
Date: Sun, 8 Jan 2012 08:58:49 +0900

Dear Cedric and Hugo,

Thank you for your detailed advice, Cedric.
I learned much in your mail.

Thank you for information of Coq 8.4, Hugo.
The new function would make easier to write programs like mine.

Regards,

===================================
Takashi Miyamoto
http://www.imasy.or.jp/~miyamoto/
http://tmiya.blogspot.com/

Re: [Coq-Club] Solving equalities over R, Rcompute fails, (continued)
- [Coq-Club] Defining the function using refine, Takashi MIYAMOTO
- Message not available
  - Re: [Coq-Club] Defining the function using refine, Pierre Boutillier
    - Re: [Coq-Club] Defining the function using refine, Takashi MIYAMOTO
    - Message not available
      - Re: [Coq-Club] Defining the function using refine, Pierre Boutillier
        
        Re: [Coq-Club] Defining the function using refine, Takashi MIYAMOTO
        
        Re: [Coq-Club] Defining the function using refine, AUGER Cédric
        
        Re: [Coq-Club] Defining the function using refine, Hugo Herbelin
        
        Re: [Coq-Club] Defining the function using refine, Takashi MIYAMOTO