Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Encoding a mixed recursive-corecursive function

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Encoding a mixed recursive-corecursive function


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page