The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On 16/01/14 14:56, Paviotti Marco wrote:

> I am trying to encode a sort of concurrent monad as you can see from 
> the Coq script attached. The bind operator turns out to be a CoFixpoint
> function, though defining it looks like a tricky thing to come by,
> because of the guarded check of Coq.

I would need to see the "seq" library that you're using in order to
understand the problem.  Can you distill your example down some more?

> Anyone has any suggestions on how to overcome this limitation?

Yves Bertot's "Eratosthenes" paper gives some useful tricks:
http://hal.inria.fr/inria-00070658

The PACO work by C-K Hur et al could also help, although it focuses on
coinductive proofs rather than coinductive function definitions:
http://plv.mpi-sws.org/paco/

Hope this helps,

- Xavier Leroy