coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jannis Limperg <jannis AT limperg.de>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Encoding a mixed recursive-corecursive function
- Date: Mon, 21 Mar 2016 20:16:22 +0100 (CET)
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jannis AT limperg.de; spf=None smtp.mailfrom=jannis AT limperg.de; spf=None smtp.helo=postmaster AT mail.limperg.de
- Ironport-phdr: 9a23:+XNVOhZIB+AbuJWvuK3GB+L/LSx+4OfEezUN459isYplN5qZpcu6bnLW6fgltlLVR4KTs6sC0LqG9fm5EjVauN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDivcSKKFwS3XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIs1AbSy09lgdCS1zO6wi/VZPsuAP7sPB80W+UJ5ulY6ozXGGA5qFtSQSgrCYCLzMj/ymDiMV2iqNAiBagogRy2YGSbIzDZ6k2Rb/UYd5PHTkJZc1WTSEUR9rkN4Y=
Dear Gregory,
The paco library might be useful to you.
thank you very much for the suggestion. I had considered paco, but it
only deals with coinductive definitions in Prop, so I'm unsure how I
could use it to define a corecursive function (short of encoding the
function as a relation, which I've tried before and may have to try
again).
Cheers,
Jannis
- [Coq-Club] Encoding a mixed recursive-corecursive function, Jannis Limperg, 03/19/2016
- Re: [Coq-Club] Encoding a mixed recursive-corecursive function, Gregory Malecha, 03/21/2016
- Re: [Coq-Club] Encoding a mixed recursive-corecursive function, Jannis Limperg, 03/21/2016
- Re: [Coq-Club] Encoding a mixed recursive-corecursive function, Gregory Malecha, 03/21/2016
Archive powered by MHonArc 2.6.18.