coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Cofixpoint definition

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: Paviotti Marco <mpav AT itu.dk>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Cofixpoint definition
Date: Sat, 18 Jan 2014 21:41:49 +0100

On 16/01/2014 14:56, Paviotti Marco wrote:
> Anyone has any suggestions on how to overcome this limitation?

You can try to use Mersenne's encoding, as done in the Paco library.

http://plv.mpi-sws.org/paco/

This seems to be the right way to go whenever one reaches the
coinduction limitations.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Cofixpoint definition, Paviotti Marco, 01/16/2014
- Re: [Coq-Club] Cofixpoint definition, Xavier Leroy, 01/18/2014
- Re: [Coq-Club] Cofixpoint definition, Pierre-Marie Pédrot, 01/18/2014