coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Equational Reasoning over streams

From: David Leduc <david.leduc6 AT googlemail.com>
To: Thorsten Altenkirch <txa AT cs.nott.ac.uk>
Cc: Herman Geuvers <herman AT cs.ru.nl>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Equational Reasoning over streams
Date: Fri, 22 Oct 2010 11:45:50 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=FTh25MW6pXL8m9hNOLFNUKuk7XUNuHYC+OrbjLzM30IYFCVBOGfTP/gldtIXEsmQIv MNWWi2fz3Bu1uwbzhJ4V3hoxwQG96cKchn6Q3u5kRdJJ1+ulsYlD4Y+7a7zkdjRnZ1Mo Vj56r/Id4Lgri+bEimbnqSdk0ew1Mipm6nIiY=

> The examples are in Agda but hopefully they can be translated to Coq.

Really? I'm already stuck with the first example in the paper? How
would you translate into Coq the definition of Stream_P (a datatype
with an coinductive constructor and an inductive one)?

[Coq-Club] recursive Ltac definitions, Aaron Bohannon
- [Coq-Club] Re: recursive Ltac definitions, Aaron Bohannon
  - [Coq-Club] Equational Reasoning over streams, Herman Geuvers
    - Re: [Coq-Club] Equational Reasoning over streams, Thorsten Altenkirch
      - Re: [Coq-Club] Equational Reasoning over streams, David Leduc
        
        Re: [Coq-Club] Equational Reasoning over streams, Herman Geuvers
        
        Re: [Coq-Club] Equational Reasoning over streams, AUGER Cedric
        
        Re: [Coq-Club] Equational Reasoning over streams, Keiko Nakata
        
        Re: [Coq-Club] Equational Reasoning over streams, David Leduc
- Re: [Coq-Club] recursive Ltac definitions, Adam Chlipala