coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Co-recursion question

From: Jeffrey Harris <janglernpl AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Co-recursion question
Date: Sat, 24 Oct 2009 18:14:26 -0500
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=TthQJEi+uiny3q7eaLkNUY6BnCMRp4ZvBQvWSefJ/IjI1lp744E6XAYjChCwRZpYsl h1mb4NfK7Mkc50aibXYlnh2jREQh+PlLuVuEIGmFlpJXvcx12Fqx2qNC8+T0xG/T7Pan 4z5KDJAh5QD0jbydGDT0Fxz7AnkQaMThGTgZQ=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello!

I apologize for the imprecise phrasing, but does anyone know if the ability to do coinduction/corecursion in Coq expands the class of definable functions on inductive types? For instance, is there any function from nat->nat which is definable in Coq, but would not be definable without the use of coinduction/corecursion? (So, perhaps, a composition of functions f1:nat->stream and f2:stream->nat).

Thanks,
Jeffrey

[Coq-Club] Co-recursion question, Jeffrey Harris
- Re: [Coq-Club] Co-recursion question, Yves Bertot
  - Re: [Coq-Club] Co-recursion question, Jeffrey Harris
    - Re: [Coq-Club] Co-recursion question, Dan Doel
      - [Coq-Club] Tail-recursion, Extraction, Mutual induction, AUGER Cédric
        
        Re: [Coq-Club] Tail-recursion, Extraction, Mutual induction, AUGER Cédric
- Re: [Coq-Club] Co-recursion question, Thorsten Altenkirch