The Coq mailing list

[Paviotti Marco <mpav AT itu.dk>]

Hi all, 

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.

Anyone has any suggestions on how to overcome this limitation? 

All the best,
Marco

Attachment: monadinst2.v
Description: Binary data

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail