The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

Hello,

From: David Leduc 
<david.leduc6 AT googlemail.com>
Subject: Re: [Coq-Club] Equational Reasoning over streams
Date: Fri, 22 Oct 2010 11:45:50 +0000

> > 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)?

I think you can use Mendler style to nest induction into coinducation if you 
like.
With Tarmo Uustalu (and thanks to Thorsten for many discussions), 
we are playing with mixed induction-coinduction in Coq,
e.g., 
http://www.cs.ioc.ee/~keiko/Coq2.pdf
http://www.cs.ioc.ee/~keiko/types10.pdf

Keiko